From 3e6a860d03dd4c3848f2ceb3693c30e4f6384895 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 22 Apr 2021 12:50:49 +0200 Subject: [PATCH 1/4] feat(algebra/monoid_algebra): add mem.span_support --- src/algebra/monoid_algebra.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 1e27f851e5815..1d2c561d218c9 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -601,6 +601,17 @@ calc (f * g) x = sum g (λ a b, (f * single a b) x) : end +section span + +variables [semiring k] [monoid G] + +lemma mem.span_support (f : (monoid_algebra k G)) : + f ∈ submodule.span k ((monoid_algebra.of k G)'' (f.support : set G)) := +by rw [monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, + finsupp.mem_supported] + +end span + end monoid_algebra /-! ### Additive monoids -/ @@ -890,6 +901,17 @@ lemma lift_nc_smul {R : Type*} [add_zero_class G] [semiring R] (f : k →+* R) end misc_theorems +section span + +variables [semiring k] [add_monoid G] + +lemma mem.span_support (f : (add_monoid_algebra k G)) : + f ∈ submodule.span k ((add_monoid_algebra.of k G)'' (f.support : set G)) := +by rw [add_monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, + finsupp.mem_supported] + +end span + end add_monoid_algebra /-! From 8585a82a957fc47b9b9cd9b1b40e980fd9f364d0 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 22 Apr 2021 15:15:57 +0200 Subject: [PATCH 2/4] Update src/algebra/monoid_algebra.lean Co-authored-by: Eric Wieser --- src/algebra/monoid_algebra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 1d2c561d218c9..0ae36be99b67d 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -603,7 +603,7 @@ end section span -variables [semiring k] [monoid G] +variables [semiring k] [mul_one_class G] lemma mem.span_support (f : (monoid_algebra k G)) : f ∈ submodule.span k ((monoid_algebra.of k G)'' (f.support : set G)) := From 80c94aa882271a7cea857950507ce279bc3261e2 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 22 Apr 2021 15:16:17 +0200 Subject: [PATCH 3/4] Update src/algebra/monoid_algebra.lean Co-authored-by: Eric Wieser --- src/algebra/monoid_algebra.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 0ae36be99b67d..32be587072823 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -605,8 +605,8 @@ section span variables [semiring k] [mul_one_class G] -lemma mem.span_support (f : (monoid_algebra k G)) : - f ∈ submodule.span k ((monoid_algebra.of k G)'' (f.support : set G)) := +lemma mem_span_support (f : monoid_algebra k G) : + f ∈ submodule.span k (monoid_algebra.of k G '' (f.support : set G)) := by rw [monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported] From d2cd5654676b66a34576d217cfd9b3558361480c Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 22 Apr 2021 15:16:53 +0200 Subject: [PATCH 4/4] golf the additive version --- src/algebra/monoid_algebra.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 32be587072823..6ab5066b56a31 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -903,10 +903,10 @@ end misc_theorems section span -variables [semiring k] [add_monoid G] +variables [semiring k] [add_zero_class G] -lemma mem.span_support (f : (add_monoid_algebra k G)) : - f ∈ submodule.span k ((add_monoid_algebra.of k G)'' (f.support : set G)) := +lemma mem_span_support (f : add_monoid_algebra k G) : + f ∈ submodule.span k (add_monoid_algebra.of k G '' (f.support : set G)) := by rw [add_monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]