← all areas

Namespace AdicCompletion 37 theorems

• Extension of a ring map to the adic completion AdicCompletion.exists_ringHom_comp_algebraMap_eq_of_forall_exists_pow_le_comap 0 below · cited by 8 · depth 18
• Completion at a maximal ideal commutes with localising there AdicCompletion.exists_ringEquiv_of_isLocalization_atPrime_of_isMaximal 0 below · cited by 12 · depth 21
• Automorphisms of widehat R are determined on R AdicCompletion.ringEquiv_eq_of_forall_apply_algebraMap_eq_of_isLocalRing 0 below · cited by 1 · depth 21
• Adic completion of a Noetherian ring is Noetherian AdicCompletion.isNoetherianRing_of_isNoetherianRing 1 below · cited by 29 · depth 23
• Levelwise isomorphic truncations give isomorphic adic completions AdicCompletion.exists_ringEquiv_of_forall_quotient_mk_comp_surjective_of_forall_ker_eq_pow 0 below · cited by 4 · depth 25
• Completion of an étale algebra is widehatR[T]/(f) AdicCompletion.exists_ringHom_ringEquiv_adjoinRoot_of_etale_of_isMaximal 6 below · cited by 1 · depth 25
• Adic completion at a maximal ideal is complete Noetherian local AdicCompletion.isNoetherianRing_and_exists_isLocalRing_maximalIdeal_eq_map_of_isMaximal 2 below · cited by 12 · depth 25
• Adic completions are transported along ring isomorphisms AdicCompletion.exists_ringEquiv_map_of_ringEquiv 0 below · cited by 7 · depth 26
• Adic completion of invariants: Noetherian, module-finite case AdicCompletion.map_algebraLinearMap_injective_and_mem_range_iff_of_isInvariant 0 below · cited by 1 · depth 28
• Invariants of a semilocal adic completion via one component AdicCompletion.semilocalComponent_smul_and_injOn_and_surjOn_fixedPoints 0 below · cited by 1 · depth 28
• Completion at a maximal ideal: complete local, with universal property AdicCompletion.exists_isLocalRing_and_existsUnique_lift_of_isArtinianRing 3 below · cited by 15 · depth 30
• Base change of a completed power-series chart along A₀ → A AdicCompletion.exists_ringEquiv_mvPowerSeries_quotient_map_of_tensorProduct_of_flat 11 below · cited by 2 · depth 30
• Residue field of a completed two-variable chart via constant coefficients AdicCompletion.exists_ringHom_residueField_surjective_of_ringEquiv_mvPowerSeries_quotient 0 below · cited by 2 · depth 30
• Primes of ̂ R contracting to 𝔪 AdicCompletion.eq_maximalIdeal_of_comap_algebraMap_eq_maximalIdeal 0 below · cited by 2 · depth 31
• Adic completion commutes with quotients over a Noetherian ring AdicCompletion.exists_ringEquiv_quotient_map_adicCompletion_quotient 0 below · cited by 1 · depth 31
• Analytic normality at a tame point of a finite cover AdicCompletion.isDomain_and_isIntegrallyClosed_of_isInvariant_of_isLocalization_atPrime_of_tame 38 below · cited by 1 · depth 31
• Local homomorphisms out of an adic completion agree on R AdicCompletion.ringHom_eq_of_map_maximalIdeal_le_of_forall_apply_algebraMap_eq 0 below · cited by 2 · depth 31
• A regular pair in the n-adic completion of a normal surface cover AdicCompletion.exists_isRegular_pair_of_isIntegrallyClosed_of_ringKrullDim_eq_two 6 below · cited by 1 · depth 32
• Domain and normality pass to the completion of the localisation AdicCompletion.isDomain_and_isIntegrallyClosed_adicCompletion_maximalIdeal_of_isLocalization_atPrime 0 below · cited by 1 · depth 32
• Locality and dimension ≤ 2 of the n-adic completion AdicCompletion.isLocalRing_and_ringKrullDim_le_two_of_liesOver 5 below · cited by 1 · depth 32
• Reducedness and separability of the completed generic fibre AdicCompletion.isReduced_and_isSeparable_genericFibre_of_isInvariant 0 below · cited by 1 · depth 32
• Regularity of non-maximal localisations of a completed tame cover AdicCompletion.isRegularLocalRing_localization_atPrime_of_not_isMaximal_of_tame 26 below · cited by 1 · depth 32
• Nonzerodivisors persist in the completed module-finite cover AdicCompletion.mem_nonZeroDivisors_algebraMap_of_mem_nonZeroDivisors_of_liesOver 0 below · cited by 4 · depth 32
• Adic completion of a Hom module between finite modules AdicCompletion.bijective_of_forall_val_apply_eq_mk_apply 0 below · cited by 1 · depth 33
• Base change of thread modules along adic completions AdicCompletion.exists_bijective_forall_apply_tmul_eq_of_isBaseChange_of_forall_ker_eq_pow_smul_top 4 below · cited by 1 · depth 33
• A comparison map widehatHom_A(M,N)toHom_A(M,widehat N) AdicCompletion.exists_linearMap_forall_val_apply_eq_mk_apply 0 below · cited by 1 · depth 33
• Threads of an adic system as a finite module over ̂ B AdicCompletion.exists_module_finite_forall_comp_eq_and_ker_eq_pow_smul_top_of_forall_surjective 1 below · cited by 1 · depth 33
• Flatness of adic completion along a flat finite-type map AdicCompletion.exists_ringHom_comp_algebraMap_eq_and_flat_of_flat_of_finiteType 3 below · cited by 1 · depth 33
• Adic completion at a finitely generated ideal is complete AdicCompletion.isAdicComplete_map_algebraMap_of_fg 0 below · cited by 2 · depth 33
• Regularity of widehatC_𝔭 at non-maximal primes containing s AdicCompletion.isRegularLocalRing_localization_atPrime_of_mem_of_not_isMaximal_of_tame 20 below · cited by 1 · depth 33
• Exactness of I-adic completion on kernels of maps of finite modules AdicCompletion.map_ker_subtype_injective_and_range_eq_ker_map 0 below · cited by 1 · depth 33
• Analytic unramifiedness: widehatC_P is a field at non-maximal primes AdicCompletion.isField_localization_atPrime_of_not_isMaximal_of_isSeparable 7 below · cited by 1 · depth 34
• Completions of two étale coefficient changes with equal residue cardinalities AdicCompletion.nonempty_ringEquiv_adicCompletion_tensorProduct_of_flat_of_map_maximalIdeal_eq_of_card_eq 21 below · cited by 4 · depth 34
• Completed unramified base change is finite étale AdicCompletion.exists_moduleFinite_etale_adicCompletion_tensorProduct_of_flat_of_map_maximalIdeal_eq 13 below · cited by 1 · depth 35
• Residue field of an adic completion at a maximal ideal AdicCompletion.finite_residueField_and_card_eq_of_isMaximal 4 below · cited by 1 · depth 35
• Adic completions at a common prime of two localisations agree AdicCompletion.exists_ringEquiv_of_isLocalization_of_comap_eq_of_comap_eq 1 below · cited by 1 · depth 36
• Adic completions of a module-finite algebra at a maximal ideal AdicCompletion.exists_algebra_moduleFinite_of_moduleFinite_of_isMaximal 0 below · cited by 2 · depth 37