opcyclesOpIso_inv_naturality — Mathlib

English

For φ: S1 ⟶ S2 with left homology, the naturality equation (opcyclesMap φ).op ≫ (S1.opcyclesOpIso).inv = S2.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ) holds.

Русский

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

LaTeX

$$(opcyclesMap(φ)).op ∘ (S1.opcyclesOpIso).inv = S2.opcyclesOpIso.inv ∘ opcyclesMap (opMap φ)$$

Lean4

@[reassoc]
theorem opcyclesOpIso_inv_naturality (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    (cyclesMap φ).op ≫ (S₁.opcyclesOpIso).inv = S₂.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ) := by
  rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc, ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_id,
    comp_id]

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