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.
Make sure that Opposite.op a
is pretty-printed as op a
instead of { unop := a }
or
⟨a⟩
.
Equations
Instances For
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
- «term_ᵒᵖ» = Lean.ParserDescr.trailingNode `«term_ᵒᵖ» 1024 0 (Lean.ParserDescr.symbol "ᵒᵖ")
Instances For
@[simp]
@[simp]
@[simp]
theorem
Opposite.equivToOpposite_symm_coe
{α : Sort u}
:
⇑Opposite.equivToOpposite.symm = Opposite.unop
theorem
Opposite.op_eq_iff_eq_unop
{α : Sort u}
{x : α}
{y : αᵒᵖ}
:
Opposite.op x = y ↔ x = Opposite.unop y
theorem
Opposite.unop_eq_iff_eq_op
{α : Sort u}
{x : αᵒᵖ}
{y : α}
:
Opposite.unop x = y ↔ x = Opposite.op y
Equations
- Opposite.instInhabited = { default := Opposite.op default }
A recursor for Opposite
.
The @[induction_eliminator]
attribute makes it the default induction principle for Opposite
so you don't need to use induction x using Opposite.rec'
.
Equations
- Opposite.rec' h X = h (Opposite.unop X)