of_arrow_iso — Mathlib

English

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

Русский

Если между стрелами 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{StrongEpi}(f)] \\Rightarrow \\mathrm{StrongEpi}(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 : StrongEpi f] :
    StrongEpi g :=
  { epi := by
      rw [Arrow.iso_w' e]
      infer_instance
    llp := fun {X Y} z => by
      intro
      apply HasLiftingProperty.of_arrow_iso_left e z }

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