NYLL
Module

GaloisObjectQuotient.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectQuotient
6 declarations indexed from sourceView source ↗

Module documentation

Finite quotients represented by Galois objects

A pointed Galois object identifies its fiber with its categorical automorphism group. Since categorical automorphisms act on the right of the fiber while the fundamental group acts on the left, the resulting quotient has target the opposite automorphism group.

Imports3
Imported by12

Declarations

def

galoisObjectQuotientMonoidHom

L37 ↗
CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom
Documentation

The quotient represented by a pointed Galois object. The opposite on the target records the contravariance of categorical automorphism multiplication relative to the left fundamental-group action.

Source context 8 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
Lean source · statement
def galoisObjectQuotientMonoidHom
    (A : C) [IsGalois A] (a : F.obj A) : G →* (Aut A)ᵐᵒᵖ
theorem

galoisObjectQuotientMonoidHom_unop_apply

L67 ↗
CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_unop_apply
Source context 9 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
include hNatural in
Lean source · statement
theorem galoisObjectQuotientMonoidHom_unop_apply
    (A : C) [IsGalois A] (a : F.obj A) (g : G) :
    (galoisObjectQuotientMonoidHom F G A a g).unop =
      (evaluationEquivOfIsGalois F A a).symm (g • a)
theorem

galoisObjectQuotientMonoidHom_evaluation

L77 ↗
CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_evaluation
Documentation

Evaluating the cover automorphism selected by the quotient recovers the fundamental-group action on the chosen point.

Source context 9 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
include hNatural in
Lean source · statement
theorem galoisObjectQuotientMonoidHom_evaluation
    (A : C) [IsGalois A] (a : F.obj A) (g : G) :
    F.map ((galoisObjectQuotientMonoidHom F G A a g).unop.hom) a = g • a
theorem

galoisObjectQuotientMonoidHom_ker

L84 ↗
CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_ker
Documentation

The kernel of the finite quotient represented by a pointed Galois object is exactly the stabilizer of the chosen fiber point.

Source context 8 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
Lean source · statement
theorem galoisObjectQuotientMonoidHom_ker
    (A : C) [IsGalois A] (a : F.obj A) :
    (galoisObjectQuotientMonoidHom F G A a).ker =
      MulAction.stabilizer G a
theorem

galoisObjectQuotientMonoidHom_surjective

L103 ↗
CategoryTheory.PreGaloisCategory.galoisObjectQuotientMonoidHom_surjective
Documentation

A transitive fundamental-group action makes the quotient represented by a Galois object surjective.

Source context 8 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
Lean source · statement
theorem galoisObjectQuotientMonoidHom_surjective
    (A : C) [IsGalois A] (a : F.obj A)
    [MulAction.IsPretransitive G (F.obj A)] :
    Function.Surjective (galoisObjectQuotientMonoidHom F G A a)
theorem

iInf_galoisObjectQuotientMonoidHom_ker

L119 ↗
CategoryTheory.PreGaloisCategory.iInf_galoisObjectQuotientMonoidHom_ker
Documentation

Pointed finite Galois quotients separate the automorphisms of a fiber functor. A natural automorphism fixing the fiber of every Galois object fixes every fiber, since every fiber point is the image of a pointed Galois object.

Source context 8 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w v
variable {C : Type u₁} [Category.{u₂} C]
variable (F : CategoryTheory.Functor C FintypeCat.{w})
  [GaloisCategory C] [FiberFunctor F]
variable (G : Type v) [Group G]
variable [∀ X, MulAction G (F.obj X)] [hNatural : IsNaturalSMul F G]
Lean source · full declaration
theorem iInf_galoisObjectQuotientMonoidHom_ker :
    (⨅ (A : C) (hA : IsGalois A) (a : F.obj A),
      (letI : IsGalois A := hA
       galoisObjectQuotientMonoidHom F (Aut F) A a).ker) = ⊥ := by
  apply le_antisymm ?_ bot_le
  intro g hg
  rw [Subgroup.mem_bot]
  apply Iso.ext
  apply natTrans_ext_of_isGalois F
  intro A hA
  apply FintypeCat.hom_ext
  intro a
  have hfix := (Subgroup.mem_iInf.mp
    (Subgroup.mem_iInf.mp (Subgroup.mem_iInf.mp hg A) hA) a)
  rw [galoisObjectQuotientMonoidHom_ker,
    MulAction.mem_stabilizer_iff] at hfix
  change g • a = a
  exact hfix

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