of_respects_arrow_iso — Mathlib

English

If for all arrows f,g in a category, and any isomorphism e: f ≅ g, P f.hom implies P g.hom, then P respects isomorphisms.

Русский

Если для любых стрел f,g в категории и любого изоморфизма e: f ≅ g выполнено, что P(hom(f)) ⇒ P(hom(g)), то P уважает изоморфизмы.

LaTeX

$$$\\big(\\forall f,g:\\mathrm{Arrow}(C),\\; e:f\\cong g \\Rightarrow (P(\\mathrm{hom}(f)) \\Rightarrow P(\\mathrm{hom}(g)))\\big) \\Rightarrow \\mathrm{RespectsIso}(P).$$$

Lean4

theorem of_respects_arrow_iso (P : MorphismProperty C) (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) :
    RespectsIso P
    where
  precomp {X Y Z} e (he : IsIso e) f
    hf := by
    refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf
    simp
  postcomp {X Y Z} e (he : IsIso e) f
    hf := by
    refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf
    simp

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