Module

InverseLimitDiagram.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitDiagram

15 declarations indexed from sourceView source ↗

Module documentation

The actual finite étale pullback diagram of an inverse system

The functors and cone maps are the canonical scheme pullbacks. Their unit and composition coherence is proved from the projection-based pullback coherence theorems, including all equalities of the original diagram's scheme maps.

Imports5

Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismInverseLimit
Nyll.EtaleFundamentalGroups.GeometricFiber.PointedComposition
Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackIdentity
Nyll.SchemeTheory.FiniteEtale.InverseLimitHom
Mathlib.CategoryTheory.Category.Preorder

Imported by3

theorem

pullbackCone_identity

L33 ↗

AlgebraicGeometry.FiniteEtale.pullbackCone_identity

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem pullbackCone_identity
    {X Y : Scheme.{u}} (p : X ⟶ Y) (f : Y ⟶ Y)
    (hf : f = 𝟙 Y) (hp : p = p ≫ f) :
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) p f p hp ≪≫
      Functor.isoWhiskerRight
        (eqToIso (congrArg pullback hf) ≪≫ pullbackIdIso Y) (pullback p) ≪≫
      Functor.leftUnitor (pullback p) = Iso.refl (pullback p)

theorem

pullbackCone_composition

L44 ↗

AlgebraicGeometry.FiniteEtale.pullbackCone_composition

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem pullbackCone_composition
    {L X Y Z : Scheme.{u}} (p : L ⟶ X) (q : L ⟶ Y) (r : L ⟶ Z)
    (f : Y ⟶ X) (g : Z ⟶ Y) (h : Z ⟶ X)
    (hp : p = q ≫ f) (hq : q = r ≫ g) (hh : h = g ≫ f)
    (hpr : p = r ≫ h) :
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) r h p hpr ≪≫
      Functor.isoWhiskerRight
        (MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) g f h hh) (pullback r) ≪≫
      Functor.associator (pullback f) (pullback g) (pullback r) =
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) q f p hp ≪≫
      Functor.isoWhiskerLeft (pullback f)
        (MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) r g q hq)

def

transitionMap

L92 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.transitionMap

Documentation

The original scheme transition associated to a comparison of indices.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def transitionMap {i j : I} (hij : i ≤ j) :
    D.obj (Opposite.op j) ⟶ D.obj (Opposite.op i)

theorem

transitionMap_id

L97 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.transitionMap_id

Documentation

Identity transitions use the identity scheme map.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

theorem transitionMap_id (i : I) :
    transitionMap D (le_rfl : i ≤ i) = 𝟙 (D.obj (Opposite.op i))

theorem

transitionMap_comp

L102 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.transitionMap_comp

Documentation

The transition maps are the maps of the given functor, with its composition law.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

theorem transitionMap_comp {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) :
    transitionMap D (hij.trans hjk) = transitionMap D hjk ≫ transitionMap D hij

abbrev

stage

L107 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stage

Documentation

The category of finite étale covers at the original stage.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

abbrev stage (i : I)

def

toLimit

L110 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.toLimit

Documentation

The actual pullback functor from a stage to the cone point.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def toLimit (i : I) : stage D i ⥤ FiniteEtale s.pt

def

transition

L114 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.transition

Documentation

The actual refinement functor between stage categories.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def transition {i j : I} (hij : i ≤ j) : stage D i ⥤ stage D j

def

comparison

L118 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.comparison

Documentation

The cone comparison is precisely the existing scheme pullback comparison.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def comparison {i j : I} (hij : i ≤ j) :
    toLimit D s i ≅ transition D hij ⋙ toLimit D s j

def

unitIso

L123 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.unitIso

Documentation

The actual unit comparison, including the original functor's map-id equality.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def unitIso (i : I) : transition D (le_rfl : i ≤ i) ≅ 𝟭 (stage D i)

def

compositionIso

L128 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.compositionIso

Documentation

The actual composition comparison, including the original map-comp equality.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

def compositionIso {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) :
    transition D (hij.trans hjk) ≅ transition D hij ⋙ transition D hjk

theorem

comparison_identity

L136 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.comparison_identity

Documentation

Unit coherence of the supplied functor diagram is a theorem of actual pullbacks.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

theorem comparison_identity (i : I) :
    comparison D s (le_rfl : i ≤ i) ≪≫
      Functor.isoWhiskerRight (unitIso D i) (toLimit D s i) ≪≫
      Functor.leftUnitor (toLimit D s i) = Iso.refl (toLimit D s i)

theorem

comparison_composition

L145 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.comparison_composition

Documentation

Composition coherence of the supplied cone is proved, not assumed.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)

Lean source · statement

theorem comparison_composition {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) :
    comparison D s (hij.trans hjk) ≪≫
      Functor.isoWhiskerRight (compositionIso D hij hjk) (toLimit D s k) ≪≫
      Functor.associator (transition D hij) (transition D hjk) (toLimit D s k) =
    comparison D s hij ≪≫ Functor.isoWhiskerLeft (transition D hij) (comparison D s hjk)

abbrev

pullbackAutSystem

L159 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.pullbackAutSystem

Documentation

The generic automorphism system instantiated with the actual scheme pullbacks.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)

Lean source · statement

abbrev pullbackAutSystem : ProCGroups.InverseSystems.InverseSystem (I := I)

def

pullbackAutComparison

L165 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.pullbackAutComparison

Documentation

The actual comparison into the stage-pullback automorphism system.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
namespace InverseLimitDiagram
variable {I : Type u} [Preorder I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D)
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)

Lean source · statement

def pullbackAutComparison : π₁ᵉᵗ(point) →ₜ* (pullbackAutSystem D s point).inverseLimit

Module documentation

The actual finite étale pullback diagram of an inverse system

Declarations