opcyclesIso_hom_comp_descQ — Mathlib

English

Let h be the right homology data for a ShortComplex S, and let k : S.X₂ ⟶ A with hk : S.f ∘ k = 0. Then the composition h.opcyclesIso.hom ∘ h.descQ(k, hk) equals S.descOpcycles(k, hk).

Русский

Пусть h — правая данные однородности для ShortComplex S, и пусть k : S.X₂ ⟶ A удовлетворяет hk: S.f ∘ k = 0. Тогда композиция h.opcyclesIso.hom ∘ h.descQ(k, hk) равна S.descOpcycles(k, hk).

LaTeX

$$$$ h.opcyclesIso.hom \circ h.descQ\,k\,hk = S.descOpcycles\,k\,hk $$$$

Lean4

@[simp]
theorem opcyclesIso_hom_comp_descQ : h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk := by
  rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]

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