Rotate

📁 Source: Mathlib/CategoryTheory/Triangulated/Rotate.lean

Statistics

Metric	Count
Definitions invRotate, rotate, invRotCompRot, invRotate, rotCompInvRot, rotate, triangleRotation	7
Theorems invRotate_mor₁, invRotate_mor₂, invRotate_mor₃, invRotate_obj₁, invRotate_obj₂, invRotate_obj₃, rotate_mor₁, rotate_mor₂, rotate_mor₃, rotate_obj₁, rotate_obj₂, rotate_obj₃, instIsEquivalenceTriangleInvRotate, instIsEquivalenceTriangleRotate, invRotCompRot_hom_app_hom₁, invRotCompRot_hom_app_hom₂, invRotCompRot_hom_app_hom₃, invRotCompRot_inv_app_hom₁, invRotCompRot_inv_app_hom₂, invRotCompRot_inv_app_hom₃, invRotate_map_hom₁, invRotate_map_hom₂, invRotate_map_hom₃, invRotate_obj, rotCompInvRot_hom_app_hom₁, rotCompInvRot_hom_app_hom₂, rotCompInvRot_hom_app_hom₃, rotCompInvRot_inv_app_hom₁, rotCompInvRot_inv_app_hom₂, rotCompInvRot_inv_app_hom₃, rotate_map_hom₁, rotate_map_hom₂, rotate_map_hom₃, rotate_obj, triangleRotation_counitIso, triangleRotation_functor, triangleRotation_inverse, triangleRotation_unitIso	38
Total	45

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
invRotCompRot 📖	CompOp	7 math math: triangleRotation_counitIso, invRotCompRot_inv_app_hom₃, invRotCompRot_hom_app_hom₂, invRotCompRot_inv_app_hom₁, invRotCompRot_hom_app_hom₃, invRotCompRot_inv_app_hom₂, invRotCompRot_hom_app_hom₁
invRotate 📖	CompOp	24 math math: rotCompInvRot_hom_app_hom₃, rotCompInvRot_inv_app_hom₂, invRotCompRot_inv_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃, invRotate_map_hom₁, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂, rotCompInvRot_inv_app_hom₃, CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁, invRotCompRot_hom_app_hom₂, invRotCompRot_inv_app_hom₁, invRotate_map_hom₂, rotCompInvRot_inv_app_hom₁, invRotCompRot_hom_app_hom₃, rotCompInvRot_hom_app_hom₂, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁, invRotate_map_hom₃, triangleRotation_inverse, CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂, invRotCompRot_inv_app_hom₂, rotCompInvRot_hom_app_hom₁, invRotate_obj, invRotCompRot_hom_app_hom₁, instIsEquivalenceTriangleInvRotate
rotCompInvRot 📖	CompOp	7 math math: rotCompInvRot_hom_app_hom₃, rotCompInvRot_inv_app_hom₂, triangleRotation_unitIso, rotCompInvRot_inv_app_hom₃, rotCompInvRot_inv_app_hom₁, rotCompInvRot_hom_app_hom₂, rotCompInvRot_hom_app_hom₁
rotate 📖	CompOp	24 math math: rotCompInvRot_hom_app_hom₃, rotCompInvRot_inv_app_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂, invRotCompRot_inv_app_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂, rotCompInvRot_inv_app_hom₃, rotate_map_hom₂, invRotCompRot_hom_app_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃, invRotCompRot_inv_app_hom₁, rotate_map_hom₃, CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁, rotCompInvRot_inv_app_hom₁, rotate_map_hom₁, invRotCompRot_hom_app_hom₃, rotate_obj, rotCompInvRot_hom_app_hom₂, CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃, triangleRotation_functor, invRotCompRot_inv_app_hom₂, rotCompInvRot_hom_app_hom₁, invRotCompRot_hom_app_hom₁, instIsEquivalenceTriangleRotate
triangleRotation 📖	CompOp	4 math math: triangleRotation_counitIso, triangleRotation_unitIso, triangleRotation_inverse, triangleRotation_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsEquivalenceTriangleInvRotate 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsEquivalence Triangle triangleCategory invRotate	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsEquivalenceTriangleRotate 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsEquivalence Triangle triangleCategory rotate	—	CategoryTheory.Equivalence.isEquivalence_functor
invRotCompRot_hom_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₁ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp invRotate rotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₁	—	—
invRotCompRot_hom_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₂ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp invRotate rotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₂	—	—
invRotCompRot_hom_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₃ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp invRotate rotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryTheory.shiftFunctorCompIsoId add_neg_cancel Triangle.obj₃	—	—
invRotCompRot_inv_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₁ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp invRotate rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₁	—	—
invRotCompRot_inv_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₂ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp invRotate rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₂	—	—
invRotCompRot_inv_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₃ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp invRotate rotate CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category invRotCompRot SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryTheory.shiftFunctorCompIsoId add_neg_cancel Triangle.obj₃	—	—
invRotate_map_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ Triangle.invRotate CategoryTheory.Functor.map Triangle triangleCategory invRotate CategoryTheory.shiftFunctor Int.instAddMonoid Triangle.obj₃ TriangleMorphism.hom₃	—	—
invRotate_map_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ Triangle.invRotate CategoryTheory.Functor.map Triangle triangleCategory invRotate TriangleMorphism.hom₁	—	—
invRotate_map_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ Triangle.invRotate CategoryTheory.Functor.map Triangle triangleCategory invRotate TriangleMorphism.hom₂	—	—
invRotate_obj 📖	mathematical	—	CategoryTheory.Functor.obj Triangle triangleCategory invRotate Triangle.invRotate	—	—
rotCompInvRot_hom_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₁ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp rotate invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryTheory.Iso.inv CategoryTheory.shiftFunctorCompIsoId add_neg_cancel Triangle.obj₁	—	—
rotCompInvRot_hom_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₂ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp rotate invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₂	—	—
rotCompInvRot_hom_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₃ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp rotate invRotate CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₃	—	—
rotCompInvRot_inv_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₁ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp rotate invRotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryTheory.Iso.hom CategoryTheory.shiftFunctorCompIsoId add_neg_cancel Triangle.obj₁	—	—
rotCompInvRot_inv_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₂ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp rotate invRotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₂	—	—
rotCompInvRot_inv_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	TriangleMorphism.hom₃ CategoryTheory.Functor.obj Triangle triangleCategory CategoryTheory.Functor.comp rotate invRotate CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rotCompInvRot CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Triangle.obj₃	—	—
rotate_map_hom₁ 📖	mathematical	—	TriangleMorphism.hom₁ Triangle.rotate CategoryTheory.Functor.map Triangle triangleCategory rotate TriangleMorphism.hom₂	—	—
rotate_map_hom₂ 📖	mathematical	—	TriangleMorphism.hom₂ Triangle.rotate CategoryTheory.Functor.map Triangle triangleCategory rotate TriangleMorphism.hom₃	—	—
rotate_map_hom₃ 📖	mathematical	—	TriangleMorphism.hom₃ Triangle.rotate CategoryTheory.Functor.map Triangle triangleCategory rotate CategoryTheory.shiftFunctor Int.instAddMonoid Triangle.obj₁ TriangleMorphism.hom₁	—	—
rotate_obj 📖	mathematical	—	CategoryTheory.Functor.obj Triangle triangleCategory rotate Triangle.rotate	—	—
triangleRotation_counitIso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.counitIso Triangle triangleCategory triangleRotation invRotCompRot	—	—
triangleRotation_functor 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.functor Triangle triangleCategory triangleRotation rotate	—	—
triangleRotation_inverse 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.inverse Triangle triangleCategory triangleRotation invRotate	—	—
triangleRotation_unitIso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.unitIso Triangle triangleCategory triangleRotation rotCompInvRot	—	—

CategoryTheory.Pretriangulated.Triangle

Definitions

Name	Category	Theorems
invRotate 📖	CompOp	18 math math: invRotate_mor₃, invRotate_obj₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃, invRotate_obj₃, CategoryTheory.Pretriangulated.invRotate_map_hom₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁, invRotate_mor₁, CategoryTheory.Pretriangulated.invRotate_map_hom₂, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, invRotate_obj₂, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', CategoryTheory.Pretriangulated.invRotate_map_hom₃, CategoryTheory.Pretriangulated.invRotate_obj, invRotate_mor₂
rotate 📖	CompOp	21 math math: rotate_obj₁, rotate_mor₃, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, rotate_mor₁, CategoryTheory.Pretriangulated.rotate_map_hom₂, CategoryTheory.Pretriangulated.rotate_map_hom₃, rotate_obj₃, CategoryTheory.Functor.rotate_essImageDistTriang, CategoryTheory.Pretriangulated.rotate_map_hom₁, CochainComplex.mappingCone.triangleRotateShortComplex_g, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', rotate_mor₂, CategoryTheory.Pretriangulated.rotate_obj, rotate_obj₂, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, CategoryTheory.Pretriangulated.rot_of_distTriang, CochainComplex.mappingCone.triangleRotateShortComplex_f, CategoryTheory.Pretriangulated.Opposite.rotate_distinguished_triangle, CategoryTheory.Pretriangulated.rotate_distinguished_triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invRotate_mor₁ 📖	mathematical	—	mor₁ invRotate Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₃ obj₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map mor₃ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup AddGroup.toSubtractionMonoid CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId add_neg_cancel	—	—
invRotate_mor₂ 📖	mathematical	—	mor₂ invRotate mor₁	—	—
invRotate_mor₃ 📖	mathematical	—	mor₃ invRotate CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₂ obj₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid mor₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId add_neg_cancel	—	—
invRotate_obj₁ 📖	mathematical	—	obj₁ invRotate CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₃	—	—
invRotate_obj₂ 📖	mathematical	—	obj₂ invRotate obj₁	—	—
invRotate_obj₃ 📖	mathematical	—	obj₃ invRotate obj₂	—	—
rotate_mor₁ 📖	mathematical	—	mor₁ rotate mor₂	—	—
rotate_mor₂ 📖	mathematical	—	mor₂ rotate mor₃	—	—
rotate_mor₃ 📖	mathematical	—	mor₃ rotate Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₁ obj₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.map mor₁	—	—
rotate_obj₁ 📖	mathematical	—	obj₁ rotate obj₂	—	—
rotate_obj₂ 📖	mathematical	—	obj₂ rotate obj₃	—	—
rotate_obj₃ 📖	mathematical	—	obj₃ rotate CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₁	—	—

---

← Back to Index