of_arrow_iso — Mathlib

English

If there is an isomorphism between arrows e: Arrow f ≅ Arrow g and f is a strong mono, then g is a strong mono.

Русский

Если между стрелами f и g существует изоморфизм стрел e: Arrow f ≅ Arrow g и f — сильный моно, то и g — сильный моно.

LaTeX

$$$\\forall A,B,A',B',\\; f:A\\to B,\\ g:A'\\to B',\\; e:\\mathrm{Arrow}(f) \\cong \\mathrm{Arrow}(g)\\;\\Rightarrow\\; [\\mathrm{StrongMono}(f)] \\Rightarrow \\mathrm{StrongMono}(g).$$$

Lean4

theorem of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] :
    StrongMono g :=
  { mono := by
      rw [Arrow.iso_w' e]
      infer_instance
    rlp := fun {X Y} z => by
      intro
      apply HasLiftingProperty.of_arrow_iso_right z e }

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