Documentation Verification Report

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftOp` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.leftOp`	—	—
`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