English
The forgetful functor from finite G-sets to sets is a fiber functor, preserving finite coproducts and quotient by finite groups and reflecting isomorphisms.
Русский
Функтор забывания от конечных G-наборов к множествам — это фибер-функтор, сохраняющий конечные копроизведения и факторизации по конечным группам и отражающий изоморфизмы.
LaTeX
$$$\\text{Forget} : \\mathrm{Action\\,FintypeCat\\,G} \\to \\mathrm{Set}$ is a fiber functor;\\quad \\text{preservesFiniteCoproducts},\\ \\text{preservesQuotientsByFiniteGroups},\\ \\text{reflectsIsos}$$$
Lean4
/-- The category of finite `G`-sets is a `PreGaloisCategory`. -/
instance : PreGaloisCategory (Action FintypeCat G)
where
hasQuotientsByFiniteGroups _ _ _ := inferInstance
monoInducesIsoOnDirectSummand {_ _} i
_ :=
⟨Action.imageComplement G i, Action.imageComplementIncl G i,
⟨isColimitOfReflects (Action.forget _ _ ⋙ FintypeCat.incl) <|
(isColimitMapCoconeBinaryCofanEquiv (forget _) i _).symm (Types.isCoprodOfMono ((forget _).map i))⟩⟩
