Module

InverseLimitComparison.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitComparison

4 declarations indexed from sourceView source ↗

Module documentation

Fundamental groups of the original qcqs inverse limit

Actual finite étale object and morphism descent supply the two inputs to automorphism assembly. The resulting bijection is the already-constructed comparison whose coordinates are the original fundamental-group maps. Compactness upgrades that same comparison to a topological group isomorphism.

Imports4

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.All

theorem

fundamentalGroupComparison_bijective

L39 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupComparison_bijective

Documentation

The canonical comparison for the original geometric data is bijective. Both categorical descent inputs are supplied by actual scheme theorems.

Source context 11 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
variable {I : Type u} [Preorder I] [IsDirectedOrder I] [Nonempty I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D) (hs : IsLimit s)
variable [∀ {i j : Iᵒᵖ} (h : i ⟶ j), IsAffineHom (D.map h)]
variable [∀ i : Iᵒᵖ, CompactSpace (D.obj i)]
variable [∀ i : Iᵒᵖ, QuasiSeparatedSpace (D.obj i)]
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)
include hs in

Lean source · statement

theorem fundamentalGroupComparison_bijective :
    Function.Bijective (fundamentalGroupComparison D s point)

def

fundamentalGroupInverseLimitEquiv

L58 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupInverseLimitEquiv

Documentation

The original fundamental group is canonically the inverse limit of the original stage fundamental groups, with their canonical topologies.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
variable {I : Type u} [Preorder I] [IsDirectedOrder I] [Nonempty I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D) (hs : IsLimit s)
variable [∀ {i j : Iᵒᵖ} (h : i ⟶ j), IsAffineHom (D.map h)]
variable [∀ i : Iᵒᵖ, CompactSpace (D.obj i)]
variable [∀ i : Iᵒᵖ, QuasiSeparatedSpace (D.obj i)]
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)

Lean source · statement

def fundamentalGroupInverseLimitEquiv :
    π₁ᵉᵗ(point) ≃ₜ* (fundamentalGroupSystem D s point).inverseLimit

theorem

fundamentalGroupInverseLimitEquiv_apply

L66 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupInverseLimitEquiv_apply

Documentation

The equivalence uses the previously constructed canonical forward map.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
variable {I : Type u} [Preorder I] [IsDirectedOrder I] [Nonempty I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D) (hs : IsLimit s)
variable [∀ {i j : Iᵒᵖ} (h : i ⟶ j), IsAffineHom (D.map h)]
variable [∀ i : Iᵒᵖ, CompactSpace (D.obj i)]
variable [∀ i : Iᵒᵖ, QuasiSeparatedSpace (D.obj i)]
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)

Lean source · statement

theorem fundamentalGroupInverseLimitEquiv_apply (a : π₁ᵉᵗ(point)) :
    fundamentalGroupInverseLimitEquiv D s hs point a =
      fundamentalGroupComparison D s point a

theorem

fundamentalGroupInverseLimitEquiv_projection

L76 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitDiagram.fundamentalGroupInverseLimitEquiv_projection

Documentation

The canonical equivalence retains the original cone projection maps on fundamental groups, without a choice of an alternative system or comparison.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale.InverseLimitDiagram
universe u
variable {I : Type u} [Preorder I] [IsDirectedOrder I] [Nonempty I]
variable (D : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone D) (hs : IsLimit s)
variable [∀ {i j : Iᵒᵖ} (h : i ⟶ j), IsAffineHom (D.map h)]
variable [∀ i : Iᵒᵖ, CompactSpace (D.obj i)]
variable [∀ i : Iᵒᵖ, QuasiSeparatedSpace (D.obj i)]
variable {Ω : Type u} [Field Ω] (point : Spec (.of Ω) ⟶ s.pt)

Lean source · statement

theorem fundamentalGroupInverseLimitEquiv_projection (i : I) (a : π₁ᵉᵗ(point)) :
    (fundamentalGroupSystem D s point).projection i
        (fundamentalGroupInverseLimitEquiv D s hs point a) =
      fundamentalGroupHom (s.π.app (Opposite.op i)) point a

Module documentation

Fundamental groups of the original qcqs inverse limit

Declarations

fundamentalGroupComparison_bijective

fundamentalGroupInverseLimitEquiv

fundamentalGroupInverseLimitEquiv_apply

fundamentalGroupInverseLimitEquiv_projection