NYLL
Module

MaximalAdicCompletionModuleGluingData.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionModuleGluingData
33 declarations indexed from sourceView source ↗

Module documentation

Module data for maximal-adic formal gluing

This file packages the degree-zero Cech diagram used in formal gluing. A datum has one completion module, one module on every principal chart, common completion/chart overlap modules, and common chart/chart overlap modules. Its global sections are the simultaneous equalizer of all restriction maps.

For the standard datum attached to an R-module M, the completion chart is Rhat tensor M, the principal charts are the localized modules M_f, and the overlap maps are the canonical localization maps. The mixed equalizer theorem identifies the resulting global-sections module with M.

Imports2
Imported by2

Declarations

structure

ModuleFormalGluingDatum

L36 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum
Documentation

A degree-zero module gluing diagram. Besides the completion/principal overlaps, it records every principal/principal overlap; equality of the two maps to these latter objects is the punctured Cech cocycle condition.

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 · full declaration
structure ModuleFormalGluingDatum
    (R : Type u) [CommRing R] (ι : Type v) where
  /-- The module on the completion chart. -/
  completion : ModuleCat.{w} R
  /-- The module on each principal chart. -/
  principal : ι → ModuleCat.{w} R
  /-- The common module on each completion/principal overlap. -/
  completionLocalOverlap : ι → ModuleCat.{w} R
  /-- The common module on each ordered pair of principal charts. -/
  principalOverlap : ι → ι → ModuleCat.{w} R
  /-- Restriction from the completion chart to each common overlap. -/
  completionRestriction :
    (i : ι) → completion ⟶ completionLocalOverlap i
  /-- Restriction from each principal chart to its completion overlap. -/
  localToCompletionOverlap :
    (i : ι) → principal i ⟶ completionLocalOverlap i
  /-- Restriction from the first principal chart to a pairwise overlap. -/
  localRestrictionLeft :
    (i j : ι) → principal i ⟶ principalOverlap i j
  /-- Restriction from the second principal chart to a pairwise overlap. -/
  localRestrictionRight :
    (i j : ι) → principal j ⟶ principalOverlap i j
abbrev

Source

L65 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.Source
Documentation

The completion component together with all principal-chart 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev Source
abbrev

CompletionLocalTarget

L69 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.CompletionLocalTarget
Documentation

The completion/principal overlap 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev CompletionLocalTarget
abbrev

PuncturedCechTarget

L73 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.PuncturedCechTarget
Documentation

The degree-one Cech components for the punctured principal cover.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev PuncturedCechTarget
abbrev

Target

L77 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.Target
Documentation

All overlap components in the formal-gluing diagram.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev Target
def

completionLocalLeft

L82 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.completionLocalLeft
Documentation

Restrict the completion component to every completion/principal overlap.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def completionLocalLeft :
    D.Source →ₗ[R] D.CompletionLocalTarget
def

completionLocalRight

L89 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.completionLocalRight
Documentation

Restrict each principal component to its completion/principal overlap.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def completionLocalRight :
    D.Source →ₗ[R] D.CompletionLocalTarget
def

puncturedCechLeft

L97 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.puncturedCechLeft
Documentation

The first restriction of every ordered pair of principal 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def puncturedCechLeft :
    ((i : ι) → D.principal i) →ₗ[R] D.PuncturedCechTarget
def

puncturedCechRight

L103 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.puncturedCechRight
Documentation

The second restriction of every ordered pair of principal 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def puncturedCechRight :
    ((i : ι) → D.principal i) →ₗ[R] D.PuncturedCechTarget
abbrev

PuncturedCechSections

L109 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.PuncturedCechSections
Documentation

Local tuples satisfying all pairwise Cech cocycle equations.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev PuncturedCechSections
def

left

L113 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.left
Documentation

The first map of the simultaneous formal-gluing 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def left : D.Source →ₗ[R] D.Target
def

right

L119 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.right
Documentation

The second map of the simultaneous formal-gluing 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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def right : D.Source →ₗ[R] D.Target
abbrev

Sections

L125 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.Sections
Documentation

The H^0 module of a formal-gluing datum.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
abbrev Sections
theorem

mem_sections_iff

L130 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.mem_sections_iff
Documentation

Membership in H^0 is exactly completion/local compatibility together with the punctured Cech cocycle condition.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
theorem mem_sections_iff (x : D.Source) :
    x ∈ D.Sections ↔
      D.completionLocalLeft x = D.completionLocalRight x ∧
        D.puncturedCechLeft x.2 = D.puncturedCechRight x.2
def

sectionsToPuncturedCech

L143 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.sectionsToPuncturedCech
Documentation

Forget the completion component of a global section and retain its punctured Cech section.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def sectionsToPuncturedCech :
    D.Sections →ₗ[R] D.PuncturedCechSections
def

completionProjection

L153 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.completionProjection
Documentation

The canonical map from global sections to the completion component.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def completionProjection : D.Sections →ₗ[R] D.completion
def

localProjection

L158 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.localProjection
Documentation

The canonical map from global sections to a principal component.

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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
def localProjection (i : ι) : D.Sections →ₗ[R] D.principal i
theorem

completionProjection_apply

L164 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.completionProjection_apply
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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
theorem completionProjection_apply (x : D.Sections) :
    D.completionProjection x = x.1.1
theorem

localProjection_apply

L169 ↗
EtaleFundamentalGroups.ModuleFormalGluingDatum.localProjection_apply
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
namespace ModuleFormalGluingDatum
variable {R : Type u} [CommRing R] {ι : Type v}
variable (D : ModuleFormalGluingDatum.{u, v, w} R ι)
Lean source · statement
theorem localProjection_apply (x : D.Sections) (i : ι) :
    D.localProjection i x = x.1.2 i
abbrev

GluingRhat

L180 ↗
EtaleFundamentalGroups.GluingRhat
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev GluingRhat
abbrev

GluingGeneratorIndex

L183 ↗
EtaleFundamentalGroups.GluingGeneratorIndex
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev GluingGeneratorIndex
abbrev

gluingGenerator

L186 ↗
EtaleFundamentalGroups.gluingGenerator
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev gluingGenerator (i : GluingGeneratorIndex R) : R
abbrev

GluingPowers

L189 ↗
EtaleFundamentalGroups.GluingPowers
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev GluingPowers (i : GluingGeneratorIndex R) : Submonoid R
def

maximalAdicCompletionStandardModuleGluingDatum

L193 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingDatum
Documentation

The standard formal-gluing datum attached to an R-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 w) [AddCommGroup M] [Module R M]
Lean source · full declaration
def maximalAdicCompletionStandardModuleGluingDatum :
    ModuleFormalGluingDatum R (GluingGeneratorIndex R) where
  completion := ModuleCat.of R (GluingRhat R ⊗[R] M)
  principal i := ModuleCat.of R (LocalizedModule (GluingPowers R i) M)
  completionLocalOverlap i :=
    ModuleCat.of R
      (LocalizedModule (GluingPowers R i) (GluingRhat R ⊗[R] M))
  principalOverlap i j :=
    ModuleCat.of R
      (LocalizedModule (GluingPowers R j)
        (LocalizedModule (GluingPowers R i) M))
  completionRestriction i := ModuleCat.ofHom <|
    LocalizedModule.mkLinearMap
      (GluingPowers R i) (GluingRhat R ⊗[R] M)
  localToCompletionOverlap i := ModuleCat.ofHom <|
    IsLocalizedModule.map (GluingPowers R i)
      (LocalizedModule.mkLinearMap (GluingPowers R i) M)
      (LocalizedModule.mkLinearMap
        (GluingPowers R i) (GluingRhat R ⊗[R] M))
      (TensorProduct.mk R (GluingRhat R) M 1)
  localRestrictionLeft i j := ModuleCat.ofHom <|
    LocalizedModule.mkLinearMap (GluingPowers R j)
      (LocalizedModule (GluingPowers R i) M)
  localRestrictionRight i j := ModuleCat.ofHom <|
    IsLocalizedModule.map (GluingPowers R j)
      (LocalizedModule.mkLinearMap (GluingPowers R j) M)
      (LocalizedModule.mkLinearMap (GluingPowers R j)
        (LocalizedModule (GluingPowers R i) M))
      (LocalizedModule.mkLinearMap (GluingPowers R i) M)
abbrev

StandardGluingDatum

L223 ↗
EtaleFundamentalGroups.StandardGluingDatum
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
abbrev StandardGluingDatum
def

maximalAdicCompletionStandardModuleGluingMap

L228 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingMap
Documentation

The canonical completion/localization tuple is a section of the standard formal-gluing datum.

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 w) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionStandardModuleGluingMap :
    M →ₗ[R] (StandardGluingDatum R M).Sections
theorem

maximalAdicCompletionStandardModuleGluingMap_completion

L252 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingMap_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 w) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionStandardModuleGluingMap_completion (m : M) :
    (maximalAdicCompletionStandardModuleGluingMap R M m).1.1 =
      1 ⊗ₜ[R] m
theorem

maximalAdicCompletionStandardModuleGluingMap_localization

L259 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingMap_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 w) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · statement
theorem maximalAdicCompletionStandardModuleGluingMap_localization
    (m : M) (i : GluingGeneratorIndex R) :
    (maximalAdicCompletionStandardModuleGluingMap R M m).1.2 i =
      LocalizedModule.mk m 1
def

maximalAdicCompletionStandardPuncturedCechMap

L268 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardPuncturedCechMap
Documentation

The canonical punctured Cech section associated to an R-module element. This is the degree-zero source used before the completion component is imposed.

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 w) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionStandardPuncturedCechMap :
    M →ₗ[R] (StandardGluingDatum R M).PuncturedCechSections
theorem

maximalAdicCompletionStandardPuncturedCechMap_apply

L275 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardPuncturedCechMap_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 w) [AddCommGroup M] [Module R M]
omit [IsNoetherianRing R] in
Lean source · full declaration
theorem maximalAdicCompletionStandardPuncturedCechMap_apply
    (m : M) :
    (maximalAdicCompletionStandardPuncturedCechMap R M m).1 =
      fun i ↦ LocalizedModule.mkLinearMap (GluingPowers R i) M m :=
  rfl
theorem

exists_pow_annihilates_of_standardPuncturedCechMap_eq_zero

L283 ↗
EtaleFundamentalGroups.exists_pow_annihilates_of_standardPuncturedCechMap_eq_zero
Documentation

The kernel of restriction to the punctured Cech diagram is maximal-ideal-power torsion.

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 w) [AddCommGroup M] [Module R M]
Lean source · statement
theorem exists_pow_annihilates_of_standardPuncturedCechMap_eq_zero
    (m : M)
    (hm : maximalAdicCompletionStandardPuncturedCechMap R M m = 0) :
    ∃ n : ℕ, ∀ r : ((maximalIdeal R) ^ n : Ideal R), r.1 • m = 0
def

maximalAdicCompletionStandardModuleGluingSectionsEquiv

L312 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingSectionsEquiv
Documentation

The H^0 of the standard completion/principal Cech datum is the original module. This is the object-level source for formal-gluing effectivity; comparison with arbitrary datum components is handled separately.

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 w) [AddCommGroup M] [Module R M]
Lean source · statement
def maximalAdicCompletionStandardModuleGluingSectionsEquiv :
    M ≃ₗ[R] (StandardGluingDatum R M).Sections
theorem

maximalAdicCompletionStandardModuleGluingSectionsEquiv_apply

L336 ↗
EtaleFundamentalGroups.maximalAdicCompletionStandardModuleGluingSectionsEquiv_apply
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 w) [AddCommGroup M] [Module R M]
Lean source · statement
theorem maximalAdicCompletionStandardModuleGluingSectionsEquiv_apply
    (m : M) :
    maximalAdicCompletionStandardModuleGluingSectionsEquiv R M m =
      maximalAdicCompletionStandardModuleGluingMap R M m

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