inrX_d — Mathlib

English

For all i, j, the composition inrX φ i ≫ d φ i j equals G.d i_j ≫ inrX φ j, with case analysis: if hij then equalities hold by ext_to_X or ext_to_X'; otherwise zero.

Русский

Для всех i, j: inrX φ i ∘ d φ i j = G.d i j ∘ inrX φ j; в зависимости от отношения c.Rel выполняются соответствующие равенства или нули.

LaTeX

$$$ inrX\\,\\phi\\,i \\circ d\\,φ\\,i\\,j = G.d\\,i\\,j \\circ inrX\\,φ\\,j. $$$

Lean4

@[reassoc (attr := simp)]
theorem inrX_d (i j : ι) : inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j :=
  by
  by_cases hij : c.Rel i j
  · by_cases hj : c.Rel j (c.next j)
    · apply ext_to_X _ _ _ hj
      · simp [d_fstX φ _ _ _ hij]
      · simp [d_sndX φ _ _ hij]
    · apply ext_to_X' _ _ hj
      simp [d_sndX φ _ _ hij]
  · rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]

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