epi_right — Mathlib

English

If sq is epi, then sq.right is epi.

Русский

Если sq эпиморфизм, то sq.right эпиморфизм.

LaTeX

$$$\text{Epi}(sq) \Rightarrow \text{Epi}(sq.right)$$$

Lean4

instance epi_right [Epi sq] : Epi sq.right where
  left_cancellation {Z} φ ψ
    h :=
    by
    let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
      { right := φ
        left := g.hom ≫ φ }
    change (aux φ).right = (aux ψ).right
    congr 1
    rw [← cancel_epi sq]
    apply CommaMorphism.ext
    · rw [Comma.comp_left, Comma.comp_left, Arrow.w_assoc, Arrow.w_assoc, h]
    · exact h

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