NYLL
Module

PointedOver.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.PointedOver
23 declarations indexed from sourceView source ↗

Module documentation

Fiber functors on pointed over-categories

For a finite fiber functor F, an object X, and a point x of its fiber, we compare the automorphisms of F fixing x with the automorphisms of the fiber-over-x functor on Over X.

Imports2
Imported by4

Declarations

def

fiberOver

L31 ↗
CategoryTheory.PreGaloisCategory.fiberOver
Documentation

The fiber over x of an object over X.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
Lean source · full declaration
def fiberOver : Over X ⥤ FintypeCat.{w} where
  obj U := FintypeCat.of { y : F.obj U.left // F.map U.hom y = x }
  map {U V} f := FintypeCat.homMk fun y ↦
    ⟨F.map f.left y.1, by
      rw [← FintypeCat.comp_apply, ← F.map_comp, Over.w f]
      exact y.2⟩
  map_id U := by
    apply FintypeCat.hom_ext
    intro y
    change (⟨F.map (𝟙 U.left) y.1, _⟩ :
      { z : F.obj U.left // F.map U.hom z = x }) = y
    simp
  map_comp f g := by
    apply FintypeCat.hom_ext
    intro y
    apply Subtype.ext
    change F.map (f.left ≫ g.left) y.1 = F.map g.left (F.map f.left y.1)
    rw [F.map_comp]
    exact FintypeCat.comp_apply (F.map f.left) (F.map g.left) y.1
theorem

fiberOver_map_val

L54 ↗
CategoryTheory.PreGaloisCategory.fiberOver_map_val
Documentation

The underlying point of a mapped element is obtained by applying F to the underlying morphism in the over-category.

Source context 7 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
Lean source · statement
theorem fiberOver_map_val {U V : Over X} (f : U ⟶ V) (y : (fiberOver F x).obj U) :
    ((fiberOver F x).map f y).1 = F.map f.left y.1
def

productOver

L61 ↗
CategoryTheory.PreGaloisCategory.productOver
Documentation

Sending Y to the projection Y ⨯ X ⟶ X defines a functor into Over X.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · full declaration
def productOver : C ⥤ Over X where
  obj Y := Over.mk (prod.snd : Y ⨯ X ⟶ X)
  map {Y Z} f := Over.homMk (prod.map f (𝟙 X)) (by
    change prod.map f (𝟙 X) ≫ prod.snd = prod.snd
    simp)
  map_id Y := by
    ext
    change prod.map (𝟙 Y) (𝟙 X) = 𝟙 (Y ⨯ X)
    exact prod.map_id_id
  map_comp f g := by
    ext
    change prod.map (f ≫ g) (𝟙 X) = prod.map f (𝟙 X) ≫ prod.map g (𝟙 X)
    exact prod.map_comp_id f g
def

productFiberEquiv

L75 ↗
CategoryTheory.PreGaloisCategory.productFiberEquiv
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · full declaration
def productFiberEquiv (Y : C) :
    F.obj Y ≃ (fiberOver F x).obj ((productOver (X := X)).obj Y) where
  toFun y :=
    ⟨(fiberBinaryProductEquiv F Y X).symm (y, x),
      fiberBinaryProductEquiv_symm_snd_apply F y x⟩
  invFun z := ((fiberBinaryProductEquiv F Y X) z.1).1
  left_inv y := by
    rw [← fiberBinaryProductEquiv_symm_fst_apply F y x]
    simp
  right_inv z := by
    apply Subtype.ext
    let e := fiberBinaryProductEquiv F Y X
    have hz : F.map (prod.snd : Y ⨯ X ⟶ X) z.1 = x := by
      exact z.2
    have hsnd : (e z.1).2 = x := by
      calc
        (e z.1).2 = F.map prod.snd (e.symm (e z.1)) :=
          (fiberBinaryProductEquiv_symm_snd_apply F (e z.1).1 (e z.1).2).symm
        _ = F.map prod.snd z.1 :=
          congrArg (F.map prod.snd) (e.symm_apply_apply z.1)
        _ = x := hz
    change e.symm ((e z.1).1, x) = z.1
    have hpair : ((e z.1).1, x) = e z.1 := by
      apply Prod.ext
      · rfl
      · exact hsnd.symm
    exact (congrArg e.symm hpair).trans (e.symm_apply_apply z.1)
theorem

fiberBinaryProductEquiv_apply

L103 ↗
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_apply
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem fiberBinaryProductEquiv_apply (Y : C) (z : F.obj (Y ⨯ X)) :
    fiberBinaryProductEquiv F Y X z = (F.map prod.fst z, F.map prod.snd z)
theorem

productPoint_naturality

L116 ↗
CategoryTheory.PreGaloisCategory.productPoint_naturality
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem productPoint_naturality {Y Z : C} (f : Y ⟶ Z) (y : F.obj Y) :
    F.map (prod.map f (𝟙 X)) ((fiberBinaryProductEquiv F Y X).symm (y, x)) =
      (fiberBinaryProductEquiv F Z X).symm (F.map f y, x)
theorem

productFiberEquiv_naturality

L145 ↗
CategoryTheory.PreGaloisCategory.productFiberEquiv_naturality
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem productFiberEquiv_naturality {Y Z : C} (f : Y ⟶ Z) (y : F.obj Y) :
    (fiberOver F x).map ((productOver (X := X)).map f) (productFiberEquiv F x Y y) =
      productFiberEquiv F x Z (F.map f y)
def

productFiberIso

L156 ↗
CategoryTheory.PreGaloisCategory.productFiberIso
Documentation

The original fiber functor is the restriction of fiberOver F x along Y ↦ (Y ⨯ X ⟶ X).

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
def productFiberIso :
    productOver (X := X) ⋙ fiberOver F x ≅ F
def

extendFiberOverAut

L167 ↗
CategoryTheory.PreGaloisCategory.extendFiberOverAut
Documentation

Extend a natural automorphism of the fiber-over-x functor to the original fiber functor by evaluating it on the projections Y ⨯ X ⟶ X.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
def extendFiberOverAut : Aut (fiberOver F x) →ₜ* Aut F
def

productFiberEquivComparison

L171 ↗
CategoryTheory.PreGaloisCategory.productFiberEquivComparison
Documentation

The point comparison used to extend fiber-over automorphisms.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
def productFiberEquivComparison (Y : C) :
    F.obj Y ≃ (fiberOver F x).obj ((productOver (X := X)).obj Y)
theorem

productFiberEquivComparison_symm_apply

L176 ↗
CategoryTheory.PreGaloisCategory.productFiberEquivComparison_symm_apply
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem productFiberEquivComparison_symm_apply
    (Y : C) (z : (fiberOver F x).obj ((productOver (X := X)).obj Y)) :
    (productFiberEquivComparison F x Y).symm z = F.map Limits.prod.fst z.1
theorem

extendFiberOverAut_hom_app_apply

L184 ↗
CategoryTheory.PreGaloisCategory.extendFiberOverAut_hom_app_apply
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem extendFiberOverAut_hom_app_apply
    (a : Aut (fiberOver F x)) (Y : C) (y : F.obj Y) :
    (extendFiberOverAut F x a).hom.app Y y =
      (productFiberEquiv F x Y).symm
        (a.hom.app ((productOver (X := X)).obj Y) (productFiberEquiv F x Y y))
theorem

extendFiberOverAut_hom_app_apply_eq

L192 ↗
CategoryTheory.PreGaloisCategory.extendFiberOverAut_hom_app_apply_eq
Documentation

Evaluation formula for the extension of a fiber-over automorphism.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem extendFiberOverAut_hom_app_apply_eq
    (a : Aut (fiberOver F x)) (Y : C) (y : F.obj Y) :
    (extendFiberOverAut F x a).hom.app Y y =
      (productFiberEquivComparison F x Y).symm
        (a.hom.app ((productOver (X := X)).obj Y)
          (productFiberEquivComparison F x Y y))
def

graphToProduct

L202 ↗
CategoryTheory.PreGaloisCategory.graphToProduct
Documentation

The graph of an object U ⟶ X as a morphism to the projection U ⨯ X ⟶ X.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
def graphToProduct (U : Over X) : U ⟶ (productOver (X := X)).obj U.left
theorem

graphPoint_eq_productPoint

L207 ↗
CategoryTheory.PreGaloisCategory.graphPoint_eq_productPoint
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem graphPoint_eq_productPoint (U : Over X) (y : F.obj U.left)
    (hy : F.map U.hom y = x) :
    F.map (prod.lift (𝟙 U.left) U.hom) y =
      (fiberBinaryProductEquiv F U.left X).symm (y, x)
theorem

fiberOver_map_graphToProduct

L221 ↗
CategoryTheory.PreGaloisCategory.fiberOver_map_graphToProduct
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem fiberOver_map_graphToProduct
    (U : Over X) (y : (fiberOver F x).obj U) :
    (fiberOver F x).map (graphToProduct (X := X) U) y =
      productFiberEquiv F x U.left y.1
theorem

extendFiberOverAut_fixes_point

L230 ↗
CategoryTheory.PreGaloisCategory.extendFiberOverAut_fixes_point
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem extendFiberOverAut_fixes_point (a : Aut (fiberOver F x)) :
    extendFiberOverAut F x a • x = x
def

restrictAutToFiberOverObj

L273 ↗
CategoryTheory.PreGaloisCategory.restrictAutToFiberOverObj
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
def restrictAutToFiberOverObj
    (a : MulAction.stabilizer (Aut F) x) (U : Over X) :
    (fiberOver F x).obj U ≅ (fiberOver F x).obj U
def

restrictAutToFiberOver

L298 ↗
CategoryTheory.PreGaloisCategory.restrictAutToFiberOver
Documentation

Restrict an automorphism of F fixing x to the fibers over x.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · full declaration
def restrictAutToFiberOver :
    MulAction.stabilizer (Aut F) x →* Aut (fiberOver F x) where
  toFun a := NatIso.ofComponents (restrictAutToFiberOverObj F x a) (fun f ↦ by
    apply FintypeCat.hom_ext
    intro y
    apply Subtype.ext
    change a.1 • F.map f.left y.1 = F.map f.left (a.1 • y.1)
    exact mulAction_naturality F a.1 f.left y.1)
  map_one' := by
    ext U y
    rfl
  map_mul' a b := by
    ext U y
    rfl
theorem

extendFiberOverAut_restrictAutToFiberOver

L313 ↗
CategoryTheory.PreGaloisCategory.extendFiberOverAut_restrictAutToFiberOver
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem extendFiberOverAut_restrictAutToFiberOver
    (a : MulAction.stabilizer (Aut F) x) :
    extendFiberOverAut F x (restrictAutToFiberOver F x a) = a.1
theorem

restrictAutToFiberOver_extendFiberOverAut

L332 ↗
CategoryTheory.PreGaloisCategory.restrictAutToFiberOver_extendFiberOverAut
Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · statement
theorem restrictAutToFiberOver_extendFiberOverAut
    (a : Aut (fiberOver F x)) :
    restrictAutToFiberOver F x
        ⟨extendFiberOverAut F x a, extendFiberOverAut_fixes_point F x a⟩ = a
def

autFiberOverMulEquivStabilizer

L366 ↗
CategoryTheory.PreGaloisCategory.autFiberOverMulEquivStabilizer
Documentation

Extension identifies the automorphism group of the fiber-over-x functor with the stabilizer of x in Aut F.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · full declaration
def autFiberOverMulEquivStabilizer :
    Aut (fiberOver F x) ≃* MulAction.stabilizer (Aut F) x where
  toFun a := ⟨extendFiberOverAut F x a, extendFiberOverAut_fixes_point F x a⟩
  invFun := restrictAutToFiberOver F x
  left_inv := restrictAutToFiberOver_extendFiberOverAut F x
  right_inv a := by
    apply Subtype.ext
    exact extendFiberOverAut_restrictAutToFiberOver F x a
  map_mul' a b := by
    apply Subtype.ext
    exact (extendFiberOverAut F x).map_mul a b
def

autFiberOverEquivStabilizer

L379 ↗
CategoryTheory.PreGaloisCategory.autFiberOverEquivStabilizer
Documentation

The stabilizer comparison is an isomorphism of topological groups.

Source context 8 commands

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

noncomputable section
universe u₁ u₂ w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C]
variable (F : C ⥤ FintypeCat.{w})
variable {X : C} (x : F.obj X)
variable [PreGaloisCategory C] [FiberFunctor F]
Lean source · full declaration
def autFiberOverEquivStabilizer :
    Aut (fiberOver F x) ≃ₜ* MulAction.stabilizer (Aut F) x where
  toMulEquiv := autFiberOverMulEquivStabilizer F x
  continuous_toFun := (extendFiberOverAut F x).continuous.subtype_mk _
  continuous_invFun :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := (autFiberOverMulEquivStabilizer F x).toEquiv)
      ((extendFiberOverAut F x).continuous.subtype_mk _)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.