Documentation

Mathlib.Data.Opposite

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.

structure Opposite (α : Sort u) :
Sort (max 1 u)
  • unop : α

    The canonical map αᵒᵖ → α.

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.

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
    Instances For
      def Opposite.op {α : Sort u} (x : α) :

      The canonical map α → αᵒᵖ.

      Equations
      Instances For
        theorem Opposite.unop_injective {α : Sort u} :
        Function.Injective Opposite.unop
        @[simp]
        theorem Opposite.op_unop {α : Sort u} (x : αᵒᵖ) :
        Opposite.op x.unop = x
        @[simp]
        theorem Opposite.unop_op {α : Sort u} (x : α) :
        (Opposite.op x).unop = x
        @[simp]
        theorem Opposite.op_inj_iff {α : Sort u} (x : α) (y : α) :
        @[simp]
        theorem Opposite.unop_inj_iff {α : Sort u} (x : αᵒᵖ) (y : αᵒᵖ) :
        x.unop = y.unop x = y

        The type-level equivalence between a type and its opposite.

        Equations
        • Opposite.equivToOpposite = { toFun := Opposite.op, invFun := Opposite.unop, left_inv := (_ : ∀ (x : α), (Opposite.op x).unop = x), right_inv := (_ : ∀ (x : αᵒᵖ), Opposite.op x.unop = x) }
        Instances For
          @[simp]
          theorem Opposite.equivToOpposite_coe {α : Sort u} :
          Opposite.equivToOpposite = Opposite.op
          @[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 = y.unop
          theorem Opposite.unop_eq_iff_eq_op {α : Sort u} {x : αᵒᵖ} {y : α} :
          x.unop = y x = Opposite.op y
          Equations
          • Opposite.instInhabitedOpposite = { default := Opposite.op default }
          def Opposite.rec' {α : Sort u} {F : αᵒᵖSort v} (h : (X : α) → F (Opposite.op X)) (X : αᵒᵖ) :
          F X

          A recursor for Opposite. The @[eliminator] attribute makes it the default induction principle for Opposite so you don't need to use induction x using Opposite.rec'.

          Equations
          Instances For