contractibleTriangleFunctor — Mathlib

English

The first projection from a triangle to its underlying object behaves as a functor from triangles to the ambient category by taking the first component of the morphism.

Русский

Первая проекция треугольника на его первый компонент гомоморфизма образует функтор из треугольников в исходную категорию, взяв первый компонент морфизма.

LaTeX

$$π1 : Triangle C ⥤ C, π1.obj(T) = T.obj1, π1.map(f) = f.hom1$$

Lean4

/-- The functor `C ⥤ Triangle C` which sends `X` to `contractibleTriangle X`. -/
@[simps]
def contractibleTriangleFunctor [HasZeroObject C] [HasZeroMorphisms C] : C ⥤ Triangle C
    where
  obj X := contractibleTriangle X
  map
    f :=
    { hom₁ := f
      hom₂ := f
      hom₃ := 0 }

Похожие утверждения