Module

BasePoint.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.BasePoint

5 declarations indexed from sourceView source ↗

Module documentation

Base points and functoriality of the étale fundamental group

The geometric fiber functors at any two geometric points of a connected scheme are isomorphic. Each such isomorphism identifies their fundamental groups as topological groups and compares their finite-action equivalences. The identification is independent of the comparison up to inner conjugation. Pullback of finite étale schemes agrees with restriction of finite continuous actions along the canonical fundamental-group homomorphism.

Imports3

Imported by13

theorem

nonempty_fiber_iso

L38 ↗

AlgebraicGeometry.FiniteEtale.nonempty_fiber_iso

Documentation

The geometric fiber functors at any two geometric points are isomorphic.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω Ω' : Type u} [Field Ω] [Field Ω'] [IsSepClosed Ω] [IsSepClosed Ω']
  (ξ : Spec (.of Ω) ⟶ X) (ξ' : Spec (.of Ω') ⟶ X)

Lean source · statement

theorem nonempty_fiber_iso : Nonempty (fiber ξ ≅ fiber ξ')

def

fundamentalGroupIsoOfFiberIso

L43 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupIsoOfFiberIso

Documentation

A comparison of geometric fiber functors induces a topological group isomorphism.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω Ω' : Type u} [Field Ω] [Field Ω'] [IsSepClosed Ω] [IsSepClosed Ω']
  (ξ : Spec (.of Ω) ⟶ X) (ξ' : Spec (.of Ω') ⟶ X)

Lean source · statement

def fundamentalGroupIsoOfFiberIso (t : fiber ξ ≅ fiber ξ') :
    π₁ᵉᵗ(ξ) ≃ₜ* π₁ᵉᵗ(ξ')

theorem

fundamentalGroupIsoOfFiberIso_eq_conj

L51 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupIsoOfFiberIso_eq_conj

Documentation

Different comparisons give fundamental-group isomorphisms differing by an explicit inner automorphism of the target fundamental group.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω Ω' : Type u} [Field Ω] [Field Ω'] [IsSepClosed Ω] [IsSepClosed Ω']
  (ξ : Spec (.of Ω) ⟶ X) (ξ' : Spec (.of Ω') ⟶ X)
omit [ConnectedSpace X] [IsSepClosed Ω] [IsSepClosed Ω'] in

Lean source · statement

theorem fundamentalGroupIsoOfFiberIso_eq_conj
    (t₁ t₂ : fiber ξ ≅ fiber ξ') (a : π₁ᵉᵗ(ξ)) :
    fundamentalGroupIsoOfFiberIso ξ ξ' t₂ a =
      MulAut.conj (G := π₁ᵉᵗ(ξ')) (t₁.symm ≪≫ t₂)
        (fundamentalGroupIsoOfFiberIso ξ ξ' t₁ a)

def

basePointContActionIso

L60 ↗

AlgebraicGeometry.FiniteEtale.basePointContActionIso

Documentation

Base-point change commutes with the equivalences to finite continuous actions.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω Ω' : Type u} [Field Ω] [Field Ω'] [IsSepClosed Ω] [IsSepClosed Ω']
  (ξ : Spec (.of Ω) ⟶ X) (ξ' : Spec (.of Ω') ⟶ X)

Lean source · statement

def basePointContActionIso (t : fiber ξ ≅ fiber ξ') :
    functorToContAction (fiber ξ) ≅ functorToContAction (fiber ξ') ⋙
      (ContAction.resEquiv FintypeCat (fundamentalGroupIsoOfFiberIso ξ ξ' t)).functor

def

pullbackContActionIso

L70 ↗

AlgebraicGeometry.FiniteEtale.pullbackContActionIso

Documentation

Pullback of finite étale covers agrees with restriction of actions along the canonical continuous map on étale fundamental groups.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω Ω' : Type u} [Field Ω] [Field Ω'] [IsSepClosed Ω] [IsSepClosed Ω']
  (ξ : Spec (.of Ω) ⟶ X) (ξ' : Spec (.of Ω') ⟶ X)
variable {Y : Scheme.{u}} [ConnectedSpace Y]

Lean source · statement

def pullbackContActionIso (f : X ⟶ Y) (ξ : Spec (.of Ω) ⟶ X) :
    pullback f ⋙ functorToContAction (fiber ξ) ≅
      functorToContAction (fiber (ξ ≫ f)) ⋙
        ContAction.res FintypeCat (fundamentalGroupHom f ξ)

Module documentation

Base points and functoriality of the étale fundamental group

Declarations

nonempty_fiber_iso

fundamentalGroupIsoOfFiberIso

fundamentalGroupIsoOfFiberIso_eq_conj

basePointContActionIso

pullbackContActionIso