Opposite

📁 Source: Mathlib/CategoryTheory/Enriched/Opposite.lean

Statistics

Metric	Count
Definitions opposite, opposite, forgetEnrichmentOppositeEquivalence, functor, inverse	5
Theorems eComp_op_eq, eComp_op_eq_assoc, forgetEnrichmentOppositeEquivalence_counitIso, forgetEnrichmentOppositeEquivalence_functor, forgetEnrichmentOppositeEquivalence_inverse, forgetEnrichmentOppositeEquivalence_unitIso, tensorHom_eComp_op_eq, tensorHom_eComp_op_eq_assoc	8
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
forgetEnrichmentOppositeEquivalence 📖	CompOp	4 math math: forgetEnrichmentOppositeEquivalence_functor, forgetEnrichmentOppositeEquivalence_unitIso, forgetEnrichmentOppositeEquivalence_counitIso, forgetEnrichmentOppositeEquivalence_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eComp_op_eq 📖	mathematical	—	eComp Opposite EnrichedCategory.opposite CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Opposite.unop Iso.hom BraidedCategory.braiding	—	—
eComp_op_eq_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Opposite EnrichedCategory.opposite eComp Opposite.unop Iso.hom BraidedCategory.braiding	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eComp_op_eq
forgetEnrichmentOppositeEquivalence_counitIso 📖	mathematical	—	Equivalence.counitIso ForgetEnrichment Opposite EnrichedCategory.opposite categoryForgetEnrichment Category.opposite forgetEnrichmentOppositeEquivalence NatIso.ofComponents Functor.comp forgetEnrichmentOppositeEquivalence.inverse forgetEnrichmentOppositeEquivalence.functor Functor.id Iso.refl Functor.obj	—	—
forgetEnrichmentOppositeEquivalence_functor 📖	mathematical	—	Equivalence.functor ForgetEnrichment Opposite EnrichedCategory.opposite categoryForgetEnrichment Category.opposite forgetEnrichmentOppositeEquivalence forgetEnrichmentOppositeEquivalence.functor	—	—
forgetEnrichmentOppositeEquivalence_inverse 📖	mathematical	—	Equivalence.inverse ForgetEnrichment Opposite EnrichedCategory.opposite categoryForgetEnrichment Category.opposite forgetEnrichmentOppositeEquivalence forgetEnrichmentOppositeEquivalence.inverse	—	—
forgetEnrichmentOppositeEquivalence_unitIso 📖	mathematical	—	Equivalence.unitIso ForgetEnrichment Opposite EnrichedCategory.opposite categoryForgetEnrichment Category.opposite forgetEnrichmentOppositeEquivalence NatIso.ofComponents Functor.id Functor.comp forgetEnrichmentOppositeEquivalence.functor forgetEnrichmentOppositeEquivalence.inverse Iso.refl Functor.obj	—	—
tensorHom_eComp_op_eq 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Opposite EnrichedCategory.opposite MonoidalCategoryStruct.tensorHom eComp Opposite.unop Iso.hom BraidedCategory.braiding	—	eComp_op_eq BraidedCategory.braiding_naturality_assoc
tensorHom_eComp_op_eq_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Opposite EnrichedCategory.opposite MonoidalCategoryStruct.tensorHom eComp Iso.hom BraidedCategory.braiding Opposite.unop	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_eComp_op_eq

CategoryTheory.EnrichedCategory

Definitions

Name	Category	Theorems
opposite 📖	CompOp	8 math math: CategoryTheory.forgetEnrichmentOppositeEquivalence_functor, CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso, CategoryTheory.eComp_op_eq_assoc, CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso, CategoryTheory.tensorHom_eComp_op_eq_assoc, CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse, CategoryTheory.tensorHom_eComp_op_eq, CategoryTheory.eComp_op_eq

CategoryTheory.EnrichedOrdinaryCategory

Definitions

Name	Category	Theorems
opposite 📖	CompOp	—

CategoryTheory.forgetEnrichmentOppositeEquivalence

Definitions

Name	Category	Theorems
functor 📖	CompOp	3 math math: CategoryTheory.forgetEnrichmentOppositeEquivalence_functor, CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso, CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso
inverse 📖	CompOp	3 math math: CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso, CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso, CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse

---

← Back to Index