triangleMorphismId — Mathlib

English

The identity triangle has identity components on hom₁, hom₂, hom₃.

Русский

У тождественной треугольной структуры все компоненты гомоморфизмов равны тождественным.

LaTeX

$$$\mathrm{Triangle}.id_{A}.hom_{i} = \mathrm{Id}_{A_{i}}$ для i = 1,2,3.$$

Lean4

/-- The identity triangle morphism.
-/
@[simps]
def triangleMorphismId (T : Triangle C) : TriangleMorphism T T
    where
  hom₁ := 𝟙 T.obj₁
  hom₂ := 𝟙 T.obj₂
  hom₃ := 𝟙 T.obj₃

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