mathlib3 documentation

algebra.monoid_algebra.support

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) :
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) :
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 {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] [decidable_eq G] (a b : monoid_algebra k G) :
(a * b).support a.support.bUnion (λ (a₁ : G), b.support.bUnion (λ (a₂ : G), {a₁ * a₂}))
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) :
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) :

An element of monoid_algebra k G is in the subalgebra generated by its support.

theorem add_monoid_algebra.support_mul {k : Type u₁} {G : Type u₂} [semiring k] [decidable_eq G] [has_add G] (a b : add_monoid_algebra k G) :
(a * b).support a.support.bUnion (λ (a₁ : G), b.support.bUnion (λ (a₂ : G), {a₁ + a₂}))
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) :
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) :

An element of add_monoid_algebra k G is in the submodule generated by its support.

An element of add_monoid_algebra k G is in the subalgebra generated by its support, using unbundled inclusion.