unop — Mathlib

English

HasLiftingProperty i p is equivalent to HasLiftingProperty p.op i.op in the opposite category.

Русский

Свойство подъёма для i, p эквивалентно HasLiftingProperty p^{op} i^{op} в противоположной категории.

LaTeX

$$$$ HasLiftingProperty\, i\, p \\iff HasLiftingProperty\, p^{op}\, i^{op} $$$$

Lean4

theorem unop {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) : HasLiftingProperty p.unop i.unop :=
  ⟨fun {f} {g} sq => by
    rw [CommSq.HasLift.iff_op]
    simp only [Quiver.Hom.op_unop]
    infer_instance⟩

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