Lemmas about the support of a finitely supported function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
monoid_algebra.support_single_mul_subset
{k : Type u₁}
{G : Type u₂}
[semiring k]
[decidable_eq G]
[has_mul G]
(f : monoid_algebra k G)
(r : k)
(a : G) :
(finsupp.single a r * f).support ⊆ finset.image (has_mul.mul a) f.support
theorem
monoid_algebra.support_mul_single_subset
{k : Type u₁}
{G : Type u₂}
[semiring k]
[decidable_eq G]
[has_mul G]
(f : monoid_algebra k G)
(r : k)
(a : G) :
(f * finsupp.single a r).support ⊆ finset.image (λ (_x : G), _x * a) f.support
theorem
monoid_algebra.support_single_mul_eq_image
{k : Type u₁}
{G : Type u₂}
[semiring k]
[decidable_eq G]
[has_mul G]
(f : monoid_algebra k G)
{r : k}
(hr : ∀ (y : k), r * y = 0 ↔ y = 0)
{x : G}
(lx : is_left_regular x) :
(finsupp.single x r * f).support = finset.image (has_mul.mul x) f.support
theorem
monoid_algebra.support_mul_single_eq_image
{k : Type u₁}
{G : Type u₂}
[semiring k]
[decidable_eq G]
[has_mul G]
(f : monoid_algebra k G)
{r : k}
(hr : ∀ (y : k), y * r = 0 ↔ y = 0)
{x : G}
(rx : is_right_regular x) :
(f * finsupp.single x r).support = finset.image (λ (_x : G), _x * x) f.support
theorem
monoid_algebra.support_mul_single
{k : Type u₁}
{G : Type u₂}
[semiring k]
[right_cancel_semigroup G]
(f : monoid_algebra k G)
(r : k)
(hr : ∀ (y : k), y * r = 0 ↔ y = 0)
(x : G) :
(f * finsupp.single x r).support = finset.map (mul_right_embedding x) f.support
theorem
monoid_algebra.support_single_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[left_cancel_semigroup G]
(f : monoid_algebra k G)
(r : k)
(hr : ∀ (y : k), r * y = 0 ↔ y = 0)
(x : G) :
(finsupp.single x r * f).support = finset.map (mul_left_embedding x) f.support
theorem
monoid_algebra.mem_span_support
{k : Type u₁}
{G : Type u₂}
[semiring k]
[mul_one_class G]
(f : monoid_algebra k G) :
f ∈ submodule.span k (⇑(monoid_algebra.of k G) '' ↑(f.support))
An element of monoid_algebra k G is in the subalgebra generated by its support.
theorem
add_monoid_algebra.support_mul_single
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_right_cancel_semigroup G]
(f : add_monoid_algebra k G)
(r : k)
(hr : ∀ (y : k), y * r = 0 ↔ y = 0)
(x : G) :
(f * finsupp.single x r).support = finset.map (add_right_embedding x) f.support
theorem
add_monoid_algebra.support_single_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_left_cancel_semigroup G]
(f : add_monoid_algebra k G)
(r : k)
(hr : ∀ (y : k), r * y = 0 ↔ y = 0)
(x : G) :
(finsupp.single x r * f).support = finset.map (add_left_embedding x) f.support
theorem
add_monoid_algebra.mem_span_support
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_zero_class G]
(f : add_monoid_algebra k G) :
f ∈ submodule.span k (⇑(add_monoid_algebra.of k G) '' ↑(f.support))
An element of add_monoid_algebra k G is in the submodule generated by its support.
theorem
add_monoid_algebra.mem_span_support'
{k : Type u₁}
{G : Type u₂}
[semiring k]
(f : add_monoid_algebra k G) :
f ∈ submodule.span k (add_monoid_algebra.of' k G '' ↑(f.support))
An element of add_monoid_algebra k G is in the subalgebra generated by its support, using
unbundled inclusion.