Skip to content

Kernels of evaluation maps out of adic completions

TheoremCompletion of a Noetherian local ring is faithfully flat#✓fully proved

The adic completion of a Noetherian local ring at its maximal ideal is faithfully flat.

theorem IsLocalRing.faithfullyFlat_adicCompletion_maximalIdeal
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] :
    Module.FaithfullyFlat R (AdicCompletion (maximalIdeal R) R)
Used by 2
Used byIdeals contract to themselves along local adic completion · Adic completion preserves Krull dimension at least two

TheoremIdeals contract to themselves along local adic completion#✓fully proved

Ideals contract back to themselves along the adic completion map of a Noetherian local ring.

theorem IsLocalRing.comap_map_adicCompletion_eq
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R) :
    (I.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))).comap
      (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) = I
Uses 1
Proof usesCompletion of a Noetherian local ring is faithfully flat
5 fully proved

Scalars

DefinitionAlgebra map between maximal ideal power quotients of a ring and its completion#✓fully proved

The finite quotient of the completion by a power of its maximal ideal identifies with the corresponding quotient of the ring.

noncomputable def quotientMaximalIdealPowAlgHom (n : ℕ) :
    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
      →ₐ[k] A ⧸ maximalIdeal A ^ n :=
  Ideal.Quotient.liftₐ _ ((evalₐ (maximalIdeal A) n).restrictScalars k) fun x hx => by
    rwa [maximalIdeal_pow_eq_ker_evalₐ, RingHom.mem_ker] at hx
Used by 1
Used byIsomorphism of maximal ideal power quotients of a ring and its completion

DefinitionIsomorphism of maximal ideal power quotients of a ring and its completion#✓fully proved

The finite quotient of the completion by a power of its maximal ideal identifies with the corresponding quotient of the ring.

noncomputable def quotientMaximalIdealPowAlgEquiv (n : ℕ) :
    (AdicCompletion (maximalIdeal A) A ⧸ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
      ≃ₐ[k] A ⧸ maximalIdeal A ^ n :=
  AlgEquiv.ofBijective _ (quotientMaximalIdealPowAlgHom_bijective k n)
Uses 1 · Used by 1
Statement usesAlgebra map between maximal ideal power quotients of a ring and its completion
Used byMaximal ideal power quotients transported along an isomorphism

Transport

DefinitionMaximal ideal power quotients transported along an isomorphism#✓fully proved

The finite quotients of B by powers of its maximal ideal agree with those of A, transported along an algebra isomorphism with the completion of A.

noncomputable def quotientMaximalIdealPowAlgEquivOfAlgEquiv (n : ℕ) :
    (B ⧸ maximalIdeal B ^ n) ≃ₐ[k] A ⧸ maximalIdeal A ^ n :=
  (Ideal.quotientEquivAlg (maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ n)
    (maximalIdeal B ^ n) Φ (by rw [Ideal.map_pow, map_maximalIdeal_algEquiv])).symm.trans
    (quotientMaximalIdealPowAlgEquiv k n)
Uses 1
Statement usesIsomorphism of maximal ideal power quotients of a ring and its completion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.