isSplitMono_iff — Mathlib

English

For any f, IsSplitMono (F.map f) holds iff IsSplitMono f, given F is full and faithful.

Русский

Для любого f, IsSplitMono (F.map f) эквивалично IsSplitMono f, если F полно и точно сохраняет морфизмы.

LaTeX

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

Lean4

@[simp]
theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f :=
  by
  constructor
  · intro h
    exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)
  · intro h
    exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)

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