English
If F is full and faithful, the split epi structure of f in C is equivalent to the split epi structure of F.map f in D; i.e., there is an equivalence between SplitEpi f and SplitEpi (F.map f).
Русский
Если F полно и точно сохраняет морфизмы, то структура расщепляющих эпиморфизмов для f и для F.map f эквивалентны; существует эквивалентность между SplitEpi f и SplitEpi(F.map f).
LaTeX
$$$$ \\text{SplitEpi } f \\;\\cong\\; \\text{SplitEpi}(F.map\\,f). $$$$
Lean4
/-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/
noncomputable def splitEpiEquiv [Full F] [Faithful F] : SplitEpi f ≃ SplitEpi (F.map f)
where
toFun f := f.map F
invFun
s :=
⟨F.preimage s.section_, by
apply F.map_injective
simp only [map_comp, map_preimage, map_id]
apply SplitEpi.id⟩
left_inv := by cat_disch
right_inv x := by cat_disch
