Module

GaloisObjectFixedFiber.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectFixedFiber

1 declaration indexed from sourceView source ↗

Module documentation

The kernel of a Galois quotient fixes its entire fiber

The point stabilizer of a Galois object fixes every point because its deck transformations act transitively and commute with the fundamental group.

The proof below was extracted unchanged from EtaleFundamentalGroups.FiniteEtale.TrivialBaseChangeAlgebra.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.GaloisObjectQuotient

Imported by3

theorem

fiber_fixed_of_galoisObjectQuotient_eq_one

L28 ↗

CategoryTheory.PreGaloisCategory.fiber_fixed_of_galoisObjectQuotient_eq_one

Documentation

The kernel of a pointed Galois quotient fixes the entire fiber, not just the chosen point. Transitivity of cover automorphisms supplies every other point.

Source context 3 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory

Lean source · statement

theorem fiber_fixed_of_galoisObjectQuotient_eq_one
    {C : Type*} [Category C] [GaloisCategory C]
    (F : C ⥤ FintypeCat) [FiberFunctor F]
    (W : C) [IsGalois W] (w₀ : F.obj W) (g : Aut F)
    (hg : galoisObjectQuotientMonoidHom F (Aut F) W w₀ g = 1)
    (w : F.obj W) : g • w = w

Module documentation

The kernel of a Galois quotient fixes its entire fiber

Declarations

fiber_fixed_of_galoisObjectQuotient_eq_one