Functoriality of adic completions

TheoremLifting compatible ring maps to adic completions#✓fully proved

A ring homomorphism compatible with the adic topologies lifts to a map from the adic completion into an adically complete target.

theorem AdicCompletion.exists_ringHom_comp_algebraMap_eq_of_forall_exists_pow_le_comap
    {B : Type*} [CommRing B] (𝔪 : Ideal B) {S : Type*} [CommRing S] (J : Ideal S)
    [IsAdicComplete J S] (ev : B →+* S)
    (hcont : ∀ k : ℕ, ∃ n : ℕ, 𝔪 ^ n ≤ (J ^ k).comap ev) :
    ∃ ψ : AdicCompletion 𝔪 B →+* S, ψ.comp (algebraMap B (AdicCompletion 𝔪 B)) = ev

TheoremRing equivalences induce equivalences of adic completions#✓fully proved

A ring equivalence induces an equivalence of adic completions.

theorem AdicCompletion.exists_ringEquiv_map_of_ringEquiv
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (I : Ideal R) (e : R ≃+* S) :
    ∃ ê : AdicCompletion I R ≃+* AdicCompletion (I.map e) S,
      ∀ r : R, ê (algebraMap R (AdicCompletion I R) r) =
        algebraMap S (AdicCompletion (I.map e) S) (e r)

Used by 1

Used byRing equivalences of local rings induce equivalent completions

TheoremRing equivalences of local rings induce equivalent completions#✓fully proved

A ring equivalence between local rings induces an equivalence of their maximal-ideal adic completions.

theorem IsLocalRing.exists_ringEquiv_adicCompletion_maximalIdeal_comp_algebraMap_of_ringEquiv
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S]
    (e : R ≃+* S) :
    ∃ ê : AdicCompletion (IsLocalRing.maximalIdeal R) R ≃+*
        AdicCompletion (IsLocalRing.maximalIdeal S) S,
      ∀ r : R, ê (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R) r) =
        algebraMap S (AdicCompletion (IsLocalRing.maximalIdeal S) S) (e r)

Uses 1

Proof usesRing equivalences induce equivalences of adic completions

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.