instFiberFunctorActionFintypeCatForget

English

There exists a lift of a monomorphism i: Y → (functorToAction F).obj X through a suitable Z with u: Y ≅ (functorToAction F).obj Z such that i = u.hom ≫ (functorToAction F).map f.

Русский

Существует подъём мономорфизма i: Y → (functorToAction F).obj X через подходящий Z с u: Y ≅ ... так, что i = u.hom ≫ (functorToAction F).map f.

LaTeX

$$$\\exists Z:\\, C, \\exists f:\\, Z \\to X, \\exists u:\\, Y \\cong (\\mathrm{functorToAction} F).obj Z,\\mathtt{Mono}\\ f,\\ i = u.hom \\circ (\\mathrm{functorToAction} F).map f$$$

Lean4

/-- The forgetful functor from finite `G`-sets to sets is a `FiberFunctor`. -/
noncomputable instance : FiberFunctor (Action.forget FintypeCat G)
    where
  preservesFiniteCoproducts := ⟨fun _ ↦ inferInstance⟩
  preservesQuotientsByFiniteGroups _ _ _ := inferInstance
  reflectsIsos := ⟨fun f (_ : IsIso f.hom) => inferInstance⟩

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