π₂ — Mathlib

English

The third projection from a triangle to its third component is a functor to the base category, mapping a morphism to its third component.

Русский

Третья проекция треугольника на третий компонент образует функтор в базовую категорию, отображая морфизм в третий компонент.

LaTeX

$$π3 : Triangle C ⥤ C, π3.obj(T) = T.obj3, π3.map(f) = f.hom3$$

Lean4

/-- The second projection `Triangle C ⥤ C`. -/
@[simps]
def π₂ : Triangle C ⥤ C where
  obj T := T.obj₂
  map f := f.hom₂

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