Opposites
In this file we define a type synonym opposite α := α
, denoted by αᵒᵖ
and two synonyms for the
identity map, op : α → αᵒᵖ
and unop : αᵒᵖ → α
. The type tag αᵒᵖ
is used with two different
meanings:
if
α
is a category, thenαᵒᵖ
is the opposite category, with all arrows reversed;if
α
is a monoid (group, etc), thenαᵒᵖ
is the opposite monoid (group, etc) withop (x * y) = op x * op y
.
The type of objects of the opposite of α
; used to define the opposite category or group.
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.
- Define
opposite α := α
. - Define the isomorphisms
op : α → opposite α
,unop : opposite α → α
. Make the definition
opposite
irreducible.This has the following consequences.
opposite α
andα
are distinct types in the elaborator, so you must useop
andunop
explicitly to convert between them.Both
unop (op X) = X
andop (unop X) = X
are definitional equalities. Notably, every object of the opposite category is definitionally of the formop X
, which greatly simplifies the definition of the structure of the opposite category, for example.(If Lean supported definitional eta equality for records, we could achieve the same goals using a structure with one field.)
The canonical map αᵒᵖ → α
.
Equations
The type-level equivalence between a type and its opposite.
Equations
- opposite.equiv_to_opposite = {to_fun := opposite.op α, inv_fun := opposite.unop α, left_inv := _, right_inv := _}
Equations
- opposite.inhabited = {default := opposite.op (default α)}
Equations
- opposite.op_induction h = λ (X : αᵒᵖ), h (opposite.unop X)
Find the first hypothesis of type opposite _
. Fail if no such hypothesis exist in the local
context.