NYLL
Module

MaximalAdicCompletionMixedEqualizer.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionMixedEqualizer
25 declarations indexed from sourceView source ↗

Module documentation

The mixed completion/localization equalizer

For a Noetherian local ring, a module is the fibre product of its maximal-adic completion and its restrictions to the chosen principal cover of the punctured spectrum. The overlap is computed by localizing the completed module at the same generators.

Imports5
Imported by3

Declarations

theorem

exists_pow_annihilates_of_localizedModule_mk_eq_zero

L33 ↗
EtaleFundamentalGroups.exists_pow_annihilates_of_localizedModule_mk_eq_zero
Documentation

If an element vanishes after localization at each member of a finite family spanning I, then some power of I annihilates it.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
Lean source · statement
theorem exists_pow_annihilates_of_localizedModule_mk_eq_zero
    {R : Type u} [CommRing R] {M : Type v}
    [AddCommGroup M] [Module R M]
    {I : Ideal R} (hI : I.FG) {ι : Type w} [Finite ι]
    (f : ι → R) (hspan : Ideal.span (Set.range f) = I)
    (x : M)
    (hx : ∀ i, LocalizedModule.mkLinearMap (Submonoid.powers (f i)) M x = 0) :
    ∃ n : ℕ, ∀ r : (I ^ n : Ideal R), r.1 • x = 0
abbrev

Rhat

L63 ↗
EtaleFundamentalGroups.Rhat
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev Rhat
abbrev

GeneratorIndex

L65 ↗
EtaleFundamentalGroups.GeneratorIndex
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev GeneratorIndex
abbrev

generator

L68 ↗
EtaleFundamentalGroups.generator
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev generator (i : GeneratorIndex R) : R
abbrev

MaximalAdicCompletionMixedSource

L73 ↗
EtaleFundamentalGroups.MaximalAdicCompletionMixedSource
Documentation

The completion component together with localized components on the chosen principal cover of the punctured spectrum.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev MaximalAdicCompletionMixedSource
abbrev

MaximalAdicCompletionMixedTarget

L80 ↗
EtaleFundamentalGroups.MaximalAdicCompletionMixedTarget
Documentation

The common overlap of the completion and punctured-localization components.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev MaximalAdicCompletionMixedTarget
def

maximalAdicCompletionMixedLeft

L85 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedLeft
Documentation

Restrict the completed component to every chosen principal open.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionMixedLeft :
    MaximalAdicCompletionMixedSource R M →ₗ[R]
      MaximalAdicCompletionMixedTarget R M
def

maximalAdicCompletionMixedRight

L94 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedRight
Documentation

Extend every punctured-localization component to the completed module.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionMixedRight :
    MaximalAdicCompletionMixedSource R M →ₗ[R]
      MaximalAdicCompletionMixedTarget R M
theorem

maximalAdicCompletionMixedLeft_apply

L107 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedLeft_apply
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionMixedLeft_apply
    (x : MaximalAdicCompletionMixedSource R M)
    (i : GeneratorIndex R) :
    maximalAdicCompletionMixedLeft R M x i =
      LocalizedModule.mk x.1 1
theorem

maximalAdicCompletionMixedRight_apply

L116 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedRight_apply
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionMixedRight_apply
    (x : MaximalAdicCompletionMixedSource R M)
    (i : GeneratorIndex R) :
    maximalAdicCompletionMixedRight R M x i =
      IsLocalizedModule.map (Submonoid.powers (generator R i))
        (LocalizedModule.mkLinearMap (Submonoid.powers (generator R i)) M)
        (LocalizedModule.mkLinearMap (Submonoid.powers (generator R i))
          (Rhat R ⊗[R] M))
        (TensorProduct.mk R (Rhat R) M 1) (x.2 i)
def

maximalAdicCompletionMixedPairMap

L128 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedPairMap
Documentation

The canonical pair consisting of completion and punctured restrictions.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionMixedPairMap :
    M →ₗ[R] MaximalAdicCompletionMixedSource R M
def

maximalAdicCompletionMixedEqualizerMap

L135 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedEqualizerMap
Documentation

The canonical map into the mixed completion/localization equalizer.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionMixedEqualizerMap :
    M →ₗ[R] LinearMap.eqLocus
      (maximalAdicCompletionMixedLeft R M)
      (maximalAdicCompletionMixedRight R M)
theorem

maximalAdicCompletionMixedEqualizerMap_completion

L155 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedEqualizerMap_completion
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionMixedEqualizerMap_completion
    (m : M) :
    (maximalAdicCompletionMixedEqualizerMap R M m).1.1 = 1 ⊗ₜ[R] m
theorem

maximalAdicCompletionMixedEqualizerMap_localization

L162 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedEqualizerMap_localization
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionMixedEqualizerMap_localization
    (m : M) (i : GeneratorIndex R) :
    (maximalAdicCompletionMixedEqualizerMap R M m).1.2 i =
      LocalizedModule.mk m 1
def

maximalAdicCompletionAmitsurDifference

L170 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurDifference
Documentation

The Amitsur difference, reassociated so that torsion reflection applies to its outer completed factor.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionAmitsurDifference :
    Rhat R ⊗[R] M →ₗ[R] Rhat R ⊗[R] (Rhat R ⊗[R] M)
theorem

maximalAdicCompletionAmitsurDifference_tmul

L177 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurDifference_tmul
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionAmitsurDifference_tmul
    (s : Rhat R) (m : M) :
    maximalAdicCompletionAmitsurDifference R M (s ⊗ₜ[R] m) =
      s ⊗ₜ[R] (1 ⊗ₜ[R] m) - 1 ⊗ₜ[R] (s ⊗ₜ[R] m)
def

maximalAdicCompletionAmitsurCounit

L188 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurCounit
Documentation

Multiplication of the two completed factors.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionAmitsurCounit :
    Rhat R ⊗[R] (Rhat R ⊗[R] M) →ₗ[R] Rhat R ⊗[R] M
theorem

maximalAdicCompletionAmitsurCounit_tmul

L196 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurCounit_tmul
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionAmitsurCounit_tmul
    (a s : Rhat R) (m : M) :
    maximalAdicCompletionAmitsurCounit R M
        (a ⊗ₜ[R] (s ⊗ₜ[R] m)) =
      (a * s) ⊗ₜ[R] m
theorem

maximalAdicCompletionAmitsurCounit_one_tmul

L205 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurCounit_one_tmul
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionAmitsurCounit_one_tmul
    (x : Rhat R ⊗[R] M) :
    maximalAdicCompletionAmitsurCounit R M (1 ⊗ₜ[R] x) = x
theorem

maximalAdicCompletionAmitsurCounit_difference

L215 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurCounit_difference
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionAmitsurCounit_difference
    (x : Rhat R ⊗[R] M) :
    maximalAdicCompletionAmitsurCounit R M
        (maximalAdicCompletionAmitsurDifference R M x) = 0
theorem

maximalAdicCompletionAmitsurDifference_eq_zero_of_pow

L224 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurDifference_eq_zero_of_pow
Documentation

A power-torsion Amitsur difference for maximal-adic completion is zero.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
theorem maximalAdicCompletionAmitsurDifference_eq_zero_of_pow
    (n : ℕ) (x : Rhat R ⊗[R] M)
    (hx : ∀ r : ((maximalIdeal R) ^ n : Ideal R),
      r.1 • maximalAdicCompletionAmitsurDifference R M x = 0) :
    maximalAdicCompletionAmitsurDifference R M x = 0
theorem

maximalAdicCompletionAmitsurDifference_localized_eq_zero

L240 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurDifference_localized_eq_zero
Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionAmitsurDifference_localized_eq_zero
    (p : LinearMap.eqLocus
      (maximalAdicCompletionMixedLeft R M)
      (maximalAdicCompletionMixedRight R M))
    (i : GeneratorIndex R) :
    LocalizedModule.mkLinearMap (Submonoid.powers (generator R i))
        (Rhat R ⊗[R] (Rhat R ⊗[R] M))
        (maximalAdicCompletionAmitsurDifference R M p.1.1) = 0
theorem

maximalAdicCompletionAmitsurDifference_eq_zero

L276 ↗
EtaleFundamentalGroups.maximalAdicCompletionAmitsurDifference_eq_zero
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
theorem maximalAdicCompletionAmitsurDifference_eq_zero
    (p : LinearMap.eqLocus
      (maximalAdicCompletionMixedLeft R M)
      (maximalAdicCompletionMixedRight R M)) :
    maximalAdicCompletionAmitsurDifference R M p.1.1 = 0
def

maximalAdicCompletionMixedEqualizerEquiv

L302 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedEqualizerEquiv
Documentation

A module over a Noetherian local ring is the mixed equalizer of its maximal-adic completion and its restrictions to the chosen principal cover of the punctured spectrum.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionMixedEqualizerEquiv :
    M ≃ₗ[R] LinearMap.eqLocus
      (maximalAdicCompletionMixedLeft R M)
      (maximalAdicCompletionMixedRight R M)
theorem

maximalAdicCompletionMixedEqualizerEquiv_apply

L358 ↗
EtaleFundamentalGroups.maximalAdicCompletionMixedEqualizerEquiv_apply
Documentation

The mixed equalizer equivalence is the canonical completion/localization pair, in a form convenient for downstream Hom and algebra descent.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w
section MaximalAdic
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]
Lean source · full declaration
theorem maximalAdicCompletionMixedEqualizerEquiv_apply (m : M) :
    (maximalAdicCompletionMixedEqualizerEquiv R M m :
      MaximalAdicCompletionMixedSource R M) =
      (1 ⊗ₜ[R] m, fun _ ↦ LocalizedModule.mk m 1) :=
  rfl

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.