d₁_eq — Mathlib

English

Equality of ιOrZero with the canonical π-index map holds by construction.

Русский

Равенство ιOrZero и канонического π-индекса сохраняется по конструктору.

LaTeX

$$$ι^{OrZero} = ι$ by construction.$$

Lean4

theorem d₁_eq {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
      (ComplexShape.ε₁ c₁₂ c₃ c₄ (ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩, i₃) * ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂)) •
        (G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃) ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j :=
  by
  obtain rfl := c₁.next_eq' h₁
  rfl

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