op — Mathlib · SciLib

English

Opposite direction: lifting property for opposite arrows implies lifting property for the original arrows when moving back via unop.

Русский

Обратное направление: свойство подъёма для противоположных стрелок означает подъём для исходных стрелок при возвращении через unop.

LaTeX

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

Lean4

theorem op (h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op :=
  ⟨fun {f} {g} sq => by
    simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
    infer_instance⟩

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