rightOp — Mathlib

English

If W is inverted by L in the original category, then W.op is inverted by L.rightOp.

Русский

Если W разворачивается по L в исходной категории, то W.op разворачивается по L.rightOp.

LaTeX

$$$ W.IsInvertedBy L \Rightarrow W.op.IsInvertedBy L.rightOp $$$

Lean4

theorem rightOp {W : MorphismProperty C} {L : Cᵒᵖ ⥤ D} (h : W.op.IsInvertedBy L) : W.IsInvertedBy L.rightOp :=
  fun X Y f hf => by
  haveI := h f.op hf
  dsimp
  infer_instance

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