Documentation

Mathlib.Algebra.MonoidAlgebra.MapDomain

MonoidAlgebra.mapDomain #

Multiplicative monoids #

@[reducible, inline]
abbrev MonoidAlgebra.mapDomain {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] (f : MN) (v : MonoidAlgebra R M) :
Equations
Instances For
    theorem MonoidAlgebra.mapDomain_sum {R : Type u_2} {S : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] (f : MN) (s : MonoidAlgebra S M) (v : MSMonoidAlgebra R M) :
    mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)
    theorem MonoidAlgebra.mapDomain_single {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : MN} {a : M} {r : R} :
    mapDomain f (single a r) = single (f a) r
    theorem MonoidAlgebra.mapDomain_injective {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : MN} (hf : Function.Injective f) :
    @[simp]
    theorem MonoidAlgebra.mapDomain_one {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [One α] [One α₂] {F : Type u_11} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :
    mapDomain (⇑f) 1 = 1

    Like Finsupp.mapDomain_zero, but for the 1 we define in this file

    theorem MonoidAlgebra.mapDomain_mul {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Mul α] [Mul α₂] {F : Type u_11} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α) :
    mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

    Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

    def MonoidAlgebra.mapDomainRingHom {G : Type u_4} (k : Type u_8) {H : Type u_9} {F : Type u_10} [Semiring k] [Monoid G] [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :

    If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is a ring homomorphism between their monoid algebras.

    Equations
    Instances For
      @[simp]
      theorem MonoidAlgebra.mapDomainRingHom_apply {G : Type u_4} (k : Type u_8) {H : Type u_9} {F : Type u_10} [Semiring k] [Monoid G] [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (a✝ : G →₀ k) :

      Additive monoids #

      @[reducible, inline]
      abbrev AddMonoidAlgebra.mapDomain {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] (f : MN) (v : AddMonoidAlgebra R M) :
      Equations
      Instances For
        theorem AddMonoidAlgebra.mapDomain_sum {R : Type u_2} {S : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] (f : MN) (s : AddMonoidAlgebra S M) (v : MSAddMonoidAlgebra R M) :
        mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)
        theorem AddMonoidAlgebra.mapDomain_single {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : MN} {a : M} {r : R} :
        mapDomain f (single a r) = single (f a) r
        theorem AddMonoidAlgebra.mapDomain_injective {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : MN} (hf : Function.Injective f) :
        @[simp]
        theorem AddMonoidAlgebra.mapDomain_one {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Zero α] [Zero α₂] {F : Type u_11} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :
        mapDomain (⇑f) 1 = 1

        Like Finsupp.mapDomain_zero, but for the 1 we define in this file

        theorem AddMonoidAlgebra.mapDomain_mul {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Add α] [Add α₂] {F : Type u_11} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x y : AddMonoidAlgebra β α) :
        mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

        Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

        def AddMonoidAlgebra.mapDomainRingHom {G : Type u_4} (k : Type u_8) [Semiring k] {H : Type u_9} {F : Type u_10} [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :

        If f : G → H is an additive homomorphism between two additive monoids, then Finsupp.mapDomain f is a ring homomorphism between their add monoid algebras.

        Equations
        Instances For
          @[simp]
          theorem AddMonoidAlgebra.mapDomainRingHom_apply {G : Type u_4} (k : Type u_8) [Semiring k] {H : Type u_9} {F : Type u_10} [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (a✝ : G →₀ k) :

          Conversions between AddMonoidAlgebra and MonoidAlgebra #

          We have not defined k[G] = MonoidAlgebra k (Multiplicative G) because historically this caused problems; since the changes that have made nsmul definitional, this would be possible, but for now we just construct the ring isomorphisms using RingEquiv.refl _.

          The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For