truncGE'_d_eq — Mathlib

English

The differential in truncGE' has a formula involving iso-terms and the original differential.

Русский

Дифференциал в truncGE' задается через изотропные составляющие и исходный дифференциал.

LaTeX

$$$(K.truncGE' e).d i j = (K.truncGE'XIso e hi' hi).hom \circ K.d i' j' \circ (K.truncGE'XIso e hj' (e.not\_boundaryGE\_next hij)).inv$$$

Lean4

theorem truncGE'_d_eq {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j')
    (hi : ¬e.BoundaryGE i) :
    (K.truncGE' e).d i j =
      (K.truncGE'XIso e hi' hi).hom ≫ K.d i' j' ≫ (K.truncGE'XIso e hj' (e.not_boundaryGE_next hij)).inv :=
  by
  dsimp [truncGE', truncGE'.d]
  rw [dif_pos hij, dif_neg hi]
  subst hi' hj'
  simp [truncGE'XIso]

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