comp_hom — Mathlib

English

The composition of two Action.Hom morphisms matches the composition on the underlying maps, associativity up to coherence.

Русский

Сведение композиции двух морфизмов действия к композиции их отображений сохраняет категориальную структуру.

LaTeX

$$$\\text{comp\_hom} : (f: M\\to N) \\to (g: N\\to K) \\Rightarrow (f\\circ g).hom = f.hom \\circ g.hom$$$

Lean4

@[simp, reassoc]
theorem comp_hom {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) : (f ≫ g : Hom M K).hom = f.hom ≫ g.hom :=
  rfl

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