Mathlib Map

Structures · Category theory

CategoryTheory.Functor.IsTriangulated

A functor which commutes with the shift by is triangulated if it sends distinguished triangles to distinguished triangles.

Defined in
Mathlib.CategoryTheory.Triangulated.Functor
Shape
One type argument · adds map_distinguished

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Concrete types that are instances5

  • CategoryTheory.ObjectProperty.FullSubcategory
  • HomotopyCategory
  • DerivedCategory
  • HomotopyCategory.Plus
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by40

Ancestors0

No ancestors.