# Documentation

Mathlib.Data.Opposite

# Opposites #

In this file we define a type synonym Opposite α := α, denoted by αᵒᵖ and two synonyms for the identity map, op : α → αᵒᵖ and unop : αᵒᵖ → α. If α is a category, then αᵒᵖ is the opposite category, with all arrows reversed.

def Opposite (α : Sort u) :

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

In order to avoid confusion between α and its opposite type, we set up the type of objects Opposite α using the following pattern, which will be repeated later for the morphisms.

1. Define Opposite α := α.
2. Define the isomorphisms op : α → Opposite α, unop : Opposite α → α.
3. Make the definition Opposite irreducible.

This has the following consequences.

• Opposite α and α are distinct types in the elaborator, so you must use op and unop explicitly to convert between them.
• Both unop (op X) = X and op (unop X) = X are definitional equalities. Notably, every object of the opposite category is definitionally of the form op X, which greatly simplifies the definition of the structure of the opposite category, for example.

(Now that Lean 4 supports definitional eta equality for records, we could achieve the same goals using a structure with one field.)

Equations

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

In order to avoid confusion between α and its opposite type, we set up the type of objects Opposite α using the following pattern, which will be repeated later for the morphisms.

1. Define Opposite α := α.
2. Define the isomorphisms op : α → Opposite α, unop : Opposite α → α.
3. Make the definition Opposite irreducible.

This has the following consequences.

• Opposite α and α are distinct types in the elaborator, so you must use op and unop explicitly to convert between them.
• Both unop (op X) = X and op (unop X) = X are definitional equalities. Notably, every object of the opposite category is definitionally of the form op X, which greatly simplifies the definition of the structure of the opposite category, for example.

(Now that Lean 4 supports definitional eta equality for records, we could achieve the same goals using a structure with one field.)

Equations
def Opposite.op {α : Sort u} :
ααᵒᵖ

The canonical map α → αᵒᵖ.

Equations
• Opposite.op = id
def Opposite.unop {α : Sort u} :
αᵒᵖα

The canonical map αᵒᵖ → α.

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

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Opposite.equivToOpposite_coe {α : Sort u} :
Opposite.equivToOpposite = Opposite.op
@[simp]
theorem Opposite.equivToOpposite_symm_coe {α : Sort u} :
↑(Equiv.symm Opposite.equivToOpposite) = Opposite.unop
theorem Opposite.op_eq_iff_eq_unop {α : Sort u} {x : α} {y : αᵒᵖ} :
= y
theorem Opposite.unop_eq_iff_eq_op {α : Sort u} {x : αᵒᵖ} {y : α} :
x =
instance Opposite.instInhabitedOpposite {α : Sort u} [inst : ] :
Equations
• Opposite.instInhabitedOpposite = { default := Opposite.op default }
def Opposite.rec {α : Sort u} {F : αᵒᵖSort v} (h : (X : α) → F ()) (X : αᵒᵖ) :
F X

A recursor for Opposite. Use as induction x using Opposite.rec.

Equations
• = h ()