comma_iso_iff — Mathlib

English

For P with RespectsIso, for arrows f,g in a comma category, P f.hom ↔ P g.hom when f ≅ g.

Русский

Для P с RespectsIso, в коммокатегории стрелки f и g эквивалентны по P f.hom ↔ P g.hom при f ≅ g.

LaTeX

$$$P f.hom \iff P g.hom$ if $f \cong g$$$

Lean4

theorem comma_iso_iff (P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B] {L : A ⥤ C}
    {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) : P f.hom ↔ P g.hom := by
  simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]

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