Mathlib.Data.Opposite

Opposite structure

Full source

/-- 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.
-/
structure Opposite where
  /-- The canonical map `α → αᵒᵖ`. -/
  op ::
  /-- The canonical map `αᵒᵖ → α`. -/
  unop : α

Opposite type

Informal description

The structure `Opposite α` represents the opposite of a type `α`, consisting of a single field of type `α` and two bijections `op : α → αᵒᵖ` and `unop : αᵒᵖ → α`. If `α` is a category, then `αᵒᵖ` is the opposite category, with all arrows reversed. The bijections satisfy `unop (op X) = X` and `op (unop X) = X` definitionally.

Opposite.unexpander_op definition

: Lean.PrettyPrinter.Unexpander

Full source

/-- Make sure that `Opposite.op a` is pretty-printed as `op a` instead of `{ unop := a }` or
`⟨a⟩`. -/
@[app_unexpander Opposite.op]
protected def Opposite.unexpander_op : Lean.PrettyPrinter.Unexpander
  | s => pure s

Unexpander for opposite operation

Informal description

The unexpander function ensures that the pretty-printing of `Opposite.op a` appears as `op a` rather than displaying the underlying structure representation like `{ unop := a }` or `⟨a⟩`.

term_ᵒᵖ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:max -- Use a high right binding power (like that of postfix ⁻¹) so that, for example,
-- `Presheaf Cᵒᵖ` parses as `Presheaf (Cᵒᵖ)` and not `(Presheaf C)ᵒᵖ`.
α "ᵒᵖ" => Opposite α

Opposite type notation

Informal description

The notation `αᵒᵖ` represents the opposite structure of `α`, which is a type containing a single field of type `α`. The notation is used to denote the opposite category when `α` is a category, where all morphisms are reversed.

Opposite.op_injective theorem

: Function.Injective (op : α → αᵒᵖ)

Full source

theorem op_injective : Function.Injective (op : α → αᵒᵖ) := fun _ _ => congr_arg Opposite.unop

Injectivity of the Opposite Construction Map

Informal description

The function $\mathrm{op} : \alpha \to \alpha^\mathrm{op}$ is injective. That is, for any $x, y \in \alpha$, if $\mathrm{op}(x) = \mathrm{op}(y)$, then $x = y$.

Opposite.unop_injective theorem

: Function.Injective (unop : αᵒᵖ → α)

Full source

theorem unop_injective : Function.Injective (unop : αᵒᵖ → α) := fun ⟨_⟩⟨_⟩ => by simp

Injectivity of the Opposite Unconstruction Map

Informal description

The function $\mathrm{unop} : \alpha^\mathrm{op} \to \alpha$ is injective. That is, for any $x, y \in \alpha^\mathrm{op}$, if $\mathrm{unop}(x) = \mathrm{unop}(y)$, then $x = y$.

Opposite.op_unop theorem

(x : αᵒᵖ) : op (unop x) = x

Full source

@[simp]
theorem op_unop (x : αᵒᵖ) : op (unop x) = x :=
  rfl

Opposite Construction Identity: $\mathrm{op} \circ \mathrm{unop} = \mathrm{id}$

Informal description

For any element $x$ in the opposite type $\alpha^\mathrm{op}$, applying the operation $\mathrm{op}$ to the result of $\mathrm{unop}(x)$ yields $x$ itself, i.e., $\mathrm{op}(\mathrm{unop}(x)) = x$.

Opposite.unop_op theorem

(x : α) : unop (op x) = x

Full source

theorem unop_op (x : α) : unop (op x) = x :=
  rfl

Opposite Construction Identity: $\mathrm{unop} \circ \mathrm{op} = \mathrm{id}$

Informal description

For any element $x$ of type $\alpha$, applying the operation $\mathrm{unop}$ to the result of $\mathrm{op}(x)$ yields $x$ itself, i.e., $\mathrm{unop}(\mathrm{op}(x)) = x$.

Opposite.op_inj_iff theorem

(x y : α) : op x = op y ↔ x = y

Full source

theorem op_inj_iff (x y : α) : opop x = op y ↔ x = y :=
  op_injective.eq_iff

Injectivity Criterion for Opposite Construction: $\mathrm{op}(x) = \mathrm{op}(y) \leftrightarrow x = y$

Informal description

For any elements $x, y$ of type $\alpha$, the equality $\mathrm{op}(x) = \mathrm{op}(y)$ holds if and only if $x = y$.

Opposite.unop_inj_iff theorem

(x y : αᵒᵖ) : unop x = unop y ↔ x = y

Full source

@[simp]
theorem unop_inj_iff (x y : αᵒᵖ) : unopunop x = unop y ↔ x = y :=
  unop_injective.eq_iff

Injectivity Criterion for Opposite Unconstruction: $\mathrm{unop}(x) = \mathrm{unop}(y) \leftrightarrow x = y$

Informal description

For any elements $x, y$ in the opposite type $\alpha^\mathrm{op}$, the equality $\mathrm{unop}(x) = \mathrm{unop}(y)$ holds if and only if $x = y$.

Opposite.equivToOpposite definition

: α ≃ αᵒᵖ

Full source

/-- The type-level equivalence between a type and its opposite. -/
def equivToOpposite : α ≃ αᵒᵖ where
  toFun := op
  invFun := unop
  left_inv := unop_op
  right_inv := op_unop

Equivalence between a type and its opposite

Informal description

The equivalence $\alpha \simeq \alpha^\mathrm{op}$ between a type $\alpha$ and its opposite type $\alpha^\mathrm{op}$, given by the bijection $\mathrm{op} : \alpha \to \alpha^\mathrm{op}$ with inverse $\mathrm{unop} : \alpha^\mathrm{op} \to \alpha$, satisfying $\mathrm{unop} \circ \mathrm{op} = \mathrm{id}$ and $\mathrm{op} \circ \mathrm{unop} = \mathrm{id}$.

Opposite.op_surjective theorem

: Function.Surjective (op : α → αᵒᵖ)

Full source

theorem op_surjective : Function.Surjective (op : α → αᵒᵖ) := equivToOpposite.surjective

Surjectivity of the Opposite Map $\mathrm{op} : \alpha \to \alpha^\mathrm{op}$

Informal description

The canonical map $\mathrm{op} : \alpha \to \alpha^\mathrm{op}$ from a type $\alpha$ to its opposite type $\alpha^\mathrm{op}$ is surjective. That is, for every element $X \in \alpha^\mathrm{op}$, there exists an element $x \in \alpha$ such that $\mathrm{op}(x) = X$.

Opposite.unop_surjective theorem

: Function.Surjective (unop : αᵒᵖ → α)

Full source

theorem unop_surjective : Function.Surjective (unop : αᵒᵖ → α) := equivToOpposite.symm.surjective

Surjectivity of the Unop Function from Opposite Type

Informal description

The function $\mathrm{unop} : \alpha^\mathrm{op} \to \alpha$ is surjective, meaning for every element $a \in \alpha$, there exists an element $X \in \alpha^\mathrm{op}$ such that $\mathrm{unop}(X) = a$.

Opposite.equivToOpposite_coe theorem

: (equivToOpposite : α → αᵒᵖ) = op

Full source

@[simp]
theorem equivToOpposite_coe : (equivToOpposite : α → αᵒᵖ) = op :=
  rfl

Equivalence to Opposite Type Coincides with Canonical Map

Informal description

The equivalence map $\alpha \simeq \alpha^\mathrm{op}$ between a type $\alpha$ and its opposite type $\alpha^\mathrm{op}$ is equal to the canonical map $\mathrm{op} : \alpha \to \alpha^\mathrm{op}$.

Opposite.equivToOpposite_symm_coe theorem

: (equivToOpposite.symm : αᵒᵖ → α) = unop

Full source

@[simp]
theorem equivToOpposite_symm_coe : (equivToOpposite.symm : αᵒᵖ → α) = unop :=
  rfl

Inverse Equivalence to Opposite Type Coincides with Canonical Unop Map

Informal description

The inverse of the equivalence between a type $\alpha$ and its opposite $\alpha^\mathrm{op}$ is equal to the canonical map $\mathrm{unop} : \alpha^\mathrm{op} \to \alpha$.

Opposite.op_eq_iff_eq_unop theorem

{x : α} {y} : op x = y ↔ x = unop y

Full source

theorem op_eq_iff_eq_unop {x : α} {y} : opop x = y ↔ x = unop y :=
  equivToOpposite.apply_eq_iff_eq_symm_apply

Equivalence between $\mathrm{op}$ and $\mathrm{unop}$ operations

Informal description

For any element $x$ of type $\alpha$ and any element $y$ of type $\alpha^\mathrm{op}$, the equality $\mathrm{op}(x) = y$ holds if and only if $x = \mathrm{unop}(y)$.

Opposite.unop_eq_iff_eq_op theorem

{x} {y : α} : unop x = y ↔ x = op y

Full source

theorem unop_eq_iff_eq_op {x} {y : α} : unopunop x = y ↔ x = op y :=
  equivToOpposite.symm.apply_eq_iff_eq_symm_apply

Equivalence between $\mathrm{unop}(x) = y$ and $x = \mathrm{op}(y)$ in the opposite type

Informal description

For any element $x$ in the opposite type $\alpha^\mathrm{op}$ and any element $y$ in $\alpha$, the equality $\mathrm{unop}(x) = y$ holds if and only if $x = \mathrm{op}(y)$.

Opposite.instInhabited instance

[Inhabited α] : Inhabited αᵒᵖ

Full source

instance [Inhabited α] : Inhabited αᵒᵖ :=
  ⟨op default⟩

Opposite Type Inherits Inhabitedness

Informal description

For any type $\alpha$ with an inhabited instance, the opposite type $\alpha^{\text{op}}$ is also inhabited.

Opposite.instNonempty instance

[Nonempty α] : Nonempty αᵒᵖ

Full source

instance [Nonempty α] : Nonempty αᵒᵖ := Nonempty.map op ‹_›

Nonempty Opposite Type

Informal description

For any nonempty type $\alpha$, the opposite type $\alpha^{\text{op}}$ is also nonempty.

Opposite.instSubsingleton instance

[Subsingleton α] : Subsingleton αᵒᵖ

Full source

instance [Subsingleton α] : Subsingleton αᵒᵖ := unop_injective.subsingleton

Opposite Type Preserves Subsingleton Property

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements of $\alpha$ are equal), the opposite type $\alpha^\mathrm{op}$ is also a subsingleton.

Opposite.rec' definition

{F : αᵒᵖ → Sort v} (h : ∀ X, F (op X)) : ∀ X, F X

Full source

/-- A deprecated alias for `Opposite.rec`. -/
@[deprecated Opposite.rec (since := "2025-04-04")]
protected def rec' {F : αᵒᵖ → Sort v} (h : ∀ X, F (op X)) : ∀ X, F X := fun X => h (unop X)

Recursor for opposite type

Informal description

Given a type family `F : αᵒᵖ → Sort v` and a function `h : ∀ X, F (op X)`, the function `Opposite.rec'` constructs a function that maps any element `X` of the opposite type `αᵒᵖ` to `F X` by applying `h` to the unopposite of `X`. This satisfies `Opposite.rec' h (op X) = h X` definitionally.

Opposite.small theorem

{X : Type v} [Small.{u} X] : Small.{u} Xᵒᵖ

Full source

/-- If `X` is `u`-small, also `Xᵒᵖ` is `u`-small.
Note: This is not an instance, because it tends to mislead typeclass search. -/
lemma small {X : Type v} [Small.{u} X] : Small.{u} Xᵒᵖ := by
  obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)
  exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩

Opposite type preserves smallness

Informal description

If a type $X$ is $u$-small (i.e., there exists a bijection between $X$ and some type in the universe `Type u`), then its opposite type $X^\mathrm{op}$ is also $u$-small.