Module

PointedCover.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.PointedCover

34 declarations indexed from sourceView source ↗

Module documentation

Geometric fibers over a pointed finite étale cover

A finite étale scheme over the source of a finite étale cover is the same as a finite étale scheme over the base equipped with a map to that cover. Under this equivalence, the geometric fiber at a lifted point is the corresponding fiber-over-a-point functor. Consequently, its automorphism group is the stabilizer of the lifted point in the automorphism group over the base.

Imports2

Imported by7

abbrev

overBaseObj

L32 ↗

AlgebraicGeometry.FiniteEtale.overBaseObj

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · statement

abbrev overBaseObj (A : FiniteEtale S) (B : FiniteEtale A.left) :
    FiniteEtale S

abbrev

overBaseHom

L37 ↗

AlgebraicGeometry.FiniteEtale.overBaseHom

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · statement

abbrev overBaseHom (A : FiniteEtale S) (B : FiniteEtale A.left) :
    overBaseObj A B ⟶ A

abbrev

toOverObj

L41 ↗

AlgebraicGeometry.FiniteEtale.toOverObj

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · statement

abbrev toOverObj (A : FiniteEtale S) (B : FiniteEtale A.left) : Over A

abbrev

toOverMap

L44 ↗

AlgebraicGeometry.FiniteEtale.toOverMap

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · statement

abbrev toOverMap (A : FiniteEtale S) {B C : FiniteEtale A.left}
    (f : B ⟶ C) : toOverObj A B ⟶ toOverObj A C

def

toOver

L54 ↗

AlgebraicGeometry.FiniteEtale.toOver

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · full declaration

def toOver (A : FiniteEtale S) : FiniteEtale A.left ⥤ Over A where
  obj B := toOverObj A B
  map f := toOverMap A f
  map_id B := by
    apply Over.OverMorphism.ext
    apply MorphismProperty.Over.Hom.ext
    rfl
  map_comp f g := by
    apply Over.OverMorphism.ext
    apply MorphismProperty.Over.Hom.ext
    rfl

abbrev

toOverFaithful

L66 ↗

AlgebraicGeometry.FiniteEtale.toOverFaithful

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · full declaration

abbrev toOverFaithful (A : FiniteEtale S) : (toOver A).Faithful where
  map_injective {B C} f g h := by
    change toOverMap A f = toOverMap A g at h
    apply MorphismProperty.Over.Hom.ext
    exact congrArg (fun q ↦ q.left.left) h

abbrev

toOverFull

L72 ↗

AlgebraicGeometry.FiniteEtale.toOverFull

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · full declaration

abbrev toOverFull (A : FiniteEtale S) : (toOver A).Full where
  map_surjective {B C} f := by
    let g : B ⟶ C := MorphismProperty.Over.homMk f.left.left (by
      exact congrArg (fun q ↦ q.left) (Over.w f))
    refine ⟨g, ?_⟩
    change toOverMap A g = f
    apply Over.OverMorphism.ext
    apply MorphismProperty.Over.Hom.ext
    rfl

abbrev

toOverEssSurj

L82 ↗

AlgebraicGeometry.FiniteEtale.toOverEssSurj

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · full declaration

abbrev toOverEssSurj (A : FiniteEtale S) : (toOver A).EssSurj where
  mem_essImage U := by
    let B : FiniteEtale A.left := FiniteEtale.mk U.hom.left
    let eBase : overBaseObj A B ≅ U.left :=
      MorphismProperty.Over.isoMk (Iso.refl U.left.left) (by
        change (𝟙 U.left.left) ≫ U.left.hom = U.hom.left ≫ A.hom
        rw [Category.id_comp]
        exact (MorphismProperty.Over.w U.hom).symm)
    let e : toOverObj A B ≅ U := Over.isoMk eBase (by
      apply MorphismProperty.Over.Hom.ext
      rfl)
    change (toOver A).essImage U
    exact ⟨B, ⟨e⟩⟩

def

overEquiv

L98 ↗

AlgebraicGeometry.FiniteEtale.overEquiv

Documentation

Finite étale schemes over the source of A are equivalent to finite étale schemes over the base equipped with a map to A.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}}

Lean source · statement

def overEquiv (A : FiniteEtale S) :
    FiniteEtale A.left ≌ Over A

abbrev

basePoint

L108 ↗

AlgebraicGeometry.FiniteEtale.basePoint

Source context 8 commands

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

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

Lean source · statement

abbrev basePoint (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) : Spec (.of Omega) ⟶ S

abbrev

liftedPointHom

L112 ↗

AlgebraicGeometry.FiniteEtale.liftedPointHom

Source context 8 commands

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

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

Lean source · statement

abbrev liftedPointHom (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    Over.mk (basePoint A xi') ⟶ A.toComma

def

liftedFiberPoint

L119 ↗

AlgebraicGeometry.FiniteEtale.liftedFiberPoint

Documentation

The point of the geometric fiber of A determined by a lift of the base geometric point to the source of A.

Source context 8 commands

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

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

Lean source · statement

def liftedFiberPoint (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    (fiber (basePoint A xi')).obj A

def

liftedFiberPointOverComposite

L126 ↗

AlgebraicGeometry.FiniteEtale.liftedFiberPointOverComposite

Documentation

The point of the geometric fiber determined by a lift, with the base point displayed explicitly as the composite with the covering map.

Source context 8 commands

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

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

Lean source · statement

def liftedFiberPointOverComposite (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    (fiber (xi' ≫ A.hom)).obj A

def

sourcePointOfFiberOver

L131 ↗

AlgebraicGeometry.FiniteEtale.sourcePointOfFiberOver

Source context 8 commands

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

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

Lean source · statement

def sourcePointOfFiberOver
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    Over.mk xi' ⟶ B.toComma

def

fiberOverOfSourcePoint

L151 ↗

AlgebraicGeometry.FiniteEtale.fiberOverOfSourcePoint

Source context 8 commands

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

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

Lean source · statement

def fiberOverOfSourcePoint
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left) (z : Over.mk xi' ⟶ B.toComma) :
    (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)

theorem

sourcePointOfFiberOver_fiberOverOfSourcePoint

L180 ↗

AlgebraicGeometry.FiniteEtale.sourcePointOfFiberOver_fiberOverOfSourcePoint

Source context 8 commands

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

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

Lean source · statement

theorem sourcePointOfFiberOver_fiberOverOfSourcePoint
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left) (z : Over.mk xi' ⟶ B.toComma) :
    sourcePointOfFiberOver A xi' B (fiberOverOfSourcePoint A xi' B z) = z

theorem

fiberOverOfSourcePoint_sourcePointOfFiberOver

L188 ↗

AlgebraicGeometry.FiniteEtale.fiberOverOfSourcePoint_sourcePointOfFiberOver

Source context 8 commands

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

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

Lean source · statement

theorem fiberOverOfSourcePoint_sourcePointOfFiberOver
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    fiberOverOfSourcePoint A xi' B (sourcePointOfFiberOver A xi' B y) = y

def

fiberOverEquiv

L199 ↗

AlgebraicGeometry.FiniteEtale.fiberOverEquiv

Source context 8 commands

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

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

Lean source · full declaration

def fiberOverEquiv
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left) :
    (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
        (toOverObj A B) ≃
      (fiber xi').obj B where
  toFun y := (fiberObjEquivHom xi' B).symm (sourcePointOfFiberOver A xi' B y)
  invFun z := fiberOverOfSourcePoint A xi' B (fiberObjEquivHom xi' B z)
  left_inv y := by
    exact (congrArg (fiberOverOfSourcePoint A xi' B)
      (Equiv.apply_symm_apply (fiberObjEquivHom xi' B)
        (sourcePointOfFiberOver A xi' B y))).trans
      (fiberOverOfSourcePoint_sourcePointOfFiberOver A xi' B y)
  right_inv z := by
    apply (fiberObjEquivHom xi' B).injective
    rw [Equiv.apply_symm_apply]
    exact sourcePointOfFiberOver_fiberOverOfSourcePoint A xi' B _

theorem

fiberOverEquiv_apply

L217 ↗

AlgebraicGeometry.FiniteEtale.fiberOverEquiv_apply

Source context 8 commands

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

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

Lean source · statement

theorem fiberOverEquiv_apply
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    fiberOverEquiv A xi' B y =
      (fiberObjEquivHom xi' B).symm (sourcePointOfFiberOver A xi' B y)

theorem

sourcePointOfFiberOver_naturality

L226 ↗

AlgebraicGeometry.FiniteEtale.sourcePointOfFiberOver_naturality

Source context 8 commands

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

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

Lean source · statement

theorem sourcePointOfFiberOver_naturality
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    {B C : FiniteEtale A.left} (f : B ⟶ C)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    sourcePointOfFiberOver A xi' C
        ((fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).map
          (toOverMap A f) y) =
      sourcePointOfFiberOver A xi' B y ≫ f.hom

theorem

fiberObjEquivHom_map_symm

L243 ↗

AlgebraicGeometry.FiniteEtale.fiberObjEquivHom_map_symm

Source context 8 commands

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

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

Lean source · statement

theorem fiberObjEquivHom_map_symm
    (xi' : Spec (.of Omega) ⟶ S) {B C : FiniteEtale S} (f : B ⟶ C)
    (z : Over.mk xi' ⟶ B.toComma) :
    z ≫ f.hom =
      fiberObjEquivHom xi' C
        ((fiber xi').map f ((fiberObjEquivHom xi' B).symm z))

theorem

fiberOverFormula_naturality

L257 ↗

AlgebraicGeometry.FiniteEtale.fiberOverFormula_naturality

Source context 8 commands

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

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

Lean source · statement

theorem fiberOverFormula_naturality
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    {B C : FiniteEtale A.left} (f : B ⟶ C)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    (fiberObjEquivHom xi' C).symm
        (sourcePointOfFiberOver A xi' C
          ((fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).map
            (toOverMap A f) y)) =
      (fiber xi').map f
        ((fiberObjEquivHom xi' B).symm (sourcePointOfFiberOver A xi' B y))

theorem

fiberOverEquiv_naturality

L272 ↗

AlgebraicGeometry.FiniteEtale.fiberOverEquiv_naturality

Source context 8 commands

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

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

Lean source · statement

theorem fiberOverEquiv_naturality
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    {B C : FiniteEtale A.left} (f : B ⟶ C)
    (y : (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).obj
      (toOverObj A B)) :
    fiberOverEquiv A xi' C
        ((fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).map
          (toOverMap A f) y) =
      (fiber xi').map f (fiberOverEquiv A xi' B y)

def

overEquivFiberIso

L285 ↗

AlgebraicGeometry.FiniteEtale.overEquivFiberIso

Documentation

Under the equivalence with the over-category, the geometric fiber at the lifted point is the fiber over the corresponding point of the base fiber.

Source context 8 commands

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

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

Lean source · statement

def overEquivFiberIso (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    (overEquiv A).functor ⋙
        fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi') ≅
      fiber xi'

def

autFiberOverEquivFiber

L301 ↗

AlgebraicGeometry.FiniteEtale.autFiberOverEquivFiber

Documentation

The over-category fiber comparison induces the actual topological isomorphism of its automorphism group with the lifted geometric fundamental group.

Source context 8 commands

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

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

Lean source · statement

def autFiberOverEquivFiber
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left) :
    Aut (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')) ≃ₜ*
      Aut (fiber xi')

def

fundamentalGroupEquivStabilizerOfLift

L331 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivStabilizerOfLift

Documentation

The étale fundamental group at a lifted geometric point is canonically isomorphic to the stabilizer of the corresponding point in the geometric fiber of the finite étale cover over the base.

Source context 8 commands

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

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

Lean source · statement

def fundamentalGroupEquivStabilizerOfLift
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    π₁ᵉᵗ(xi') ≃ₜ*
      MulAction.stabilizer (π₁ᵉᵗ(basePoint A xi')) (liftedFiberPoint A xi')

def

pullbackToProductOver

L339 ↗

AlgebraicGeometry.FiniteEtale.pullbackToProductOver

Source context 8 commands

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

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

Lean source · statement

def pullbackToProductOver
    (A : FiniteEtale S) (B : FiniteEtale S) :
    toOverObj A ((pullback A.hom).obj B) ⟶
      (productOver (X := A)).obj B

theorem

sourcePointOf_overEquivFiberIso_inv

L351 ↗

AlgebraicGeometry.FiniteEtale.sourcePointOf_overEquivFiberIso_inv

Source context 8 commands

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

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

Lean source · statement

theorem sourcePointOf_overEquivFiberIso_inv
    (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale A.left) (p : (fiber xi').obj B) :
    sourcePointOfFiberOver A xi' B
        ((overEquivFiberIso A xi').inv.app B p) =
      fiberObjEquivHom xi' B p

theorem

fiberOver_map_pullbackToProductOver

L365 ↗

AlgebraicGeometry.FiniteEtale.fiberOver_map_pullbackToProductOver

Source context 8 commands

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

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

Lean source · statement

theorem fiberOver_map_pullbackToProductOver
    [ConnectedSpace S] (A : FiniteEtale S) (xi' : Spec (.of Omega) ⟶ A.left)
    (B : FiniteEtale S) (b : (fiber (basePoint A xi')).obj B) :
    (fiberOver (fiber (basePoint A xi')) (liftedFiberPoint A xi')).map
        (pullbackToProductOver A B)
        ((overEquivFiberIso A xi').inv.app ((pullback A.hom).obj B)
          (transportedPointOfCompIso (pullback A.hom)
            (pullbackFiberIso A.hom xi') B b)) =
      productFiberEquivComparison
        (fiber (basePoint A xi')) (liftedFiberPoint A xi') B b

theorem

fundamentalGroupEquivStabilizerOfLift_coe

L458 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivStabilizerOfLift_coe

Source context 8 commands

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

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

Lean source · statement

theorem fundamentalGroupEquivStabilizerOfLift_coe
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) (a : π₁ᵉᵗ(xi')) :
    (fundamentalGroupEquivStabilizerOfLift A xi' a :
        π₁ᵉᵗ(basePoint A xi')) =
      fundamentalGroupHom A.hom xi' a

def

fundamentalGroupEquivStabilizerOfLiftOverComposite

L549 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivStabilizerOfLiftOverComposite

Documentation

The lifted-point stabilizer equivalence with the base point written as the literal composite with the finite-etale covering map.

Source context 8 commands

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

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

Lean source · statement

def fundamentalGroupEquivStabilizerOfLiftOverComposite
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left) :
    π₁ᵉᵗ(xi') ≃ₜ*
      MulAction.stabilizer (π₁ᵉᵗ(xi' ≫ A.hom))
        (liftedFiberPointOverComposite A xi')

theorem

transported_stabilizer_liftedFiberPointOverComposite

L560 ↗

AlgebraicGeometry.FiniteEtale.transported_stabilizer_liftedFiberPointOverComposite

Documentation

Transporting the stabilizer of a lifted fiber point along an equality of base points gives the stabilizer of the corresponding point in the chosen fiber.

Source context 8 commands

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

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

Lean source · statement

theorem transported_stabilizer_liftedFiberPointOverComposite
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left)
    {xi : Spec (.of Omega) ⟶ S} (hxi : xi' ≫ A.hom = xi) :
    (hxi ▸ MulAction.stabilizer (π₁ᵉᵗ(xi' ≫ A.hom))
      (liftedFiberPointOverComposite A xi')) =
        MulAction.stabilizer (π₁ᵉᵗ(xi))
          ((fiberObjEquivHom xi A).symm (Over.homMk xi' hxi))

def

fundamentalGroupEquivStabilizerOfLiftOfEq

L573 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivStabilizerOfLiftOfEq

Documentation

The stabilizer equivalence transported along an equality identifying the composite of a lifted point with a chosen base point.

Source context 8 commands

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

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

Lean source · full declaration

def fundamentalGroupEquivStabilizerOfLiftOfEq
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left)
    {xi : Spec (.of Omega) ⟶ S} (hxi : xi' ≫ A.hom = xi) :
    π₁ᵉᵗ(xi') ≃ₜ*
      ↥(show Subgroup π₁ᵉᵗ(xi) from
        hxi ▸ MulAction.stabilizer (π₁ᵉᵗ(xi' ≫ A.hom))
          (liftedFiberPointOverComposite A xi')) := by
  subst xi
  exact fundamentalGroupEquivStabilizerOfLiftOverComposite A xi'

theorem

fundamentalGroupEquivStabilizerOfLiftOfEq_coe

L586 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivStabilizerOfLiftOfEq_coe

Documentation

After transporting the base point equality, the stabilizer equivalence is the homomorphism on fundamental groups induced by the covering map.

Source context 8 commands

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

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

Lean source · full declaration

theorem fundamentalGroupEquivStabilizerOfLiftOfEq_coe
    [ConnectedSpace S] (A : FiniteEtale S)
    (xi' : Spec (.of Omega) ⟶ A.left)
    {xi : Spec (.of Omega) ⟶ S} (hxi : xi' ≫ A.hom = xi)
    (a : π₁ᵉᵗ(xi')) :
    ((fundamentalGroupEquivStabilizerOfLiftOfEq A xi' hxi a :
        ↥(show Subgroup π₁ᵉᵗ(xi) from
          hxi ▸ MulAction.stabilizer (π₁ᵉᵗ(xi' ≫ A.hom))
            (liftedFiberPointOverComposite A xi'))) : π₁ᵉᵗ(xi)) =
      hxi ▸ fundamentalGroupHom A.hom xi' a := by
  subst xi
  exact fundamentalGroupEquivStabilizerOfLift_coe A xi' a

Module documentation

Geometric fibers over a pointed finite étale cover

Declarations