extendCyclesIso_hom_naturality — Mathlib

English

Relates the naturality of extendCyclesIso with respect to extendMap and cyclesMap.

Русский

Связано естественное свойство extendCyclesIso относительно extendMap и cyclesMap.

LaTeX

$$cyclesMap (extendMap φ e) j' ≫ (L.extendCyclesIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ cyclesMap φ j$$

Lean4

@[reassoc (attr := simp)]
theorem extendCyclesIso_hom_naturality :
    cyclesMap (extendMap φ e) j' ≫ (L.extendCyclesIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ cyclesMap φ j := by
  simp [← cancel_mono (L.iCycles j), extendMap_f φ e hj']

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