liftCycles_comp_cyclesMap — Mathlib

English

For φ: S ⟶ S1, S.liftCycles k hk ≫ cyclesMap φ = S1.liftCycles (k ≫ φ.τ₂) with boundary adjustment.

Русский

Для φ: S ⟶ S1, подъем циклов совместим с cyclesMap φ по правилу: liftCycles k hk ≫ cyclesMap φ = S1.liftCycles (k ≫ φ.τ₂) с поправкой на границу.

LaTeX

$$$S.liftCycles\,k\,hk \;\circ\; cyclesMap(\varphi) = S_{1}.liftCycles( k \circ φ.τ_2)$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCycles_comp_cyclesMap (φ : S ⟶ S₁) [S₁.HasLeftHomology] :
    S.liftCycles k hk ≫ cyclesMap φ = S₁.liftCycles (k ≫ φ.τ₂) (by rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]) :=
  by cat_disch

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