mk_lt_mk_of_comm — Mathlib

English

For i1, i2 with f: A1 → A2 and fac: f ≫ i2 = i1, Subobject mk i1 < Subobject mk i2 iff not IsIso f.

Русский

Для i1, i2 и f: A1 → A2 с fac: f ≫ i2 = i1, mk i1 < mk i2 эквивалентно не изоморфизму f.

LaTeX

$$$Subobject.mk i_1 < Subobject.mk i_2 \iff \lnot \IsIso f$$$

Lean4

theorem mk_lt_mk_of_comm {X A₁ A₂ : C} {i₁ : A₁ ⟶ X} {i₂ : A₂ ⟶ X} [Mono i₁] [Mono i₂] (f : A₁ ⟶ A₂) (fac : f ≫ i₂ = i₁)
    (hf : ¬IsIso f) : Subobject.mk i₁ < Subobject.mk i₂ :=
  by
  obtain _ | h := (mk_le_mk_of_comm _ fac).lt_or_eq
  · assumption
  · exfalso
    apply hf
    convert (isoOfMkEqMk i₁ i₂ h).isIso_hom
    rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]

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