← all areas

Namespace HenselianLocalRing 21 theorems

• Complete local rings are Henselian HenselianLocalRing.of_isAdicComplete_maximalIdeal 0 below · cited by 9 · depth 11
• Henselian lifting of residue points of smooth algebras HenselianLocalRing.exists_algHom_lift_of_isSmoothAt 1 below · cited by 3 · depth 14
• Residue-field points of étale algebras lift over Henselian local rings HenselianLocalRing.exists_algHom_lift_of_etale 0 below · cited by 8 · depth 15
• Finite part of a quasi-finite algebra over a Henselian local ring HenselianLocalRing.exists_isIdempotentElem_moduleFinite_quotient_of_quasiFinite 2 below · cited by 1 · depth 16
• Idempotents lift uniquely to module-finite algebras over Henselian local rings HenselianLocalRing.existsUnique_isIdempotentElem_mk_eq_of_moduleFinite 1 below · cited by 9 · depth 17
• Module-finite algebras over henselian local rings split into local factors HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite 2 below · cited by 10 · depth 22
• Hensel sections of formally étale A[T]-algebras, non-noetherian base HenselianLocalRing.existsUnique_section_and_ker_eq_span_of_formallyUnramified_of_isLocalization 2 below · cited by 1 · depth 24
• Module-finiteness of S_q over a henselian local ring HenselianLocalRing.moduleFinite_localization_atPrime_of_quasiFiniteAt 2 below · cited by 2 · depth 25
• Primitive q-th root of unity from a (q²-1)-st root of q HenselianLocalRing.exists_isPrimitiveRoot_of_pow_sq_sub_one_eq 0 below · cited by 6 · depth 26
• Module-finiteness of S/hS over a henselian valuation ring HenselianLocalRing.moduleFinite_quotient_span_and_exists_pow_mem_of_isLocalizationAtPrime_of_mem_nonZeroDivisors 4 below · cited by 2 · depth 26
• Integral local extensions of henselian local rings are henselian HenselianLocalRing.of_isIntegral_of_isLocalRing 4 below · cited by 14 · depth 26
• Sections over a henselian base parametrised by the value of T HenselianLocalRing.existsUnique_section_and_ker_eq_span_of_formallySmooth_of_formallyUnramified 2 below · cited by 3 · depth 27
• Finite flat branch through an isolated point over a henselian DVR HenselianLocalRing.exists_ideal_moduleFinite_quotient_of_forall_isPrime_imp_eq_of_isDiscreteValuationRing 5 below · cited by 1 · depth 27
• Integrality modulo a prime over a henselian base HenselianLocalRing.forall_exists_monic_dvd_eval_of_prime_of_not_associated 5 below · cited by 1 · depth 27
• A domain module-finite over a henselian local ring is local HenselianLocalRing.isLocalRing_of_isDomain_of_moduleFinite 2 below · cited by 3 · depth 27
• Finiteness of localisations of a finite algebra over a henselian base HenselianLocalRing.moduleFinite_localizationAtPrime_of_moduleFinite 3 below · cited by 2 · depth 27
• Module-finite local algebras over henselian local rings are henselian HenselianLocalRing.of_moduleFinite_of_isLocalRing 3 below · cited by 5 · depth 27
• Idempotents lift along 𝔪 B for finite algebras over henselian local rings HenselianLocalRing.exists_isIdempotentElem_map_eq_of_module_finite 1 below · cited by 1 · depth 28
• Hensel lifting of primitive n-th roots of unity HenselianLocalRing.exists_isPrimitiveRoot_of_isUnit_of_residueField 0 below · cited by 4 · depth 31
• Unique lifting of simple residual roots over a henselian local ring HenselianLocalRing.existsUnique_isRoot_map_residue_eq_of_isRoot_of_derivative_ne_zero 0 below · cited by 2 · depth 33
• Teichmüller lift of a unit in a Henselian local ring HenselianLocalRing.exists_pow_card_residueField_sub_one_eq_one_sub_mem_maximalIdeal 0 below · cited by 1 · depth 34