Module

AdicCompletionQuotient.lean

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionQuotient

15 declarations indexed from sourceView source ↗

Module documentation

The first quotient of an adic completion

For a finitely generated ideal I, reduction of the I-adic completion modulo the extended ideal is canonically the original quotient R ⧸ I. This is the closed-fibre comparison used by formal gluing along completion.

Imports1

Mathlib.RingTheory.AdicCompletion.LocalRing

Imported by2

def

adicCompletionQuotientEquiv

L27 ↗

EtaleFundamentalGroups.adicCompletionQuotientEquiv

Documentation

Reduction modulo the extended ideal identifies the first quotient of an adic completion with the original quotient.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

def adicCompletionQuotientEquiv
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) :
    AdicCompletion I R ⧸ I.map (algebraMap R (AdicCompletion I R)) ≃+*
      R ⧸ I

theorem

adicCompletionQuotientEquiv_mk

L36 ↗

EtaleFundamentalGroups.adicCompletionQuotientEquiv_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionQuotientEquiv_mk
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG)
    (x : AdicCompletion I R) :
    adicCompletionQuotientEquiv I hI
        (Ideal.Quotient.mk (I.map (algebraMap R (AdicCompletion I R))) x) =
      AdicCompletion.evalOneₐ I x

theorem

adicCompletionQuotientEquiv_algebraMap_mk

L48 ↗

EtaleFundamentalGroups.adicCompletionQuotientEquiv_algebraMap_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionQuotientEquiv_algebraMap_mk
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (x : R) :
    adicCompletionQuotientEquiv I hI
        (Ideal.Quotient.mk (I.map (algebraMap R (AdicCompletion I R)))
          (algebraMap R (AdicCompletion I R) x)) =
      Ideal.Quotient.mk I x

def

adicCompletionClosedFiberAlgHom

L61 ↗

EtaleFundamentalGroups.adicCompletionClosedFiberAlgHom

Documentation

The closed-fibre comparison, regarded as an R-algebra map from the adic completion to R ⧸ I.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · full declaration

def adicCompletionClosedFiberAlgHom
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) :
    AdicCompletion I R →ₐ[R] R ⧸ I where
  toRingHom := (adicCompletionQuotientEquiv I hI).toRingHom.comp
    (Ideal.Quotient.mk (I.map (algebraMap R (AdicCompletion I R))))
  commutes' x := adicCompletionQuotientEquiv_algebraMap_mk I hI x

theorem

adicCompletionClosedFiberAlgHom_apply

L69 ↗

EtaleFundamentalGroups.adicCompletionClosedFiberAlgHom_apply

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionClosedFiberAlgHom_apply
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG)
    (x : AdicCompletion I R) :
    adicCompletionClosedFiberAlgHom I hI x =
      adicCompletionQuotientEquiv I hI
        (Ideal.Quotient.mk
          (I.map (algebraMap R (AdicCompletion I R))) x)

theorem

adicCompletionClosedFiberAlgHom_algebraMap

L79 ↗

EtaleFundamentalGroups.adicCompletionClosedFiberAlgHom_algebraMap

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionClosedFiberAlgHom_algebraMap
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (x : R) :
    adicCompletionClosedFiberAlgHom I hI
        (algebraMap R (AdicCompletion I R) x) =
      Ideal.Quotient.mk I x

theorem

adicCompletion_exists_sub_mem_map

L88 ↗

EtaleFundamentalGroups.adicCompletion_exists_sub_mem_map

Documentation

Every element of an adic completion is congruent modulo the extended ideal to an element of the original ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletion_exists_sub_mem_map
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG)
    (x : AdicCompletion I R) :
    ∃ r : R,
      x - algebraMap R (AdicCompletion I R) r ∈
        I.map (algebraMap R (AdicCompletion I R))

theorem

adicCompletion_ker_evalₐ_eq_map_pow

L112 ↗

EtaleFundamentalGroups.adicCompletion_ker_evalₐ_eq_map_pow

Documentation

The kernel of reduction of an I-adic completion modulo I ^ n is the extension of I ^ n to the completion.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletion_ker_evalₐ_eq_map_pow
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (n : ℕ) :
    RingHom.ker (AdicCompletion.evalₐ I n).toRingHom =
      (I ^ n).map (algebraMap R (AdicCompletion I R))

def

adicCompletionPowQuotientEquiv

L142 ↗

EtaleFundamentalGroups.adicCompletionPowQuotientEquiv

Documentation

Reduction modulo any power of a finitely generated adic ideal commutes with completion.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

def adicCompletionPowQuotientEquiv
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (n : ℕ) :
    AdicCompletion I R ⧸
        (I ^ n).map (algebraMap R (AdicCompletion I R)) ≃+*
      R ⧸ I ^ n

theorem

adicCompletionPowQuotientEquiv_mk

L153 ↗

EtaleFundamentalGroups.adicCompletionPowQuotientEquiv_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionPowQuotientEquiv_mk
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (n : ℕ)
    (x : AdicCompletion I R) :
    adicCompletionPowQuotientEquiv I hI n
        (Ideal.Quotient.mk
          ((I ^ n).map (algebraMap R (AdicCompletion I R))) x) =
      AdicCompletion.evalₐ I n x

theorem

adicCompletionPowQuotientEquiv_algebraMap_mk

L166 ↗

EtaleFundamentalGroups.adicCompletionPowQuotientEquiv_algebraMap_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletionPowQuotientEquiv_algebraMap_mk
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (n : ℕ)
    (x : R) :
    adicCompletionPowQuotientEquiv I hI n
        (Ideal.Quotient.mk
          ((I ^ n).map (algebraMap R (AdicCompletion I R)))
          (algebraMap R (AdicCompletion I R) x)) =
      Ideal.Quotient.mk (I ^ n) x

theorem

adicCompletion_exists_sub_mem_map_pow

L179 ↗

EtaleFundamentalGroups.adicCompletion_exists_sub_mem_map_pow

Documentation

Every element of an I-adic completion is congruent modulo the extension of I ^ n to an element of the original ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem adicCompletion_exists_sub_mem_map_pow
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) (n : ℕ)
    (x : AdicCompletion I R) :
    ∃ r : R,
      x - algebraMap R (AdicCompletion I R) r ∈
        (I ^ n).map (algebraMap R (AdicCompletion I R))

def

maximalAdicCompletionResidueEquiv

L199 ↗

EtaleFundamentalGroups.maximalAdicCompletionResidueEquiv

Documentation

The residue ring of a Noetherian local ring is unchanged by maximal-adic completion. The source ideal is stated as the actual maximal ideal of the completed local ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

def maximalAdicCompletionResidueEquiv
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    AdicCompletion (maximalIdeal R) R ⧸
        maximalIdeal (AdicCompletion (maximalIdeal R) R) ≃+*
      R ⧸ maximalIdeal R

theorem

maximalAdicCompletionResidueEquiv_mk

L209 ↗

EtaleFundamentalGroups.maximalAdicCompletionResidueEquiv_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem maximalAdicCompletionResidueEquiv_mk
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x : AdicCompletion (maximalIdeal R) R) :
    maximalAdicCompletionResidueEquiv R
        (Ideal.Quotient.mk
          (maximalIdeal (AdicCompletion (maximalIdeal R) R)) x) =
      AdicCompletion.evalOneₐ (maximalIdeal R) x

theorem

maximalAdicCompletionResidueEquiv_algebraMap_mk

L220 ↗

EtaleFundamentalGroups.maximalAdicCompletionResidueEquiv_algebraMap_mk

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
universe u
open IsLocalRing

Lean source · statement

theorem maximalAdicCompletionResidueEquiv_algebraMap_mk
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x : R) :
    maximalAdicCompletionResidueEquiv R
        (Ideal.Quotient.mk
          (maximalIdeal (AdicCompletion (maximalIdeal R) R))
          (algebraMap R (AdicCompletion (maximalIdeal R) R) x)) =
      Ideal.Quotient.mk (maximalIdeal R) x

Module documentation

The first quotient of an adic completion

Declarations