Theorems · Definition · ring theory

SkewMonoidAlgebra.mapDomainRingHom

{α : Type u_3} →
  {α₂ : Type u_4} →
    {β : Type u_5} →
      {F : Type u_6} →
        [inst : Semiring β] →
          [inst_1 : Monoid α] →
            [inst_2 : Monoid α₂] →
              [inst_3 : FunLike F α α₂] →
                [inst_4 : MulSemiringAction α β] →
                  [inst_5 : MulSemiringAction α₂ β] →
                    [MonoidHomClass F α α₂] →
                      {f : F} → (∀ (a : α) (x : β), a • x = f a • x) → SkewMonoidAlgebra β α →+* SkewMonoidAlgebra β α₂

If f : G → H is a multiplicative homomorphism between two monoids and ∀ (a : G) (x : k), a • x = (f a) • x, then mapDomain f is a ring homomorphism between their skew monoid algebras.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringMonoidMonoidFunLikeMulSemiringActionMulSemiringActionMonoidHomClass