split_imp_of_iso — Mathlib

English

If φ : X ≅ X' carries an idempotent p to p' and p splits as i;e, then p' splits similarly.

Русский

Если φ переносит идемпотент p на p' и p распадается как i;e, то p' распадается аналогично.

LaTeX

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

Lean4

theorem split_imp_of_iso {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') (hpp' : p ≫ φ.hom = φ.hom ≫ p')
    (h : ∃ (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
  rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
  use Y, i ≫ φ.hom, φ.inv ≫ e
  grind

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