truncGE'_d_eq_fromOpcycles — Mathlib

English

If i maps to i' and i is a boundary, the truncation differential equals an iso-twist around fromOpcycles.

Русский

Если i связано с i' и i является границей, дифференциал truncGE' равен изотропному повороту вокруг fromOpcycles.

LaTeX

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

Lean4

theorem truncGE'_d_eq_fromOpcycles {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'XIsoOpcycles e hi' hi).hom ≫
        K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' (e.not_boundaryGE_next hij)).inv :=
  by
  dsimp [truncGE', truncGE'.d]
  rw [dif_pos hij, dif_pos hi]
  subst hi' hj'
  simp [truncGE'XIso, truncGE'XIsoOpcycles]

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