comm — Mathlib

English

RestrictionToTruncGE' commutes with truncGE'Map via restrictionMap.

Русский

RestrictionToTruncGE' взаимно переставляется с truncGE'Map через restrictionMap.

LaTeX

$$$\text{comm}(K,L,M; e) :\ K.restrictionToTruncGE' e \;\circ\; \mathrm{truncGE'Map}(\phi,e) = \mathrm{restrictionMap}(\phi,e) \;\circ\; L.restrictionToTruncGE' e$$$

Lean4

@[reassoc (attr := simp)]
theorem comm (i j : ι) : f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j :=
  by
  by_cases hij : c.Rel i j
  · by_cases hi : e.BoundaryGE i
    · rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi, f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi]
      simp [restrictionXIso]
    · rw [f_eq_iso_hom_iso_inv K e rfl hi, f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq e hij rfl rfl hi]
      simp [restrictionXIso]
  · simp [HomologicalComplex.shape _ _ _ hij]

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