isSplitEpi_iff — Mathlib

English

For any morphism f, IsSplitEpi (F.map f) holds iff IsSplitEpi f, provided F is full and faithful.

Русский

Пусть F полно и точно сохраняет мономорфизмы; тогда IsSplitEpi (F.map f) эквивалично IsSplitEpi f.

LaTeX

$$$$ \\operatorname{IsSplitEpi}(F.map f) \\iff \\operatorname{IsSplitEpi}(f). $$$$

Lean4

@[simp]
theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f :=
  by
  constructor
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

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