splitMonoEquiv — Mathlib

English

If F is fully faithful, then SplitMono f is equivalent to SplitMono (F.map f).

Русский

Если F полно и точно сохраняет морфизмы, то SplitMono f эквивалентно SplitMono(F.map f).

LaTeX

$$$$ \\text{SplitMono } f \\;\\cong\\; \\text{SplitMono}(F.map\\,f). $$$$

Lean4

/-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
noncomputable def splitMonoEquiv [Full F] [Faithful F] : SplitMono f ≃ SplitMono (F.map f)
    where
  toFun f := f.map F
  invFun
    s :=
    ⟨F.preimage s.retraction, by
      apply F.map_injective
      simp only [map_comp, map_preimage, map_id]
      apply SplitMono.id⟩
  left_inv := by cat_disch
  right_inv x := by cat_disch

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