opcyclesToCycles_naturality — Mathlib

English

Naturality of opcyclesToCycles with respect to a morphism φ: K → L: opcyclesMap φ i ≫ opcyclesToCycles L i j = opcyclesToCycles K i j ≫ cyclesMap φ j.

Русский

Естественность для сопоставления opcycles в отношении отображения φ: K → L: opcyclesMap φ i ≫ opcyclesToCycles L i j = opcyclesToCycles K i j ≫ cyclesMap φ j.

LaTeX

$$$opcyclesMap\,φ\,i ≫ opcyclesToCycles\,L\,i\,j = opcyclesToCycles\,K\,i\,j ≫ cyclesMap\,φ\,j$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesToCycles_naturality :
    opcyclesMap φ i ≫ opcyclesToCycles L i j = opcyclesToCycles K i j ≫ cyclesMap φ j := by
  simp only [← cancel_mono (L.iCycles j), ← cancel_epi (K.pOpcycles i), assoc, p_opcyclesMap_assoc,
    pOpcycles_opcyclesToCycles_iCycles, Hom.comm, cyclesMap_i, pOpcycles_opcyclesToCycles_iCycles_assoc]

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