NYLL
Module

InverseLimitFundamentalGroupSystem.lean

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

Module documentation

The canonical inverse system of original geometric fundamental groups

This is the stagewise transport of the actual pullback automorphism system. Both the transition maps and the forward comparison coordinates are proved equal to the existing fundamental-group homomorphisms.

Imports1
Imported by2

Declarations

def

stageEquiv

L32 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stageEquiv
Documentation

The actual pullback-fiber comparison is an isomorphism of the canonical topological automorphism groups.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 stageEquiv (i : I) :
    Aut (toLimit D s i ⋙ fiber point) ≃ₜ* π₁ᵉᵗ(stagePoint D s point i)
theorem

stageEquiv_apply

L40 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.stageEquiv_apply
Documentation

The stage equivalence uses the canonical conjugation formula.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 stageEquiv_apply (i : I) (a : Aut (toLimit D s i ⋙ fiber point)) :
    stageEquiv D s point i a = (stageFiberIso D s point i).conjAut a
def

fundamentalGroupTransition

L49 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupTransition
Documentation

The original stage transition, expressed through the canonical fiber comparisons so that its topology and group structure are retained.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 · full declaration
def fundamentalGroupTransition {i j : I} (hij : i ≤ j) :
    π₁ᵉᵗ(stagePoint D s point j) →ₜ* π₁ᵉᵗ(stagePoint D s point i) where
  toMonoidHom := (stageEquiv D s point i).toMulEquiv.toMonoidHom.comp
    ((stageAutRestriction (stage D) (toLimit D s) (transition D) (comparison D s)
      (fiber point) hij).toMonoidHom.comp
      (stageEquiv D s point j).symm.toMulEquiv.toMonoidHom)
  continuous_toFun := (stageEquiv D s point i).continuous_toFun.comp
    ((stageAutRestriction (stage D) (toLimit D s) (transition D) (comparison D s)
      (fiber point) hij).continuous_toFun.comp
      (stageEquiv D s point j).continuous_invFun)
theorem

fundamentalGroupTransition_apply

L62 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupTransition_apply
Documentation

The transported transition is exactly the original fundamental-group map along the given scheme transition, after the cone-induced point equality.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 fundamentalGroupTransition_apply {i j : I} (hij : i ≤ j)
    (a : π₁ᵉᵗ(stagePoint D s point j)) :
    fundamentalGroupTransition D s point hij a =
      stagePoint_comp D s point hij ▸
        fundamentalGroupHom (transitionMap D hij) (stagePoint D s point j) a
def

fundamentalGroupSystem

L73 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupSystem
Documentation

The single canonical system of original stage fundamental groups.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 · full declaration
def fundamentalGroupSystem : InverseSystem (I := I) where
  X i := π₁ᵉᵗ(stagePoint D s point i)
  topologicalSpace i := inferInstance
  map hij := fundamentalGroupTransition D s point hij
  continuous_map hij := (fundamentalGroupTransition D s point hij).continuous_toFun
  map_id i := by
    funext a
    change stageEquiv D s point i
      ((pullbackAutSystem D s point).map (le_rfl : i ≤ i)
        ((stageEquiv D s point i).symm a)) = a
    rw [(pullbackAutSystem D s point).map_id_apply,
      ContinuousMulEquiv.apply_symm_apply]
  map_comp {i j k} hij hjk := by
    funext a
    change stageEquiv D s point i
      ((pullbackAutSystem D s point).map hij
        ((stageEquiv D s point j).symm (stageEquiv D s point j
          ((pullbackAutSystem D s point).map hjk ((stageEquiv D s point k).symm a))))) =
      stageEquiv D s point i ((pullbackAutSystem D s point).map (hij.trans hjk)
        ((stageEquiv D s point k).symm a))
    rw [ContinuousMulEquiv.symm_apply_apply, (pullbackAutSystem D s point).map_comp_apply]
instance

fundamentalGroupSystem_isGroupSystem

L96 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupSystem_isGroupSystem
Documentation

The canonical system has the group laws carried by its continuous homomorphisms.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 · full declaration
instance fundamentalGroupSystem_isGroupSystem :
    IsGroupSystem (fundamentalGroupSystem D s point) where
  map_one hij := (fundamentalGroupTransition D s point hij).map_one
  map_mul hij a b := (fundamentalGroupTransition D s point hij).map_mul a b
  map_inv hij a := (fundamentalGroupTransition D s point hij).map_inv a
def

fundamentalGroupSystemIso

L103 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupSystemIso
Documentation

The stagewise identification uses the existing inverse-system-isomorphism API.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 · full declaration
def fundamentalGroupSystemIso : InverseSystem.InverseSystemIso
    (pullbackAutSystem D s point) (fundamentalGroupSystem D s point) where
  stageEquiv := stageEquiv D s point
  comm {i j} hij a := by
    change stageEquiv D s point i ((pullbackAutSystem D s point).map hij a) =
      stageEquiv D s point i ((pullbackAutSystem D s point).map hij
        ((stageEquiv D s point j).symm (stageEquiv D s point j a)))
    rw [ContinuousMulEquiv.symm_apply_apply]
def

fundamentalGroupComparison

L113 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupComparison
Documentation

The forward comparison into the original stage fundamental groups.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 fundamentalGroupComparison :
    π₁ᵉᵗ(point) →ₜ* (fundamentalGroupSystem D s point).inverseLimit
theorem

fundamentalGroupComparison_projection

L120 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupComparison_projection
Documentation

Every forward coordinate is the existing fundamental-group homomorphism of the original cone projection.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
open ProCGroups.InverseSystems
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
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 fundamentalGroupComparison_projection (i : I) (a : π₁ᵉᵗ(point)) :
    (fundamentalGroupSystem D s point).projection i (fundamentalGroupComparison D s point 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.