Module

OpenNormalUniverse.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalUniverse

1 declaration indexed from sourceView source ↗

Module documentation

Open normal subgroups across fiber-functor universes

The usual quotient construction for a fiber functor can live in a larger universe than its finite fibers. This file removes that presentation-level restriction by switching the universe of the fiber functor, applying the quotient construction there, and transporting the distinguished point back.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormal

Imported by8

theorem

exists_galois_object_point_stabilizer_eq_any_universe

L32 ↗

CategoryTheory.PreGaloisCategory.exists_galois_object_point_stabilizer_eq_any_universe

Documentation

Every open normal subgroup of the automorphism group of an arbitrary fiber functor is the stabilizer of a point on a Galois object, without a restriction relating the universe of the fibers to that of the category.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]

Lean source · statement

theorem exists_galois_object_point_stabilizer_eq_any_universe
    (U : OpenNormalSubgroup (Aut F)) :
    ∃ (X : C) (_ : IsGalois X) (x : F.obj X),
      MulAction.stabilizer (Aut F) x = (U : Subgroup (Aut F))

Module documentation

Open normal subgroups across fiber-functor universes

Declarations

exists_galois_object_point_stabilizer_eq_any_universe