instGaloisCategoryActionFintypeCat

English

The category of finite G-sets is a Galois category; it carries a canonical fiber functor given by forgetful functor to sets.

Русский

Категория конечных G-наборов является Галуа-категорией; существует естественный фибер-функтор, задаваемый забыванием до множеств.

LaTeX

$$$\\text{FintypeCat Action } G \\text{ is a } \\mathrm{GaloisCategory}$$$

Lean4

/-- The category of finite `G`-sets is a `GaloisCategory`. -/
instance : GaloisCategory (Action FintypeCat G) where hasFiberFunctor := ⟨Action.forget FintypeCat G, ⟨inferInstance⟩⟩

Похожие утверждения