comp — Mathlib

English

The composition of two Action.Hom morphisms is given by the composition of their underlying maps.

Русский

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

LaTeX

$$$\text{comp} : \mathrm{Action}.Hom M N \to \mathrm{Action}.Hom N K \to \mathrm{Action}.Hom M K$, and $(f \circ h).hom = f.hom \circ g.hom$$$

Lean4

/-- The composition of two `Action V G` homomorphisms is the composition of the underlying maps.
-/
@[simps]
def comp {M N K : Action V G} (p : Action.Hom M N) (q : Action.Hom N K) : Action.Hom M K where hom := p.hom ≫ q.hom

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