triangleMorphism₁ — Mathlib

English

For the triple-rotation isomorphism, corresponding equalities are verified componentwise using triangle data.

Русский

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

LaTeX

$$$(\\rotate C)^{\\circ 3} \\cong \\Triangle.shiftFunctor C 1$ with explicit verifications$$

Lean4

/-- The first morphism of triangles given by an octahedron. -/
@[simps]
def triangleMorphism₁ : Triangle.mk u₁₂ v₁₂ w₁₂ ⟶ Triangle.mk u₁₃ v₁₃ w₁₃
    where
  hom₁ := 𝟙 X₁
  hom₂ := u₂₃
  hom₃ := h.m₁
  comm₁ := by
    dsimp
    rw [id_comp, comm]
  comm₂ := h.comm₁
  comm₃ := by
    dsimp
    simpa only [Functor.map_id, comp_id] using h.comm₂.symm

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