English
Even in a more general fiber functor setting, every finite Aut F-set with continuous action is in the essential image of the induced ContAction functor.
Русский
Даже в более общем случае фибер-функторов, любое конечное Aut F-множество с непрерывным действием содержится в образе индукированного функторa ContAction.
LaTeX
$$$\\text{EssSurj}((\\mathrm{functorToContAction} F))$$$
Lean4
instance : (functorToContAction F).EssSurj :=
by
let F' : C ⥤ FintypeCat.{u₁} := F ⋙ FintypeCat.uSwitch.{w, u₁}
letI : FiberFunctor F' := FiberFunctor.comp_right _
have : (functorToContAction F').EssSurj := inferInstance
let f : Aut F ≃ₜ* Aut F' := (autEquivAutWhiskerRight F (FintypeCat.uSwitchEquivalence.{w, u₁}).fullyFaithfulFunctor)
let equiv : ContAction FintypeCat.{u₁} (Aut F') ≌ ContAction FintypeCat.{w} (Aut F) :=
(FintypeCat.uSwitchEquivalence.{u₁, w}.mapContAction (Aut F')
(fun X ↦ by
rw [Action.isContinuous_def]
change
Continuous
((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
(fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) ∘
(fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
have : Continuous (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) := X.2.1
fun_prop)
(fun X ↦ by
rw [Action.isContinuous_def]
change
Continuous
((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
(fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) ∘
(fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
have : Continuous (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) := X.2.1
fun_prop)).trans <|
ContAction.resEquiv _ f
have : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor :=
NatIso.ofComponents
(fun X ↦
ObjectProperty.isoMk _
(Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app _)
(fun g ↦ FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (g.hom.app X))))
(fun f ↦ by
ext : 2
exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f))
exact Functor.essSurj_of_iso this.symm
