toCycles_naturality — Mathlib

English

The global toCycles map is natural with respect to cycles maps: S1.toCycles followed by cyclesMap φ equals φ.τ1 followed by S2.toCycles.

Русский

Карта toCycles естественна относительно циклических отображений: S1.toCycles затем cyclesMap φ равно φ.τ1 затем S2.toCycles.

LaTeX

$$$S_1.\toCycles \circ \mathrm{cyclesMap}(\phi) = \phi.\tau_1 \circ S_2.\toCycles$$$

Lean4

@[reassoc (attr := simp)]
theorem toCycles_naturality : S₁.toCycles ≫ cyclesMap φ = φ.τ₁ ≫ S₂.toCycles :=
  f'_cyclesMap' _ _ _

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