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) with op (x * y) = op x * op y.

source

def opposite (α : Sort u) :

Sort u

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 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.

(If Lean supported definitional eta equality for records, we could achieve the same goals using a structure with one field.)

Equations

αᵒᵖ = α

source

def opposite.op {α : Sort u} :

α → αᵒᵖ

The canonical map α → αᵒᵖ.

Equations

opposite.op = id

source

def opposite.unop {α : Sort u} :

αᵒᵖ → α

The canonical map αᵒᵖ → α.

Equations

opposite.unop = id

source

theorem opposite.op_injective {α : Sort u} :

function.injective opposite.op

source

theorem opposite.unop_injective {α : Sort u} :

function.injective opposite.unop

source

@[simp]

theorem opposite.op_inj_iff {α : Sort u} (x y : α) :

opposite.op x = opposite.op y ↔ x = y

source

@[simp]

theorem opposite.unop_inj_iff {α : Sort u} (x y : αᵒᵖ) :

opposite.unop x = opposite.unop y ↔ x = y

source

@[simp]

theorem opposite.op_unop {α : Sort u} (x : αᵒᵖ) :

opposite.op (opposite.unop x) = x

source

@[simp]

theorem opposite.unop_op {α : Sort u} (x : α) :

opposite.unop (opposite.op x) = x

source

def opposite.equiv_to_opposite {α : Sort u} :

α ≃ αᵒᵖ

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 := _}

source

@[simp]

theorem opposite.equiv_to_opposite_coe {α : Sort u} :

⇑opposite.equiv_to_opposite = opposite.op

source

@[simp]

theorem opposite.equiv_to_opposite_symm_coe {α : Sort u} :

⇑(opposite.equiv_to_opposite.symm) = opposite.unop

source

theorem opposite.op_eq_iff_eq_unop {α : Sort u} {x : α} {y : αᵒᵖ} :

opposite.op x = y ↔ x = opposite.unop y

source

theorem opposite.unop_eq_iff_eq_op {α : Sort u} {x : αᵒᵖ} {y : α} :

opposite.unop x = y ↔ x = opposite.op y

source

@[instance]

def opposite.inhabited {α : Sort u} [inhabited α] :

inhabited αᵒᵖ

Equations

opposite.inhabited = {default := opposite.op (default α)}

source

@[simp]

def opposite.rec {α : Sort u} {F : αᵒᵖ → Sort v} (h : Π (X : α), F (opposite.op X)) (X : αᵒᵖ) :

F X

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

Equations

opposite.rec h = λ (X : αᵒᵖ), h (opposite.unop X)

source

meta def tactic.op_induction.is_opposite (e : expr) :

tactic bool

Test if e : expr is of type opposite α for some α.

source

meta def tactic.op_induction.find_opposite_hyp :

tactic name

Find the first hypothesis of type opposite _. Fail if no such hypothesis exist in the local context.

source

meta def tactic.op_induction' :

tactic unit

A version of induction x using opposite.rec which finds the appropriate hypothesis automatically, for use with local attribute [tidy] op_induction'. This is necessary because induction x is not able to deduce that opposite.rec should be used.