opcyclesMap_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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