cyclesOpIso_inv_naturality — Mathlib

English

For φ: S1 ⟶ S2 with right homology, the equation (opcyclesMap φ).op ≫ (S1.cyclesOpIso).inv = S2.cyclesOpIso.inv ≫ cyclesMap (opMap φ).op holds.

Русский

Для φ: S1 ⟶ S2 с правой гомологией выполняется (opcyclesMap φ).op ∘ (S1.cyclesOpIso).inv = (S2.cyclesOpIso.inv) ∘ cyclesMap (opMap φ).op.

LaTeX

$$(opcyclesMap(φ)).op ≫ (S1.cyclesOpIso).inv = S2.cyclesOpIso.inv ≫ cyclesMap (opMap φ).op$$

Lean4

@[reassoc]
theorem cyclesOpIso_inv_naturality (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
    (opcyclesMap φ).op ≫ (S₁.cyclesOpIso).inv = S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ) := by
  rw [← cancel_mono S₁.op.iCycles, assoc, assoc, cyclesOpIso_inv_op_iCycles, cyclesMap_i,
    cyclesOpIso_inv_op_iCycles_assoc, ← op_comp, p_opcyclesMap, op_comp, opMap_τ₂]

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