NYLL
Module

InverseLimitFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFundamentalGroup
9 declarations indexed from sourceView source ↗

Module documentation

The original fundamental-group maps in the pullback inverse system

The canonical pullback-fiber isomorphisms identify stage automorphisms with the original geometric-point fundamental groups. The intertwining equation retains the given scheme transition and the cone-induced point equality.

Imports3
Imported by2

Declarations

theorem

conjAut_autHomOfCompIso

L29 ↗
CategoryTheory.PreGaloisCategory.conjAut_autHomOfCompIso
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace CategoryTheory.PreGaloisCategory
universe u₀ v₀ u₁ v₁ w
Lean source · statement
theorem conjAut_autHomOfCompIso
    {C₀ : Type u₀} [Category.{v₀} C₀] {C₁ : Type u₁} [Category.{v₁} C₁]
    (H : C₀ ⥤ C₁) {F₀ G₀ : C₀ ⥤ FintypeCat.{w}}
    {F₁ G₁ : C₁ ⥤ FintypeCat.{w}}
    (r : H ⋙ F₁ ≅ F₀) (e₀ : F₀ ≅ G₀) (e₁ : F₁ ≅ G₁)
    (t : H ⋙ G₁ ≅ G₀) (h : r ≪≫ e₀ = isoWhiskerLeft H e₁ ≪≫ t)
    (a : Aut F₁) :
    e₀.conjAut (autHomOfCompIso H r a) =
      autHomOfCompIso H t (e₁.conjAut a)
theorem

fundamentalGroupHom_transport

L63 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_transport
Documentation

Transport of the target geometric point preserves the original fundamental-group homomorphism and its canonical pullback comparison.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
Lean source · statement
theorem fundamentalGroupHom_transport
    {X Y : Scheme.{u}} {Ω : Type u} [Field Ω]
    (f : X ⟶ Y) (point : Spec (.of Ω) ⟶ X) (eta : Spec (.of Ω) ⟶ Y)
    (h : point ≫ f = eta) (a : π₁ᵉᵗ(point)) :
    autHomOfCompIso (pullback f)
        (pullbackFiberIso f point ≪≫ eqToIso (congrArg fiber h)) a =
      h ▸ fundamentalGroupHom f point a
def

stagePoint

L82 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stagePoint
Documentation

The prescribed point on the original stage.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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 stagePoint (i : I) : Spec (.of Ω) ⟶ D.obj (Opposite.op i)
theorem

stagePoint_comp

L86 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stagePoint_comp
Documentation

The point compatibility is exactly the cone equation.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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
theorem stagePoint_comp {i j : I} (hij : i ≤ j) :
    stagePoint D s point j ≫ transitionMap D hij = stagePoint D s point i
def

stageFiberIso

L92 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stageFiberIso
Documentation

The original pullback-fiber comparison at a cone leg.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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 stageFiberIso (i : I) :
    toLimit D s i ⋙ fiber point ≅ fiber (stagePoint D s point i)
def

pointedTransitionIso

L98 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.pointedTransitionIso
Documentation

The canonical fiber comparison of the original transition, with its cone-induced equality of geometric points.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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 pointedTransitionIso {i j : I} (hij : i ≤ j) :
    transition D hij ⋙ fiber (stagePoint D s point j) ≅
      fiber (stagePoint D s point i)
theorem

stageFiberIso_coherence

L105 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stageFiberIso_coherence
Documentation

The point comparisons commute with the actual pullback cone comparison.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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
theorem stageFiberIso_coherence {i j : I} (hij : i ≤ j) :
    isoWhiskerRight (comparison D s hij) (fiber point) ≪≫
      associator (transition D hij) (toLimit D s j) (fiber point) ≪≫
      isoWhiskerLeft (transition D hij) (stageFiberIso D s point j) ≪≫
      pointedTransitionIso D s point hij = stageFiberIso D s point i
theorem

stageAutRestriction_eq_fundamentalGroupHom

L116 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stageAutRestriction_eq_fundamentalGroupHom
Documentation

Under the actual fiber comparisons, restriction is the original fundamental-group homomorphism with the original point transport.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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
theorem stageAutRestriction_eq_fundamentalGroupHom {i j : I} (hij : i ≤ j)
    (a : Aut (toLimit D s j ⋙ fiber point)) :
    (stageFiberIso D s point i).conjAut
        (stageAutRestriction (stage D) (toLimit D s) (transition D) (comparison D s)
          (fiber point) hij a) =
      stagePoint_comp D s point hij ▸
        fundamentalGroupHom (transitionMap D hij) (stagePoint D s point j)
          ((stageFiberIso D s point j).conjAut a)
theorem

globalAutRestriction_eq_fundamentalGroupHom

L145 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.globalAutRestriction_eq_fundamentalGroupHom
Documentation

Global restriction followed by the canonical stage comparison is exactly the original fundamental-group map of that cone leg.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Functor CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
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
theorem globalAutRestriction_eq_fundamentalGroupHom (i : I) (a : π₁ᵉᵗ(point)) :
    (stageFiberIso D s point i).conjAut
        (globalAutRestriction (stage D) (toLimit D s) (fiber point) i a) =
      fundamentalGroupHom (s.π.app (Opposite.op i)) point a

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