of_arrow_iso_left — Mathlib

English

Preservation of lifting under left-arrow iso in the Arrow category.

Русский

Сохранение подъема при левой стрелке-изоморфизме в категории стрелок.

LaTeX

$$$$ HasLiftingProperty\\big( Arrow.mk i \\big)\\; p \\Rightarrow HasLiftingProperty\\big( Arrow.mk i' \\big)\\; p $$$$

Lean4

theorem of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y)
    [hip : HasLiftingProperty i p] : HasLiftingProperty i' p :=
  by
  rw [Arrow.iso_w' e]
  infer_instance

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