unopEquiv — Mathlib

English

Equivalences of LiftStruct for a square in the opposite category and the corresponding square in the original category.

Русский

Эквиваленции LiftStruct для квадрата в противоположной категории и соответствующего квадрата в исходной.

LaTeX

$$$unopEquiv\ (sq) : LiftStruct\ sq \simeq LiftStruct\ sq.unop$$$

Lean4

/-- Equivalences of `LiftStruct` for a square in the opposite category and
the corresponding square in the original category. -/
def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CommSq f i p g) :
    LiftStruct sq ≃ LiftStruct sq.unop where
  toFun := unop
  invFun := op
  left_inv := by cat_disch
  right_inv := by cat_disch

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