Module

DeckFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.DeckFundamentalGroup

5 declarations indexed from sourceView source ↗

Module documentation

Actual geometric deck maps and subgroup conjugation

The deck pullback here is the scheme-theoretic pullback functor. Its pointed fiber comparison is obtained from the actual over-category comparison and ambient monodromy. Under the canonical inclusion of the covering fundamental group, the induced automorphism is ambient conjugation.

Imports3

Imported by4

instance

baseFiberFunctor

L31 ↗

AlgebraicGeometry.FiniteEtale.baseFiberFunctor

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)

Lean source · statement

instance baseFiberFunctor : FiberFunctor (fiber (xi ≫ A.hom))

def

deckPointedGeometricFiberIso

L40 ↗

AlgebraicGeometry.FiniteEtale.deckPointedGeometricFiberIso

Documentation

A fiber comparison for the actual geometric pullback along a deck automorphism, pointed by its lift in the ambient fundamental group.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor : FiberFunctor (fiber (xi ≫ A.hom)) :=
  fiberFunctor (X := S) (xi ≫ A.hom)
variable (σ : Aut A) (g : π₁ᵉᵗ(xi ≫ A.hom))
variable (h : (fiber (xi ≫ A.hom)).map σ.hom (liftedFiberPoint A xi) =
  g • liftedFiberPoint A xi)

Lean source · statement

def deckPointedGeometricFiberIso :
    pullback σ.hom.left ⋙ fiber xi ≅ fiber xi

theorem

coverHom_autFiberOver

L48 ↗

AlgebraicGeometry.FiniteEtale.coverHom_autFiberOver

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor : FiberFunctor (fiber (xi ≫ A.hom)) :=
  fiberFunctor (X := S) (xi ≫ A.hom)
variable (σ : Aut A) (g : π₁ᵉᵗ(xi ≫ A.hom))
variable (h : (fiber (xi ≫ A.hom)).map σ.hom (liftedFiberPoint A xi) =
  g • liftedFiberPoint A xi)

Lean source · statement

theorem coverHom_autFiberOver (b : Aut
    (fiberOver (fiber (xi ≫ A.hom)) (liftedFiberPoint A xi))) :
    fundamentalGroupHom A.hom xi (autFiberOverEquivFiber A xi b) =
      extendFiberOverAut (fiber (xi ≫ A.hom)) (liftedFiberPoint A xi) b

theorem

fundamentalGroupHom_deckPointed

L59 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_deckPointed

Documentation

The actual deck pullback induces conjugation on the actual covering fundamental group, after its canonical inclusion in the base group.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor : FiberFunctor (fiber (xi ≫ A.hom)) :=
  fiberFunctor (X := S) (xi ≫ A.hom)
variable (σ : Aut A) (g : π₁ᵉᵗ(xi ≫ A.hom))
variable (h : (fiber (xi ≫ A.hom)).map σ.hom (liftedFiberPoint A xi) =
  g • liftedFiberPoint A xi)

Lean source · statement

theorem fundamentalGroupHom_deckPointed
    (a : π₁ᵉᵗ(xi)) :
    fundamentalGroupHom A.hom xi
        (autHomOfCompIso (pullback σ.hom.left)
          (deckPointedGeometricFiberIso A xi σ g h) a) =
      g⁻¹ * fundamentalGroupHom A.hom xi a * g

theorem

deckPointed_eq_self_of_centralizes

L88 ↗

AlgebraicGeometry.FiniteEtale.deckPointed_eq_self_of_centralizes

Documentation

An ambient element centralizing the covering subgroup induces the identity on the actual pointed fundamental group under its geometric deck comparison.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor : FiberFunctor (fiber (xi ≫ A.hom)) :=
  fiberFunctor (X := S) (xi ≫ A.hom)
variable (σ : Aut A) (g : π₁ᵉᵗ(xi ≫ A.hom))
variable (h : (fiber (xi ≫ A.hom)).map σ.hom (liftedFiberPoint A xi) =
  g • liftedFiberPoint A xi)

Lean source · statement

theorem deckPointed_eq_self_of_centralizes
    (hc : ∀ a : π₁ᵉᵗ(xi), Commute g (fundamentalGroupHom A.hom xi a))
    (a : π₁ᵉᵗ(xi)) :
    autHomOfCompIso (pullback σ.hom.left)
      (deckPointedGeometricFiberIso A xi σ g h) a = a

Module documentation

Actual geometric deck maps and subgroup conjugation

Declarations

baseFiberFunctor

deckPointedGeometricFiberIso

coverHom_autFiberOver

fundamentalGroupHom_deckPointed

deckPointed_eq_self_of_centralizes