π_comp_H0IsoOfIsTrivial_hom — Mathlib

English

For trivial A, the composite π A 0 ≫ (H0IsoOfIsTrivial A).hom equals (cyclesIso₀ A).hom.

Русский

Для тривиального A композиция π_A0 затем gомоморфизм H0IsoOfIsTrivial(A) равна гомоморфизму cycles₀(A).hom.

LaTeX

$$$\\pi A 0 \\;\\circ\\; (H_0\\mathrm{IsoOfIsTrivial}\\ A).hom = (\\mathrm{cyclesIso}_0\\ A).hom$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem π_comp_H0IsoOfIsTrivial_hom : π A 0 ≫ (H0IsoOfIsTrivial A).hom = (cyclesIso₀ A).hom := by
  simp [H0IsoOfIsTrivial]

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