Documentation

Toric.Mathlib.Algebra.MonoidAlgebra.Basic

source
@[simp]
theorem MonoidAlgebra.liftNCAlgHom_single {k : Type u_1} {A : Type u_2} {B : Type u_3} {G : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring B] [Algebra k B] [Monoid G] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), Commute (f x) (g y)) (a : G) (b : A) :
(liftNCAlgHom f g h_comm) (single a b) = f b * g a
source
@[simp]
theorem MonoidAlgebra.mapRangeRingHom_comp_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] [CommSemiring R] [CommSemiring S] (f : R →+* S) :
(mapRangeRingHom f).comp (algebraMap R (MonoidAlgebra R M)) = (algebraMap S (MonoidAlgebra S M)).comp f
source
noncomputable def MonoidAlgebra.mapRangeAlgHom {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] {T : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) :
MonoidAlgebra S M →ₐ[R] MonoidAlgebra T M

The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras.

Equations
Instances For
    source
    @[simp]
    theorem MonoidAlgebra.mapRangeAlgHom_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] {T : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) (x : MonoidAlgebra S M) (m : M) :
    ((mapRangeAlgHom f) x) m = f (x m)
    source
    @[simp]
    theorem MonoidAlgebra.mapRangeAlgHom_single {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] {T : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) (a : M) (b : S) :
    (mapRangeAlgHom f) (single a b) = single a (f b)
    source
    noncomputable def MonoidAlgebra.mapRangeAlgEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] {T : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] (f : S ≃ₐ[R] T) :
    MonoidAlgebra S M ≃ₐ[R] MonoidAlgebra T M

    The algebra isomorphism of monoid algebras induced by an isomorphism of the base algebras.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MonoidAlgebra.mapRangeAlgEquiv_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] {T : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] (f : S ≃ₐ[R] T) (a✝ : MonoidAlgebra S M) :
      (mapRangeAlgEquiv f) a✝ = (↑↑(mapRangeAlgHom ↑f).toRingHom).toFun a✝
      source
      @[reducible, inline]
      noncomputable abbrev MonoidAlgebra.algebraMonoidAlgebra {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] :
      Algebra (MonoidAlgebra R M) (MonoidAlgebra S M)

      If S is an R-algebra, then MonoidAlgebra S σ is a MonoidAlgebra R σ algebra.

      Warning: This produces a diamond for Algebra (MonoidAlgebra R σ) (MonoidAlgebra (MonoidAlgebra S σ) σ). That's why it is not a global instance.

      Equations
      Instances For
        source
        @[simp]
        theorem MonoidAlgebra.algebraMap_def {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] :
        algebraMap (MonoidAlgebra R M) (MonoidAlgebra S M) = mapRangeRingHom (algebraMap R S)
        source
        instance MonoidAlgebra.instIsScalarTower_toric {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] :
        IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra T M)