Lemmas for algebra/monoid_algebra.lean #
These are part of upstream PR https://github.com/leanprover-community/mathlib/pull/4321
noncomputable
def
add_monoid_algebra.sum_id
(k : Type u_1)
{G : Type u_2}
{A : Type u_3}
[comm_semiring k]
[semiring A]
[algebra k A]
[add_monoid G] :
add_monoid_algebra A G →ₐ[k] A
The alg_hom which maps from a grading of an algebra A back to that algebra.
Equations
- add_monoid_algebra.sum_id k = add_monoid_algebra.lift_nc_alg_hom (alg_hom.id k A) {to_fun := λ (g : multiplicative G), 1, map_one' := _, map_mul' := _} _
theorem
add_monoid_algebra.sum_id_apply
(k : Type u_1)
{G : Type u_2}
{A : Type u_3}
[comm_semiring k]
[semiring A]
[algebra k A]
[add_monoid G]
(g : add_monoid_algebra A G) :
⇑(add_monoid_algebra.sum_id k) g = finsupp.sum g (λ (_x : G) (gi : A), gi)
noncomputable
def
add_monoid_algebra.lsingle
{G : Type u_2}
{k : Type u_1}
{A : Type u_3}
[semiring k]
[semiring A]
[module k A]
(i : G) :
A →ₗ[k] add_monoid_algebra A G
Equations
@[simp]
theorem
add_monoid_algebra.lsingle_apply
{G : Type u_2}
{k : Type u_1}
{A : Type u_3}
[semiring k]
[semiring A]
[module k A]
(i : G)
(a : A) :
⇑(add_monoid_algebra.lsingle i) a = finsupp.single i a