Module

PullbackFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackFundamentalGroup

3 declarations indexed from sourceView source ↗

Module documentation

Fundamental groups of pointed pullbacks

A point in the geometric fiber of a finite étale cover determines a lift of the geometric point to every pullback of that cover. The fundamental group at this lifted point is the inverse image of the original point stabilizer under the homomorphism on étale fundamental groups.

Imports2

Imported by2

def

pullbackLiftOfFiberPoint

L33 ↗

AlgebraicGeometry.FiniteEtale.pullbackLiftOfFiberPoint

Documentation

The lift to the pullback of a finite étale cover determined by a point in the original geometric fiber.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X Y : Scheme.{u}}
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

def pullbackLiftOfFiberPoint
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (x : (fiber (xi ≫ f)).obj A) :
    Spec (.of Omega) ⟶ ((pullback f).obj A).left

theorem

pullbackLiftOfFiberPoint_comp

L44 ↗

AlgebraicGeometry.FiniteEtale.pullbackLiftOfFiberPoint_comp

Documentation

The lift determined by a fiber point lies over the chosen geometric point.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X Y : Scheme.{u}}
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem pullbackLiftOfFiberPoint_comp
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (x : (fiber (xi ≫ f)).obj A) :
    pullbackLiftOfFiberPoint f xi A x ≫ ((pullback f).obj A).hom = xi

def

fundamentalGroupEquivComapStabilizerOfPullback

L54 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivComapStabilizerOfPullback

Documentation

The fundamental group at the lift of a point to a pulled-back finite étale cover is the inverse image of the original point stabilizer.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X Y : Scheme.{u}}
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

def fundamentalGroupEquivComapStabilizerOfPullback
    [ConnectedSpace X]
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (A : FiniteEtale Y) (x : (fiber (xi ≫ f)).obj A) :
    π₁ᵉᵗ(pullbackLiftOfFiberPoint f xi A x) ≃ₜ*
      (MulAction.stabilizer π₁ᵉᵗ(xi ≫ f) x).comap
        (fundamentalGroupHom f xi).toMonoidHom

Module documentation

Fundamental groups of pointed pullbacks

Declarations

pullbackLiftOfFiberPoint

pullbackLiftOfFiberPoint_comp

fundamentalGroupEquivComapStabilizerOfPullback