fromOpcycles_op_cyclesOpIso_inv — Mathlib

English

The homomorphisms along the canonical isomorphisms between opcycles and cycles satisfy a natural compatibility: (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i.

Русский

Гомоморфизмы, связанные с каноническими изоморфизмами между opcycles и cycles, удовлетворяют естественной совместимости: (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i.

LaTeX

$$(K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i$$

Lean4

@[reassoc (attr := simp)]
theorem fromOpcycles_op_cyclesOpIso_inv : (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i :=
  by
  by_cases hij : c.Rel i j
  · obtain rfl := c.next_eq' hij
    exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv
  · rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]

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