← all areas

Namespace IsAdicComplete 15 theorems

• Adic completeness descends along surjections of Noetherian rings IsAdicComplete.map_of_surjective 0 below · cited by 1 · depth 9
• Finite modules over a complete Noetherian ring are adically complete IsAdicComplete.of_module_finite 0 below · cited by 4 · depth 10
• Idempotent cutting out the local factor at a section IsAdicComplete.exists_isIdempotentElem_apply_eq_zero_isLocalRing_quotient 3 below · cited by 1 · depth 18
• p-adically complete ring with residue field mathbf Fₚ is a DVR IsAdicComplete.exists_isDomain_isDiscreteValuationRing_of_ker_algebraMap_zmod_eq_span 0 below · cited by 9 · depth 21
• Finite free algebras over (p)-adically complete rings IsAdicComplete.of_module_finite_free_span_natCast 0 below · cited by 20 · depth 21
• Lifting residual norms to exact norms over a varpi-adically complete ring IsAdicComplete.exists_isUnit_prod_iterate_eq_of_forall_isUnit_exists_sub_mem_span_singleton 0 below · cited by 1 · depth 25
• Finite modules over a complete Noetherian ring are complete IsAdicComplete.of_finite_of_isNoetherianRing 0 below · cited by 5 · depth 25
• Complete ring with maximal principal ideal is a DVR IsAdicComplete.exists_isDomain_isDiscreteValuationRing_of_span_singleton_isMaximal 0 below · cited by 2 · depth 26
• Primitive n-th roots of unity lift along the residue map IsAdicComplete.exists_isPrimitiveRoot_of_residueField 0 below · cited by 3 · depth 26
• Finite free algebras inherit adic completeness IsAdicComplete.of_module_finite_free_map 0 below · cited by 1 · depth 27
• Complete rings with (p) maximal and p regular are DVRs IsAdicComplete.exists_isDomain_isDiscreteValuationRing_of_span_natCast_isMaximal 0 below · cited by 3 · depth 28
• Inverse limits of truncated modules over an adically complete ring IsAdicComplete.finite_and_surjective_and_apply_eq_zero_iff_of_forall_ker_le_pow_smul_top 0 below · cited by 1 · depth 34
• Nilpotent ideals are adically complete IsAdicComplete.of_isNilpotent 0 below · cited by 13 · depth 34
• Hensel descent of e-th roots of units to the base IsAdicComplete.mem_range_algebraMap_of_pow_eq_unit_of_forall_sub_mem_maximalIdeal 0 below · cited by 1 · depth 35
• Passing factorisation through Artinian quotients to a complete local ring IsAdicComplete.existsUnique_algHom_comp_eq_of_forall_residue_eq_of_factorsThrough_artinian 0 below · cited by 2 · depth 36