strongEpi_map_iff_strongEpi_of_isEquivalence

English

For any f, IsSplitMono (F.map f) iff IsSplitMono f under Full F and Faithful F.

Русский

При полном и точном сохранении мономорфизм IsSplitMono (F.map f) эквивалентно IsSplitMono f.

LaTeX

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

Lean4

@[simp]
theorem strongEpi_map_iff_strongEpi_of_isEquivalence [IsEquivalence F] : StrongEpi (F.map f) ↔ StrongEpi f :=
  by
  constructor
  · intro
    have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) := Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
    rw [StrongEpi.iff_of_arrow_iso e]
    infer_instance
  · intro
    infer_instance

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