Monoid algebras #
Multiplicative monoids #
Non-unital, non-associative algebra structure #
theorem
MonoidAlgebra.nonUnitalAlgHom_ext
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Mul G]
[NonUnitalNonAssocSemiring A]
[DistribMulAction k A]
{φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A}
(h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1))
:
A non_unital k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its
values on the functions single a 1.
theorem
AddMonoidAlgebra.nonUnitalAlgHom_ext
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Add G]
[NonUnitalNonAssocSemiring A]
[DistribMulAction k A]
{φ₁ φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A}
(h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1))
:
A non_unital k-algebra homomorphism from k[G] is uniquely defined by its
values on the functions single a 1.
theorem
MonoidAlgebra.nonUnitalAlgHom_ext'
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Mul G]
[NonUnitalNonAssocSemiring A]
[DistribMulAction k A]
{φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A}
(h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G))
:
See note [partially-applied ext lemmas].
def
MonoidAlgebra.liftMagma
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Mul G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
:
The functor G ↦ MonoidAlgebra k G, from the category of magmas to the category of non-unital,
non-associative algebras over k is adjoint to the forgetful functor in the other direction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MonoidAlgebra.liftMagma_apply_apply
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Mul G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
(f : G →ₙ* A)
(a : MonoidAlgebra k G)
:
@[simp]
theorem
MonoidAlgebra.liftMagma_symm_apply
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Mul G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
(F : MonoidAlgebra k G →ₙₐ[k] A)
:
Algebra structure #
instance
MonoidAlgebra.algebra
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
:
Algebra k (MonoidAlgebra A G)
The instance Algebra k (MonoidAlgebra A G) whenever we have Algebra k A.
In particular this provides the instance Algebra k (MonoidAlgebra k G).
Equations
- MonoidAlgebra.algebra = { toSMul := MonoidAlgebra.smulZeroClass.toSMul, algebraMap := MonoidAlgebra.singleOneRingHom.comp (algebraMap k A), commutes' := ⋯, smul_def' := ⋯ }
instance
AddMonoidAlgebra.algebra
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
:
Algebra k (AddMonoidAlgebra A G)
The instance Algebra R k[G] whenever we have Algebra R k.
In particular this provides the instance Algebra k k[G].
Equations
- AddMonoidAlgebra.algebra = { toSMul := MonoidAlgebra.smulZeroClass.toSMul, algebraMap := AddMonoidAlgebra.singleZeroRingHom.comp (algebraMap k A), commutes' := ⋯, smul_def' := ⋯ }
def
MonoidAlgebra.singleOneAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
:
Finsupp.single 1 as an AlgHom
Equations
- MonoidAlgebra.singleOneAlgHom = { toRingHom := MonoidAlgebra.singleOneRingHom, commutes' := ⋯ }
Instances For
def
AddMonoidAlgebra.singleZeroAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
:
Finsupp.single 0 as an AlgHom
Equations
- AddMonoidAlgebra.singleZeroAlgHom = { toRingHom := AddMonoidAlgebra.singleZeroRingHom, commutes' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.singleOneAlgHom_apply
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
(b : A)
:
@[simp]
theorem
AddMonoidAlgebra.singleZeroAlgHom_apply
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
(b : A)
:
@[simp]
theorem
MonoidAlgebra.coe_algebraMap
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
:
@[simp]
theorem
AddMonoidAlgebra.coe_algebraMap
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
:
theorem
MonoidAlgebra.single_eq_algebraMap_mul_of
{k : Type u_1}
{G : Type u_2}
[CommSemiring k]
[Monoid G]
(a : G)
(b : k)
:
theorem
MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
(a : G)
(b : k)
:
instance
MonoidAlgebra.isLocalHom_singleOneAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
:
instance
AddMonoidAlgebra.isLocalHom_singleZeroAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
:
instance
MonoidAlgebra.isLocalHom_algebraMap
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[Monoid G]
[IsLocalHom (algebraMap k A)]
:
IsLocalHom (algebraMap k (MonoidAlgebra A G))
instance
AddMonoidAlgebra.isLocalHom_algebraMap
{k : Type u_1}
{G : Type u_2}
{A : Type u_11}
[CommSemiring k]
[Semiring A]
[Algebra k A]
[AddMonoid G]
[IsLocalHom (algebraMap k A)]
:
IsLocalHom (algebraMap k (AddMonoidAlgebra A G))
def
MonoidAlgebra.liftNCAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
{B : Type u_8}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
[Semiring B]
[Algebra k B]
(f : A →ₐ[k] B)
(g : G →* B)
(h_comm : ∀ (x : A) (y : G), Commute (f x) (g y))
:
liftNCRingHom as an AlgHom, for when f is an AlgHom
Equations
- MonoidAlgebra.liftNCAlgHom f g h_comm = { toRingHom := MonoidAlgebra.liftNCRingHom (↑f) g h_comm, commutes' := ⋯ }
Instances For
theorem
MonoidAlgebra.algHom_ext
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄
(h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1))
:
A k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its
values on the functions single a 1.
theorem
AddMonoidAlgebra.algHom_ext
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
⦃φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A⦄
(h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1))
:
A k-algebra homomorphism from k[G] is uniquely defined by its
values on the functions single a 1.
def
MonoidAlgebra.lift
(k : Type u_1)
(G : Type u_2)
(A : Type u_7)
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
:
Any monoid homomorphism G →* A can be lifted to an algebra homomorphism
MonoidAlgebra k G →ₐ[k] A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MonoidAlgebra.lift_apply'
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
(F : G →* A)
(f : MonoidAlgebra k G)
:
theorem
MonoidAlgebra.lift_apply
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
(F : G →* A)
(f : MonoidAlgebra k G)
:
theorem
MonoidAlgebra.lift_def
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
(F : G →* A)
:
theorem
MonoidAlgebra.lift_unique
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
(F : MonoidAlgebra k G →ₐ[k] A)
(f : MonoidAlgebra k G)
:
Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by
its values on F (single a 1).
def
MonoidAlgebra.mapDomainNonUnitalAlgHom
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{G : Type u_13}
{H : Type u_14}
{F : Type u_15}
[Mul G]
[Mul H]
[FunLike F G H]
[MulHomClass F G H]
(f : F)
:
If f : G → H is a homomorphism between two magmas, then
Finsupp.mapDomain f is a non-unital algebra homomorphism between their magma algebras.
Equations
- MonoidAlgebra.mapDomainNonUnitalAlgHom k A f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }
Instances For
def
AddMonoidAlgebra.mapDomainNonUnitalAlgHom
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{G : Type u_13}
{H : Type u_14}
{F : Type u_15}
[Add G]
[Add H]
[FunLike F G H]
[AddHomClass F G H]
(f : F)
:
If f : G → H is a homomorphism between two additive magmas, then Finsupp.mapDomain f is a
non-unital algebra homomorphism between their additive magma algebras.
Equations
- AddMonoidAlgebra.mapDomainNonUnitalAlgHom k A f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }
Instances For
@[simp]
theorem
AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{G : Type u_13}
{H : Type u_14}
{F : Type u_15}
[Add G]
[Add H]
[FunLike F G H]
[AddHomClass F G H]
(f : F)
(a✝ : G →₀ A)
:
@[simp]
theorem
MonoidAlgebra.mapDomainNonUnitalAlgHom_apply
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{G : Type u_13}
{H : Type u_14}
{F : Type u_15}
[Mul G]
[Mul H]
[FunLike F G H]
[MulHomClass F G H]
(f : F)
(a✝ : G →₀ A)
:
theorem
MonoidAlgebra.mapDomain_algebraMap
{k : Type u_1}
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[Monoid G]
[Monoid H]
[Semiring A]
[Algebra k A]
{F : Type u_11}
[FunLike F G H]
[MonoidHomClass F G H]
(f : F)
(r : k)
:
theorem
AddMonoidAlgebra.mapDomain_algebraMap
{k : Type u_1}
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[AddMonoid G]
[AddMonoid H]
[Semiring A]
[Algebra k A]
{F : Type u_11}
[FunLike F G H]
[AddMonoidHomClass F G H]
(f : F)
(r : k)
:
def
MonoidAlgebra.mapDomainAlgHom
{G : Type u_2}
[Monoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{H : Type u_13}
{F : Type u_14}
[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 an algebra homomorphism between their monoid algebras.
Equations
- MonoidAlgebra.mapDomainAlgHom k A f = { toRingHom := MonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }
Instances For
def
AddMonoidAlgebra.mapDomainAlgHom
{G : Type u_2}
[AddMonoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{H : Type u_13}
{F : Type u_14}
[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 an algebra homomorphism between their additive monoid algebras.
Equations
- AddMonoidAlgebra.mapDomainAlgHom k A f = { toRingHom := AddMonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.mapDomainAlgHom_apply
{G : Type u_2}
[Monoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{H : Type u_13}
{F : Type u_14}
[Monoid H]
[FunLike F G H]
[MonoidHomClass F G H]
(f : F)
(a✝ : G →₀ A)
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainAlgHom_apply
{G : Type u_2}
[AddMonoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
{H : Type u_13}
{F : Type u_14}
[AddMonoid H]
[FunLike F G H]
[AddMonoidHomClass F G H]
(f : F)
(a✝ : G →₀ A)
:
@[simp]
theorem
MonoidAlgebra.mapDomainAlgHom_id
{G : Type u_2}
[Monoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainAlgHom_id
{G : Type u_2}
[AddMonoid G]
(k : Type u_11)
(A : Type u_12)
[CommSemiring k]
[Semiring A]
[Algebra k A]
:
def
MonoidAlgebra.domCongr
(k : Type u_1)
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[Monoid G]
[Monoid H]
[Semiring A]
[Algebra k A]
(e : G ≃* H)
:
If e : G ≃* H is a multiplicative equivalence between two monoids, then
MonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.
Equations
- MonoidAlgebra.domCongr k A e = AlgEquiv.ofLinearEquiv (Finsupp.domLCongr ↑e) ⋯ ⋯
Instances For
def
AddMonoidAlgebra.domCongr
(k : Type u_1)
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[AddMonoid G]
[AddMonoid H]
[Semiring A]
[Algebra k A]
(e : G ≃+ H)
:
If e : G ≃+ H is an additive equivalence between two additive monoids, then
AddMonoidAlgebra.domCongr e is an algebra equivalence between their additive monoid algebras.
Equations
- AddMonoidAlgebra.domCongr k A e = AlgEquiv.ofLinearEquiv (Finsupp.domLCongr ↑e) ⋯ ⋯
Instances For
@[simp]
theorem
MonoidAlgebra.domCongr_support
(k : Type u_1)
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[Monoid G]
[Monoid H]
[Semiring A]
[Algebra k A]
(e : G ≃* H)
(f : MonoidAlgebra A G)
:
@[simp]
theorem
AddMonoidAlgebra.domCongr_support
(k : Type u_1)
{G : Type u_2}
{H : Type u_3}
(A : Type u_7)
[CommSemiring k]
[AddMonoid G]
[AddMonoid H]
[Semiring A]
[Algebra k A]
(e : G ≃+ H)
(f : AddMonoidAlgebra A G)
:
@[simp]
theorem
MonoidAlgebra.domCongr_refl
(k : Type u_1)
{G : Type u_2}
(A : Type u_7)
[CommSemiring k]
[Monoid G]
[Semiring A]
[Algebra k A]
:
@[simp]
theorem
AddMonoidAlgebra.domCongr_refl
(k : Type u_1)
{G : Type u_2}
(A : Type u_7)
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainRingHom_comp_algebraMap
{R : Type u_4}
{A : Type u_7}
{M : Type u_9}
{N : Type u_10}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
:
(mapDomainRingHom A f).comp (algebraMap R (AddMonoidAlgebra A M)) = algebraMap R (AddMonoidAlgebra A N)
@[simp]
theorem
MonoidAlgebra.mapRangeRingHom_comp_algebraMap
{R : Type u_4}
{S : Type u_5}
{M : Type u_9}
[CommSemiring R]
[CommSemiring S]
[Monoid M]
(f : R →+* S)
:
(mapRangeRingHom M f).comp (algebraMap R (MonoidAlgebra R M)) = (algebraMap S (MonoidAlgebra S M)).comp f
@[simp]
theorem
AddMonoidAlgebra.mapRangeRingHom_comp_algebraMap
{R : Type u_4}
{S : Type u_5}
{M : Type u_9}
[CommSemiring R]
[CommSemiring S]
[AddMonoid M]
(f : R →+* S)
:
(mapRangeRingHom M f).comp (algebraMap R (AddMonoidAlgebra R M)) = (algebraMap S (AddMonoidAlgebra S M)).comp f
noncomputable def
MonoidAlgebra.mapRangeAlgHom
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Monoid M]
(f : A →ₐ[R] B)
:
The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras.
Equations
- MonoidAlgebra.mapRangeAlgHom M f = { toRingHom := MonoidAlgebra.mapRangeRingHom M ↑f, commutes' := ⋯ }
Instances For
noncomputable def
AddMonoidAlgebra.mapRangeAlgHom
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[AddMonoid M]
(f : A →ₐ[R] B)
:
The algebra homomorphism of additive monoid algebras induced by a homomorphism of the base algebras.
Equations
- AddMonoidAlgebra.mapRangeAlgHom M f = { toRingHom := AddMonoidAlgebra.mapRangeRingHom M ↑f, commutes' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.mapRangeAlgHom_apply
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
{M : Type u_9}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Monoid M]
(f : A →ₐ[R] B)
(x : MonoidAlgebra A M)
(m : M)
:
@[simp]
theorem
AddMonoidAlgebra.mapRangeAlgHom_apply
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
{M : Type u_9}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[AddMonoid M]
(f : A →ₐ[R] B)
(x : AddMonoidAlgebra A M)
(m : M)
:
noncomputable def
MonoidAlgebra.mapRangeAlgEquiv
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Monoid M]
(f : A ≃ₐ[R] B)
:
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
noncomputable def
AddMonoidAlgebra.mapRangeAlgEquiv
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[AddMonoid M]
(f : A ≃ₐ[R] B)
:
The algebra isomorphism of additive 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
@[simp]
theorem
AddMonoidAlgebra.mapRangeAlgEquiv_apply
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[AddMonoid M]
(f : A ≃ₐ[R] B)
(a✝ : AddMonoidAlgebra A M)
:
@[simp]
theorem
MonoidAlgebra.mapRangeAlgEquiv_apply
{R : Type u_4}
{A : Type u_7}
{B : Type u_8}
(M : Type u_9)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Monoid M]
(f : A ≃ₐ[R] B)
(a✝ : MonoidAlgebra A M)
:
def
MonoidAlgebra.GroupSMul.linearMap
(k : Type u_1)
{G : Type u_2}
[Monoid G]
[CommSemiring k]
(V : Type u_11)
[AddCommMonoid V]
[Module k V]
[Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V]
(g : G)
:
When V is a k[G]-module, multiplication by a group element g is a k-linear map.
Equations
- MonoidAlgebra.GroupSMul.linearMap k V g = { toFun := fun (v : V) => MonoidAlgebra.single g 1 • v, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.GroupSMul.linearMap_apply
(k : Type u_1)
{G : Type u_2}
[Monoid G]
[CommSemiring k]
(V : Type u_11)
[AddCommMonoid V]
[Module k V]
[Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V]
(g : G)
(v : V)
:
def
MonoidAlgebra.equivariantOfLinearOfComm
{k : Type u_1}
{G : Type u_2}
[Monoid G]
[CommSemiring k]
{V : Type u_11}
{W : Type u_12}
[AddCommMonoid V]
[Module k V]
[Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V]
[AddCommMonoid W]
[Module k W]
[Module (MonoidAlgebra k G) W]
[IsScalarTower k (MonoidAlgebra k G) W]
(f : V →ₗ[k] W)
(h : ∀ (g : G) (v : V), f (single g 1 • v) = single g 1 • f v)
:
Build a k[G]-linear map from a k-linear map and evidence that it is G-equivariant.
Equations
- MonoidAlgebra.equivariantOfLinearOfComm f h = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.equivariantOfLinearOfComm_apply
{k : Type u_1}
{G : Type u_2}
[Monoid G]
[CommSemiring k]
{V : Type u_11}
{W : Type u_12}
[AddCommMonoid V]
[Module k V]
[Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V]
[AddCommMonoid W]
[Module k W]
[Module (MonoidAlgebra k G) W]
[IsScalarTower k (MonoidAlgebra k G) W]
(f : V →ₗ[k] W)
(h : ∀ (g : G) (v : V), f (single g 1 • v) = single g 1 • f v)
(v : V)
:
Non-unital, non-associative algebra structure #
theorem
AddMonoidAlgebra.nonUnitalAlgHom_ext'
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Add G]
[NonUnitalNonAssocSemiring A]
[DistribMulAction k A]
{φ₁ φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A}
(h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G))
:
See note [partially-applied ext lemmas].
def
AddMonoidAlgebra.liftMagma
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Add G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
:
The functor G ↦ k[G], from the category of magmas to the category of
non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other
direction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AddMonoidAlgebra.liftMagma_apply_apply
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Add G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
(f : Multiplicative G →ₙ* A)
(a : AddMonoidAlgebra k G)
:
@[simp]
theorem
AddMonoidAlgebra.liftMagma_symm_apply
(k : Type u_1)
{G : Type u_2}
{A : Type u_7}
[Semiring k]
[Add G]
[NonUnitalNonAssocSemiring A]
[Module k A]
[IsScalarTower k A A]
[SMulCommClass k A A]
(F : AddMonoidAlgebra k G →ₙₐ[k] A)
:
Algebra structure #
def
AddMonoidAlgebra.liftNCAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
{B : Type u_8}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
[Semiring B]
[Algebra k B]
(f : A →ₐ[k] B)
(g : Multiplicative G →* B)
(h_comm : ∀ (x : A) (y : Multiplicative G), Commute (f x) (g y))
:
liftNCRingHom as an AlgHom, for when f is an AlgHom
Equations
- AddMonoidAlgebra.liftNCAlgHom f g h_comm = { toRingHom := AddMonoidAlgebra.liftNCRingHom (↑f) g h_comm, commutes' := ⋯ }
Instances For
@[simp]
theorem
AddMonoidAlgebra.coe_liftNCAlgHom
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
{B : Type u_8}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
[Semiring B]
[Algebra k B]
(f : A →ₐ[k] B)
(g : Multiplicative G →* B)
(h_comm : ∀ (x : A) (y : Multiplicative G), Commute (f x) (g y))
:
def
AddMonoidAlgebra.lift
(k : Type u_1)
(G : Type u_2)
(A : Type u_7)
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
:
Any monoid homomorphism G →* A can be lifted to an algebra homomorphism
k[G] →ₐ[k] A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AddMonoidAlgebra.lift_apply'
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
(f : MonoidAlgebra k G)
:
((lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => (algebraMap k A) b * F (Multiplicative.ofAdd a)
theorem
AddMonoidAlgebra.lift_apply
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
(f : MonoidAlgebra k G)
:
theorem
AddMonoidAlgebra.lift_def
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
:
@[simp]
theorem
AddMonoidAlgebra.lift_symm_apply
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : AddMonoidAlgebra k G →ₐ[k] A)
(x : Multiplicative G)
:
theorem
AddMonoidAlgebra.lift_of
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
(x : Multiplicative G)
:
@[simp]
theorem
AddMonoidAlgebra.lift_single
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
(a : G)
(b : k)
:
theorem
AddMonoidAlgebra.lift_of'
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : Multiplicative G →* A)
(x : G)
:
theorem
AddMonoidAlgebra.lift_unique
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
(F : AddMonoidAlgebra k G →ₐ[k] A)
(f : MonoidAlgebra k G)
:
Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by
its values on F (single a 1).
theorem
AddMonoidAlgebra.algHom_ext_iff
{k : Type u_1}
{G : Type u_2}
{A : Type u_7}
[CommSemiring k]
[AddMonoid G]
[Semiring A]
[Algebra k A]
{φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A}
:
def
AddMonoidAlgebra.toMultiplicativeAlgEquiv
(k : Type u_1)
(G : Type u_2)
{R : Type u_4}
[CommSemiring R]
[Semiring k]
[Algebra R k]
[AddMonoid G]
:
The algebra equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of
Multiplicative.
Equations
- AddMonoidAlgebra.toMultiplicativeAlgEquiv k G = { toEquiv := (AddMonoidAlgebra.toMultiplicative k G).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
def
MonoidAlgebra.toAdditiveAlgEquiv
(k : Type u_1)
(G : Type u_2)
{R : Type u_4}
[CommSemiring R]
[Semiring k]
[Algebra R k]
[Monoid G]
:
The algebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of
Additive.
Equations
- MonoidAlgebra.toAdditiveAlgEquiv k G = { toEquiv := (MonoidAlgebra.toAdditive k G).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }