mapDomainBialgHom_comp — Mathlib

English

The construction of a bialgebra hom from an algebra hom preserves scalar action and comultiplication compatibility; the internal equalities ensure the resulting map is indeed a bialgebra hom.

Русский

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

LaTeX

$$⊢ φ : A →ₐc[R] B with counit_comp and map_comp_comul$$

Lean4

@[simp]
theorem mapDomainBialgHom_comp (f : N →* O) (g : M →* N) :
    mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g) := by ext;
  simp [Finsupp.mapDomain_comp]

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