English
Given short complexes S1,S2 with homology, the opposite of the homology map is equal to the composition of the inverses of the opposite isomorphisms with the opposite of the homology map, concluding with the opposite of the other isomorphism. This is the functoriality in the opposite direction.
Русский
При наличии коротких комплексов S1,S2 с гомологией противоположная карта гомологии равна композиции с инверсией противоположности изоморфизмов, с противоположной маппой и далее противоположной другой изоморфизмом. Это проявление функториальности в противоположном направлении.
LaTeX
$$homologyMap'(φ,h₁,h₂).op = h₂.iso.inv.op ≫ homologyMap'(opMap φ,h₂.op,h₁.op) ≫ h₁.iso.hom.op$$
Lean4
theorem homologyMap'_op :
(homologyMap' φ h₁ h₂).op = h₂.iso.inv.op ≫ homologyMap' (opMap φ) h₂.op h₁.op ≫ h₁.iso.hom.op :=
Quiver.Hom.unop_inj
(by
dsimp
have γ : HomologyMapData φ h₁ h₂ := default
simp only [γ.homologyMap'_eq, γ.op.homologyMap'_eq, HomologyData.op_left, HomologyMapData.op_left,
RightHomologyMapData.op_φH, Quiver.Hom.unop_op, assoc, ← γ.comm_assoc, Iso.hom_inv_id, comp_id])
