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)

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.

• op :: (
• unop : α

  The canonical map αᵒᵖ → α.

• )

Instances For

• CategoryTheory.Category.opposite
• CategoryTheory.Limits.hasCoequalizers_opposite
• CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
• CategoryTheory.Limits.hasColimits_op_of_hasLimits
• CategoryTheory.Limits.hasCoproductsOfShape_opposite
• CategoryTheory.Limits.hasCoproducts_opposite
• CategoryTheory.Limits.hasEqualizers_opposite
• CategoryTheory.Limits.hasFiniteColimits_opposite
• CategoryTheory.Limits.hasFiniteCoproducts_opposite
• CategoryTheory.Limits.hasFiniteLimits_opposite
• CategoryTheory.Limits.hasFiniteProducts_opposite
• CategoryTheory.Limits.hasInitial_op_of_hasTerminal
• CategoryTheory.Limits.hasLimits_op_of_hasColimits
• CategoryTheory.Limits.hasProductsOfShape_opposite
• CategoryTheory.Limits.hasProducts_opposite
• CategoryTheory.Limits.hasPullbacks_opposite
• CategoryTheory.Limits.hasPushouts_opposite
• CategoryTheory.Limits.hasTerminal_op_of_hasInitial
• CategoryTheory.Limits.hasZeroMorphismsOpposite
• CategoryTheory.Limits.hasZeroObject_op
• CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits
• CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits
• CategoryTheory.finCategoryOpposite
• CategoryTheory.instEssentiallySmallOpposite
• CategoryTheory.instIsDiscreteOpposite
• CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty
• CategoryTheory.isCofiltered_op_of_isFiltered
• CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty
• CategoryTheory.isFiltered_op_of_isCofiltered
• Opposite.instInhabited
• Opposite.instNonempty
• Opposite.instSubsingleton
• Quiver.opposite

def Opposite.unexpander_op : Lean.PrettyPrinter.Unexpander

Make sure that Opposite.op a is pretty-printed as op a instead of { unop := a } or ⟨a⟩.

Equations

• Opposite.unexpander_op x = pure x

def «term_ᵒᵖ» : Lean.TrailingParserDescr

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 "ᵒᵖ")

theorem Opposite.op_injective {α : Sort u} : Function.Injective Opposite.op

theorem Opposite.unop_injective {α : Sort u} : Function.Injective Opposite.unop

@[simp]

theorem Opposite.op_unop {α : Sort u} (x : αᵒᵖ) : Opposite.op (Opposite.unop x) = x

theorem Opposite.unop_op {α : Sort u} (x : α) : Opposite.unop (Opposite.op x) = x

theorem Opposite.op_inj_iff {α : Sort u} (x y : α) : Opposite.op x = Opposite.op y ↔ x = y

@[simp]

theorem Opposite.unop_inj_iff {α : Sort u} (x y : αᵒᵖ) : Opposite.unop x = Opposite.unop y ↔ x = y

def Opposite.equivToOpposite {α : Sort u} : α ≃ αᵒᵖ

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

Equations

• Opposite.equivToOpposite = { toFun := Opposite.op, invFun := Opposite.unop, left_inv := ⋯, right_inv := ⋯ }

theorem Opposite.op_surjective {α : Sort u} : Function.Surjective Opposite.op

theorem Opposite.unop_surjective {α : Sort u} : Function.Surjective Opposite.unop

@[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 = Opposite.unop y

theorem Opposite.unop_eq_iff_eq_op {α : Sort u} {x : αᵒᵖ} {y : α} : Opposite.unop x = y ↔ x = Opposite.op y

instance Opposite.instInhabited {α : Sort u} [Inhabited α] : Inhabited αᵒᵖ

Equations

• Opposite.instInhabited = { default := Opposite.op default }

instance Opposite.instNonempty {α : Sort u} [Nonempty α] : Nonempty αᵒᵖ

Equations

• ⋯ = ⋯

instance Opposite.instSubsingleton {α : Sort u} [Subsingleton α] : Subsingleton αᵒᵖ

Equations

• ⋯ = ⋯

def Opposite.rec' {α : Sort u} {F : αᵒᵖ → Sort v} (h : (X : α) → F (Opposite.op X)) (X : αᵒᵖ) : F X

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)