split_iff_of_iso — Mathlib

English

There is an equivalence between the existence of a split for p and for p' under an isomorphism φ: X ≅ X'.

Русский

Существование разложения/распада p эквивалентно существованию разложения p' через изоморфизм φ: X ≅ X'.

LaTeX

$$$ (\\exists Y,i,e) \\; (i \\circ e = id_Y) \\land (e \\circ i = p) \\iff (\\exists Y',i',e') \\; (i' \\circ e' = id_{Y'}) \\land (e' \\circ i' = p') $$$

Lean4

theorem split_iff_of_iso {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') (hpp' : p ≫ φ.hom = φ.hom ≫ p') :
    (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔
      ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p' :=
  by
  constructor
  · exact split_imp_of_iso φ p p' hpp'
  · apply split_imp_of_iso φ.symm p' p
    rw [← comp_id p, ← φ.hom_inv_id]
    slice_rhs 2 3 => rw [hpp']
    simp

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