isoCocycles₂_hom_comp_i — Mathlib

English

The homomorphism component of isoCocycles₂ A composed with the i-map in the H2 complex equals iCocycles A 2 composed with cochainsIso₂ A. This expresses a compatiblity of morphisms between the second cocycles and the second cochains isomorphisms.

Русский

Гомоморфизм компоненты из isoCocycles₂ A, композиция с i-маршрутом в H2-цепи равна iCocycles A 2 композиции с cochainsIso₂ A. Отражает совместимость отображений между кокозиалами и коциклами второго уровня.

LaTeX

$$$(isoCocycles_{2}(A))^{\mathrm{hom}} \circ (shortComplexH2(A)).moduleCatLeftHomologyData.i = iCocycles(A,2) \circ (cochainsIso_{2}(A)).hom$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem isoCocycles₂_hom_comp_i :
    (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCocycles A 2 ≫ (cochainsIso₂ A).hom := by
  simp [isoCocycles₂, iCocycles, HomologicalComplex.iCycles, iCycles]

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