Opposites #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.
- 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.)
Instances for opposite
- opposite.inhabited
- quiver.opposite
- category_theory.category.opposite
- category_theory.limits.has_initial_op_of_has_terminal
- category_theory.limits.has_terminal_op_of_has_initial
- category_theory.limits.has_zero_object_op
- category_theory.limits.has_zero_morphisms_opposite
- category_theory.fin_category_opposite
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
A recursor for opposite
. Use as induction x using opposite.rec
.
Equations
- opposite.rec h = λ (X : αᵒᵖ), h (opposite.unop X)