Opposites

📁 Source: Mathlib/CategoryTheory/Adjunction/Opposites.lean

Statistics

Metric	Count
Definitions leftAdjointsCoyonedaEquiv, leftOp, natIsoOfLeftAdjointNatIso, natIsoOfRightAdjointNatIso, op, rightOp, unop	7
Theorems leftOp_counit, leftOp_eq, leftOp_unit, op_counit, op_unit, rightOp_counit, rightOp_eq, rightOp_unit, unop_counit, unop_unit, leftOp, op, rightOp, leftOp, op, rightOp	16
Total	23

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
leftAdjointsCoyonedaEquiv 📖	CompOp	—
leftOp 📖	CompOp	3 math math: leftOp_unit, leftOp_counit, leftOp_eq
natIsoOfLeftAdjointNatIso 📖	CompOp	—
natIsoOfRightAdjointNatIso 📖	CompOp	—
op 📖	CompOp	10 math math: Triple.op_adj₁, Triple.op_adj₂, rightOp_eq, op_unit, CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int, leftOp_eq, Quadruple.op_adj₁, op_counit, Quadruple.op_adj₂, Quadruple.op_adj₃
rightOp 📖	CompOp	3 math math: rightOp_counit, rightOp_eq, rightOp_unit
unop 📖	CompOp	2 math math: unop_counit, unop_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftOp_counit 📖	mathematical	—	counit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp leftOp CategoryTheory.NatTrans.op CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	—
leftOp_eq 📖	mathematical	—	leftOp comp Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm CategoryTheory.opOpEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.op CategoryTheory.Functor.leftOp CategoryTheory.Equivalence.toAdjunction op	—	ext CategoryTheory.NatTrans.ext' comp_unit_app CategoryTheory.Category.id_comp
leftOp_unit 📖	mathematical	—	unit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp leftOp CategoryTheory.NatTrans.unop CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	—
op_counit 📖	mathematical	—	counit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.NatTrans.op CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	—
op_unit 📖	mathematical	—	unit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.NatTrans.op CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	—
rightOp_counit 📖	mathematical	—	counit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp rightOp CategoryTheory.NatTrans.op CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	—
rightOp_eq 📖	mathematical	—	rightOp comp Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm CategoryTheory.opOpEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.op CategoryTheory.Functor.rightOp CategoryTheory.Equivalence.toAdjunction op	—	ext CategoryTheory.NatTrans.ext' comp_unit_app CategoryTheory.Category.id_comp
rightOp_unit 📖	mathematical	—	unit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp rightOp CategoryTheory.NatTrans.unop CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	—
unop_counit 📖	mathematical	—	counit CategoryTheory.Functor.unop unop CategoryTheory.NatTrans.unop CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp unit	—	—
unop_unit 📖	mathematical	—	unit CategoryTheory.Functor.unop unop CategoryTheory.NatTrans.unop CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id counit	—	—

CategoryTheory.Functor.IsLeftAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftOp 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
op 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
rightOp 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	CategoryTheory.Functor.isRightAdjoint_comp CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse op

CategoryTheory.Functor.IsRightAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftOp 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	CategoryTheory.Functor.isLeftAdjoint_comp op CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor
op 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
rightOp 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—

---

← Back to Index