cyclesMap_comp — Mathlib

English

The cycles map is compatible with composition: cyclesMap(φ ∘ ψ) i equals cyclesMap φ i composed with cyclesMap ψ i.

Русский

Отображение циклов совместимо с композициией: cyclesMap(φ ∘ ψ) i = cyclesMap φ i ∘ cyclesMap ψ i.

LaTeX

$$$\operatorname{cyclesMap}(\varphi \circ \psi) i = \operatorname{cyclesMap}(\varphi) i \circ \operatorname{cyclesMap}(\psi) i$$$

Lean4

@[reassoc]
theorem cyclesMap_comp : cyclesMap (φ ≫ ψ) i = cyclesMap φ i ≫ cyclesMap ψ i :=
  by
  dsimp [cyclesMap]
  rw [Functor.map_comp, ShortComplex.cyclesMap_comp]

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