Documentation

Mathlib.Data.Opposite

Opposites #

In this file we define a structure Opposite α containing a single field of type α and two bijections op : α → αᵒᵖ and unop : αᵒᵖ → α. If α is a category, then αᵒᵖ is the opposite category, with all arrows reversed.

structure Opposite (α : Sort u) :
Sort (max 1 u)

The type of objects of the opposite of α; used to define the opposite category.

Now that Lean 4 supports definitional eta equality for records, both unop (op X) = X and op (unop X) = X are definitional equalities.

  • op :: (
    • unop : α

      The canonical map αᵒᵖ → α.

  • )

Make sure that Opposite.op a is pretty-printed as op a instead of { unop := a } or ⟨a⟩.

Equations

The type of objects of the opposite of α; used to define the opposite category.

Now that Lean 4 supports definitional eta equality for records, both unop (op X) = X and op (unop X) = X are definitional equalities.

Equations
@[simp]
theorem Opposite.op_unop {α : Sort u} (x : αᵒᵖ) :
op (unop x) = x
theorem Opposite.unop_op {α : Sort u} (x : α) :
unop (op x) = x
theorem Opposite.op_inj_iff {α : Sort u} (x y : α) :
op x = op y x = y
@[simp]
theorem Opposite.unop_inj_iff {α : Sort u} (x y : αᵒᵖ) :
unop x = unop y x = y

The type-level equivalence between a type and its opposite.

Equations
theorem Opposite.op_eq_iff_eq_unop {α : Sort u} {x : α} {y : αᵒᵖ} :
op x = y x = unop y
theorem Opposite.unop_eq_iff_eq_op {α : Sort u} {x : αᵒᵖ} {y : α} :
unop x = y x = op y
@[deprecated Opposite.rec (since := "2025-04-04")]
def Opposite.rec' {α : Sort u} {F : αᵒᵖSort v} (h : (X : α) → F (op X)) (X : αᵒᵖ) :
F X

A deprecated alias for Opposite.rec.

Equations

If X is u-small, also Xᵒᵖ is u-small. Note: This is not an instance, because it tends to mislead typeclass search.