mono_left — Mathlib

English

If sq is mono, then sq.left is mono.

Русский

Если sq моно, то sq.left моно.

LaTeX

$$$\text{Mono}(sq) \Rightarrow \text{Mono}(sq.left)$$$

Lean4

instance mono_left [Mono sq] : Mono sq.left where
  right_cancellation {Z} φ ψ
    h :=
    by
    let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
      { left := φ
        right := φ ≫ f.hom }
    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp
    change (aux φ).left = (aux ψ).left
    congr 1
    rw [← cancel_mono sq]
    apply CommaMorphism.ext
    · exact h
    · rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc]
      rw [← Arrow.w]
      simp only [← Category.assoc, h]

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