Opposite

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

Statistics

Metric	Count
Definitions structuredArrowRightwardsOpEquivalence, functor, inverse	3
Theorems guitartExact_id', guitartExact_op_iff, instGuitartExactOppositeOp, functor_map_left_right, functor_obj_hom_right, functor_obj_left_hom, functor_obj_left_left_as, functor_obj_left_right, functor_obj_right_as, structuredArrowRightwardsOpEquivalence_counitIso, structuredArrowRightwardsOpEquivalence_functor, structuredArrowRightwardsOpEquivalence_inverse, structuredArrowRightwardsOpEquivalence_unitIso	13
Total	16

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
structuredArrowRightwardsOpEquivalence 📖	CompOp	4 math math: structuredArrowRightwardsOpEquivalence_inverse, structuredArrowRightwardsOpEquivalence_counitIso, structuredArrowRightwardsOpEquivalence_unitIso, structuredArrowRightwardsOpEquivalence_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
guitartExact_id' 📖	mathematical	—	GuitartExact CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	guitartExact_op_iff guitartExact_id
guitartExact_op_iff 📖	mathematical	—	GuitartExact Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op	—	ext vComp_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id GuitartExact.vComp guitartExact_of_isEquivalence_of_isIso CategoryTheory.instIsEquivalenceOppositeOpOp CategoryTheory.IsIso.id instGuitartExactOppositeOp CategoryTheory.instIsEquivalenceOppositeUnopUnop
instGuitartExactOppositeOp 📖	mathematical	—	GuitartExact Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op	—	guitartExact_iff_isConnected_rightwards CategoryTheory.isConnected_op_iff_isConnected CategoryTheory.isConnected_iff_of_equivalence instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact
structuredArrowRightwardsOpEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite StructuredArrowRightwards CategoryTheory.Category.opposite CategoryTheory.Functor.op op CostructuredArrowDownwards Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards structuredArrowRightwardsOpEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp structuredArrowRightwardsOpEquivalence.inverse structuredArrowRightwardsOpEquivalence.functor	—	—
structuredArrowRightwardsOpEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite StructuredArrowRightwards CategoryTheory.Category.opposite CategoryTheory.Functor.op op CostructuredArrowDownwards Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards structuredArrowRightwardsOpEquivalence structuredArrowRightwardsOpEquivalence.functor	—	—
structuredArrowRightwardsOpEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite StructuredArrowRightwards CategoryTheory.Category.opposite CategoryTheory.Functor.op op CostructuredArrowDownwards Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards structuredArrowRightwardsOpEquivalence structuredArrowRightwardsOpEquivalence.inverse	—	—
structuredArrowRightwardsOpEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite StructuredArrowRightwards CategoryTheory.Category.opposite CategoryTheory.Functor.op op CostructuredArrowDownwards Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowRightwards CategoryTheory.StructuredArrow structuredArrowDownwards structuredArrowRightwardsOpEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—

CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence

Definitions

Name	Category	Theorems
functor 📖	CompOp	8 math math: functor_obj_hom_right, functor_obj_left_hom, functor_obj_right_as, functor_obj_left_right, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso, functor_map_left_right, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_functor, functor_obj_left_left_as
inverse 📖	CompOp	2 math math: CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_inverse, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_map_left_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.left CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Comma.right CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.TwoSquare.CostructuredArrowDownwards functor Opposite.op CategoryTheory.NatTrans.op CategoryTheory.Functor.comp CategoryTheory.TwoSquare.natTrans	—	—
functor_obj_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj Opposite.unop CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.TwoSquare.structuredArrowDownwards CategoryTheory.Comma.left Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Comma.right CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.TwoSquare.StructuredArrowRightwards Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.TwoSquare.CostructuredArrowDownwards functor Opposite.op CategoryTheory.NatTrans.op CategoryTheory.Functor.comp CategoryTheory.TwoSquare.natTrans CategoryTheory.CommaMorphism.left CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.CostructuredArrow.pre CategoryTheory.Comma.mapLeft Quiver.Hom.op CategoryTheory.Functor.map	—	—
functor_obj_left_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.left CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards functor Opposite.op CategoryTheory.Comma.right CategoryTheory.NatTrans.op CategoryTheory.Functor.comp CategoryTheory.TwoSquare.natTrans	—	—
functor_obj_left_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards functor	—	—
functor_obj_left_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.left CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards functor Opposite.op CategoryTheory.NatTrans.op CategoryTheory.Functor.comp CategoryTheory.TwoSquare.natTrans	—	—
functor_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.StructuredArrow Opposite.unop CategoryTheory.instCategoryStructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.TwoSquare.structuredArrowDownwards CategoryTheory.Functor.fromPUnit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.TwoSquare.StructuredArrowRightwards CategoryTheory.TwoSquare.op CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.TwoSquare.costructuredArrowRightwards CategoryTheory.TwoSquare.CostructuredArrowDownwards functor	—	—

---

← Back to Index