Module

MaximalAdicCompletionModuleCoverDescent.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionModuleCoverDescent

31 declarations indexed from sourceView source ↗

Module documentation

Faithfully flat descent for the maximal-adic module cover

Let Rhat be the completion of a Noetherian local ring R at its maximal ideal, and let R_i be the principal localizations associated to a finite generating family of that ideal. This file packages the single affine cover

R -> Rhat x product_i R_i.

The cover is faithfully flat because its completion factor already is. We then apply comonadic module descent to a genuine descent coalgebra on this cover. Its descended module is presented explicitly as the equalizer of the coalgebra map and the adjunction unit. The main constructions identify base change of this equalizer with the cover module, with the completion chart, and with every principal chart.

The final structure records when an abstract ModuleFormalGluingDatum is identified, at the level of its degree-zero and degree-one diagrams, with such a full cover descent coalgebra. Its chart comparison isomorphisms are derived from those diagram identifications; they are not fields of the structure.

Imports3

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionModuleGluingData
Mathlib.Algebra.Category.ModuleCat.Descent
Mathlib.CategoryTheory.Adjunction.FullyFaithful

Imported by1

Nyll.EtaleFundamentalGroups.Purity.Local.All

abbrev

MaximalAdicModuleCoverCompletion

L45 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverCompletion

Documentation

The maximal-adic completion occurring in the module cover.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

abbrev MaximalAdicModuleCoverCompletion

abbrev

MaximalAdicModuleCoverGeneratorIndex

L49 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverGeneratorIndex

Documentation

The finite family indexing the chosen generators of the maximal ideal.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

abbrev MaximalAdicModuleCoverGeneratorIndex

abbrev

maximalAdicModuleCoverGenerator

L53 ↗

EtaleFundamentalGroups.maximalAdicModuleCoverGenerator

Documentation

A member of the chosen generating family of the maximal ideal.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

abbrev maximalAdicModuleCoverGenerator
    (i : MaximalAdicModuleCoverGeneratorIndex R) : R

abbrev

MaximalAdicModuleCoverLocalization

L58 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverLocalization

Documentation

The principal localization associated to a chosen generator.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

abbrev MaximalAdicModuleCoverLocalization
    (i : MaximalAdicModuleCoverGeneratorIndex R)

abbrev

MaximalAdicModuleCover

L64 ↗

EtaleFundamentalGroups.MaximalAdicModuleCover

Documentation

The single affine algebra containing the completion chart and all principal charts.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

abbrev MaximalAdicModuleCover

def

maximalAdicModuleCoverToCompletion

L70 ↗

EtaleFundamentalGroups.maximalAdicModuleCoverToCompletion

Documentation

Projection of the module cover to its completion factor.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

def maximalAdicModuleCoverToCompletion :
    MaximalAdicModuleCover R →+* MaximalAdicModuleCoverCompletion R

def

maximalAdicModuleCoverToPrincipal

L75 ↗

EtaleFundamentalGroups.maximalAdicModuleCoverToPrincipal

Documentation

Projection of the module cover to one principal-localization factor.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

def maximalAdicModuleCoverToPrincipal
    (i : MaximalAdicModuleCoverGeneratorIndex R) :
    MaximalAdicModuleCover R →+* MaximalAdicModuleCoverLocalization R i

theorem

maximalAdicModuleCoverToCompletion_comp

L84 ↗

EtaleFundamentalGroups.maximalAdicModuleCoverToCompletion_comp

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

theorem maximalAdicModuleCoverToCompletion_comp :
    (maximalAdicModuleCoverToCompletion R).comp
        (algebraMap R (MaximalAdicModuleCover R)) =
      algebraMap R (MaximalAdicModuleCoverCompletion R)

theorem

maximalAdicModuleCoverToPrincipal_comp

L92 ↗

EtaleFundamentalGroups.maximalAdicModuleCoverToPrincipal_comp

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

Lean source · statement

theorem maximalAdicModuleCoverToPrincipal_comp
    (i : MaximalAdicModuleCoverGeneratorIndex R) :
    (maximalAdicModuleCoverToPrincipal R i).comp
        (algebraMap R (MaximalAdicModuleCover R)) =
      algebraMap R (MaximalAdicModuleCoverLocalization R i)

theorem

maximalAdicModuleCover_flat

L105 ↗

EtaleFundamentalGroups.maximalAdicModuleCover_flat

Documentation

The completion/principal product is flat over the original local ring.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · statement

theorem maximalAdicModuleCover_flat :
    Module.Flat R (MaximalAdicModuleCover R)

theorem

maximalAdicModuleCover_faithfullyFlat

L111 ↗

EtaleFundamentalGroups.maximalAdicModuleCover_faithfullyFlat

Documentation

The completion/principal product is faithfully flat over the original local ring. Faithfulness is detected by the completion factor.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · statement

theorem maximalAdicModuleCover_faithfullyFlat :
    Module.FaithfullyFlat R (MaximalAdicModuleCover R)

abbrev

MaximalAdicModuleCoverAdjunction

L129 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverAdjunction

Documentation

The extension/restriction adjunction for the single maximal-adic module cover.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · statement

abbrev MaximalAdicModuleCoverAdjunction

abbrev

MaximalAdicModuleCoverDescentDatum

L135 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum

Documentation

A genuine faithfully-flat module descent datum on the single completion/principal product cover.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · statement

abbrev MaximalAdicModuleCoverDescentDatum

instance

(anonymous instance)

L142 ↗

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)

Lean source · statement

instance : Module R D.A

def

left

L146 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.left

Documentation

The coalgebra structure map, viewed after restriction to R.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def left :
    (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj D.A ⟶
      (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj
        ((ModuleCat.extendScalars
          (algebraMap R (MaximalAdicModuleCover R))).obj
            ((ModuleCat.restrictScalars
              (algebraMap R (MaximalAdicModuleCover R))).obj D.A))

def

right

L159 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.right

Documentation

The adjunction unit, viewed as the second map of the descent equalizer.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def right :
    (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj D.A ⟶
      (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj
        ((ModuleCat.extendScalars
          (algebraMap R (MaximalAdicModuleCover R))).obj
            ((ModuleCat.restrictScalars
              (algebraMap R (MaximalAdicModuleCover R))).obj D.A))

abbrev

Sections

L171 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.Sections

Documentation

The descended R-module, written as the usual degree-zero equalizer.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

abbrev Sections

def

sectionsFork

L175 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.sectionsFork

Documentation

The explicit equalizer fork defining Sections.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def sectionsFork : Fork (D.left (R := R)) (D.right (R := R))

def

sectionsForkIsLimit

L181 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.sectionsForkIsLimit

Documentation

The explicit Sections fork has the universal property of an equalizer.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def sectionsForkIsLimit : IsLimit (D.sectionsFork (R := R))

def

sectionsIsoComparisonEqualizer

L198 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.sectionsIsoComparisonEqualizer

Documentation

The explicit linear equalizer agrees with the categorical equalizer used by Beck's comparison adjunction.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def sectionsIsoComparisonEqualizer :
    ModuleCat.of R D.Sections ≅
      Comonad.ComonadicityInternal.comparisonRightAdjointObj
        (MaximalAdicModuleCoverAdjunction R) D

def

coverBaseChangeIso

L208 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.coverBaseChangeIso

Documentation

Base change of the explicit descended sections to the full product cover recovers the carrier of the descent datum.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def coverBaseChangeIso :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCover R))).obj
        (ModuleCat.of R D.Sections) ≅ D.A

abbrev

completionChart

L228 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.completionChart

Documentation

The completion chart cut out from the product-cover module.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

abbrev completionChart :
    ModuleCat (MaximalAdicModuleCoverCompletion R)

abbrev

principalChart

L234 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.principalChart

Documentation

A principal chart cut out from the product-cover module.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

abbrev principalChart (i : MaximalAdicModuleCoverGeneratorIndex R) :
    ModuleCat (MaximalAdicModuleCoverLocalization R i)

def

completionBaseChangeIso

L241 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.completionBaseChangeIso

Documentation

Base change of descended sections to the completion recovers the completion chart of the descent datum.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def completionBaseChangeIso :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCoverCompletion R))).obj
        (ModuleCat.of R D.Sections) ≅ D.completionChart (R := R)

def

principalBaseChangeIso

L256 ↗

EtaleFundamentalGroups.MaximalAdicModuleCoverDescentDatum.principalBaseChangeIso

Documentation

Base change of descended sections to a principal localization recovers that principal chart of the descent datum.

Source context 11 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace MaximalAdicModuleCoverDescentDatum
variable (D : MaximalAdicModuleCoverDescentDatum R)
local instance : Module R D.A :=
  Module.compHom D.A (algebraMap R (MaximalAdicModuleCover R))

Lean source · statement

def principalBaseChangeIso
    (i : MaximalAdicModuleCoverGeneratorIndex R) :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCoverLocalization R i))).obj
        (ModuleCat.of R D.Sections) ≅ D.principalChart (R := R) i

def

eqLocusCongr

L272 ↗

EtaleFundamentalGroups.eqLocusCongr

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · full declaration

def eqLocusCongr
    {A B A' B' : Type u}
    [AddCommGroup A] [AddCommGroup B] [AddCommGroup A'] [AddCommGroup B']
    [Module R A] [Module R B] [Module R A'] [Module R B']
    (l r : A →ₗ[R] B) (l' r' : A' →ₗ[R] B')
    (eA : A ≃ₗ[R] A') (eB : B ≃ₗ[R] B')
    (hl : eB.toLinearMap.comp l = l'.comp eA.toLinearMap)
    (hr : eB.toLinearMap.comp r = r'.comp eA.toLinearMap) :
    LinearMap.eqLocus l r ≃ₗ[R] LinearMap.eqLocus l' r' where
  toFun x := ⟨eA x, by
    have hlx := (LinearMap.ext_iff.mp hl) x.1
    have hrx := (LinearMap.ext_iff.mp hr) x.1
    change eB (l x.1) = l' (eA x.1) at hlx
    change eB (r x.1) = r' (eA x.1) at hrx
    exact hlx.symm.trans ((congrArg eB x.2).trans hrx)⟩
  invFun x := ⟨eA.symm x, by
    apply eB.injective
    have hlx := (LinearMap.ext_iff.mp hl) (eA.symm x.1)
    have hrx := (LinearMap.ext_iff.mp hr) (eA.symm x.1)
    change eB (l (eA.symm x.1)) = l' (eA (eA.symm x.1)) at hlx
    change eB (r (eA.symm x.1)) = r' (eA (eA.symm x.1)) at hrx
    calc
      eB (l (eA.symm x.1)) = l' (eA (eA.symm x.1)) := hlx
      _ = l' x.1 := by rw [eA.apply_symm_apply]
      _ = r' x.1 := x.2
      _ = r' (eA (eA.symm x.1)) := by rw [eA.apply_symm_apply]
      _ = eB (r (eA.symm x.1)) := hrx.symm⟩
  left_inv x := by ext; simp
  right_inv x := by ext; simp
  map_add' x y := by ext; simp
  map_smul' r x := by ext; simp

structure

FullCoverDescent

L312 ↗

EtaleFundamentalGroups.ModuleFormalGluingDatum.FullCoverDescent

Documentation

Evidence that an abstract formal-gluing equalizer is the degree-zero diagram of a genuine descent coalgebra on the full completion/principal product cover.

The fields identify source and overlap diagrams and record compatibility of their two arrows. In particular, this structure does not assume any base-change statement about D.Sections; those isomorphisms are consequences below.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]

Lean source · full declaration

structure ModuleFormalGluingDatum.FullCoverDescent
    (D : ModuleFormalGluingDatum R
      (MaximalAdicModuleCoverGeneratorIndex R)) where
  /-- The module descent coalgebra on the full product cover. -/
  descent : MaximalAdicModuleCoverDescentDatum R
  /-- Identification of the degree-zero sources of the two diagrams. -/
  sourceEquiv :
    D.Source ≃ₗ[R]
      (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj descent.A
  /-- Identification of the overlap targets of the two diagrams. -/
  targetEquiv :
    D.Target ≃ₗ[R]
      (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCover R))).obj
          ((ModuleCat.extendScalars
            (algebraMap R (MaximalAdicModuleCover R))).obj
              ((ModuleCat.restrictScalars
                (algebraMap R (MaximalAdicModuleCover R))).obj descent.A))
  /-- The source and target identifications commute with the first diagram map. -/
  left_compatibility :
    targetEquiv.toLinearMap.comp D.left =
      (descent.left (R := R)).hom.comp sourceEquiv.toLinearMap
  /-- The source and target identifications commute with the second diagram map. -/
  right_compatibility :
    targetEquiv.toLinearMap.comp D.right =
      (descent.right (R := R)).hom.comp sourceEquiv.toLinearMap
  /-- The descended completion chart agrees with the specified completion module. -/
  completion_identification :
    (ModuleCat.restrictScalars
      (algebraMap R (MaximalAdicModuleCoverCompletion R))).obj
        (descent.completionChart (R := R)) ≅ D.completion
  /-- Each descended principal chart agrees with the specified principal module. -/
  principal_identification :
    (i : MaximalAdicModuleCoverGeneratorIndex R) →
      (ModuleCat.restrictScalars
        (algebraMap R (MaximalAdicModuleCoverLocalization R i))).obj
          (descent.principalChart (R := R) i) ≅ D.principal i

def

sectionsEquiv

L358 ↗

EtaleFundamentalGroups.ModuleFormalGluingDatum.FullCoverDescent.sectionsEquiv

Documentation

Diagram compatibility identifies formal-gluing sections with the explicit equalizer of the full cover descent coalgebra.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace ModuleFormalGluingDatum.FullCoverDescent
variable {D : ModuleFormalGluingDatum R
  (MaximalAdicModuleCoverGeneratorIndex R)}

Lean source · statement

def sectionsEquiv (V : D.FullCoverDescent (R := R)) :
    D.Sections ≃ₗ[R] V.descent.Sections

def

coverBaseChangeIso

L367 ↗

EtaleFundamentalGroups.ModuleFormalGluingDatum.FullCoverDescent.coverBaseChangeIso

Documentation

Base change of the formal-gluing Sections to the full product cover recovers the full cover module.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace ModuleFormalGluingDatum.FullCoverDescent
variable {D : ModuleFormalGluingDatum R
  (MaximalAdicModuleCoverGeneratorIndex R)}

Lean source · statement

def coverBaseChangeIso (V : D.FullCoverDescent (R := R)) :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCover R))).obj
        (ModuleCat.of R D.Sections) ≅ V.descent.A

def

completionBaseChangeIso

L378 ↗

EtaleFundamentalGroups.ModuleFormalGluingDatum.FullCoverDescent.completionBaseChangeIso

Documentation

Base change of the formal-gluing Sections recovers the typed completion chart associated to the full descent datum.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace ModuleFormalGluingDatum.FullCoverDescent
variable {D : ModuleFormalGluingDatum R
  (MaximalAdicModuleCoverGeneratorIndex R)}

Lean source · statement

def completionBaseChangeIso
    (V : D.FullCoverDescent (R := R)) :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCoverCompletion R))).obj
        (ModuleCat.of R D.Sections) ≅
      V.descent.completionChart (R := R)

def

principalBaseChangeIso

L395 ↗

EtaleFundamentalGroups.ModuleFormalGluingDatum.FullCoverDescent.principalBaseChangeIso

Documentation

Base change of the formal-gluing Sections recovers each typed principal chart associated to the full descent datum.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open CategoryTheory CategoryTheory.Limits
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]
section Noetherian
variable [IsNoetherianRing R]
namespace ModuleFormalGluingDatum.FullCoverDescent
variable {D : ModuleFormalGluingDatum R
  (MaximalAdicModuleCoverGeneratorIndex R)}

Lean source · statement

def principalBaseChangeIso
    (V : D.FullCoverDescent (R := R))
    (i : MaximalAdicModuleCoverGeneratorIndex R) :
    (ModuleCat.extendScalars
      (algebraMap R (MaximalAdicModuleCoverLocalization R i))).obj
        (ModuleCat.of R D.Sections) ≅
      V.descent.principalChart (R := R) i

Module documentation

Faithfully flat descent for the maximal-adic module cover

Declarations