f_eq_iso_hom_pOpcycles_iso_inv — Mathlib

English

If i' is the image of i and i is a boundary, then f K e i equals a composite of restrictionXIso, pOpcycles, and truncGE'XIsoOpcycles inv.

Русский

Если i' — образ i и i является границей, то f K e i равен композиции restrictionXIso, pOpcycles и обратного изоморфизма truncGE'XIsoOpcycles.

LaTeX

$$$f K e i = (K.restrictionXIso e hi').hom \circ K.pOpcycles i' \circ (K.truncGE'XIsoOpcycles e hi' hi).inv$$$

Lean4

theorem f_eq_iso_hom_pOpcycles_iso_inv {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) :
    f K e i = (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv :=
  by
  dsimp [f]
  rw [dif_pos hi]
  subst hi'
  simp [restrictionXIso]

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