costructuredArrow_iso_iff — Mathlib

English

If P respects isomorphisms on T, then for L: A ⥤ T and X ∈ T, for any f,g : CostructuredArrow L X, an iso e: f ≅ g yields that P f.hom ↔ P g.hom.

Русский

Если P сохраняет изоморфизмы на T, то для L: A ⥤ T и X ∈ T, для любых f,g: CostructuredArrow L X, изоморфизм e: f ≅ g даёт эквивалентность P f.hom ↔ P g.hom.

LaTeX

$$$P\\,\\text{costructuredArrowIso} (L,X):\\; P(f.hom) \\iff P(g.hom) ,\\; e: f\\cong g$$$

Lean4

theorem costructuredArrow_iso_iff (P : MorphismProperty T) [P.RespectsIso] {L : A ⥤ T} {X : T}
    {f g : CostructuredArrow L X} (e : f ≅ g) : P f.hom ↔ P g.hom :=
  P.comma_iso_iff e

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