Lemmas about the support of an element of a skew monoid algebra

For f : SkewMonoidAlgebra k G, f.support is the set of all a ∈ G such that f.coeff a ≠ 0.

theorem SkewMonoidAlgebra.support_single_ne_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {b : k} (a : G) (h : b ≠ 0) : (single a b).support = {a}

theorem SkewMonoidAlgebra.support_single_subset {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : G} {b : k} : (single a b).support ⊆ {a}

theorem SkewMonoidAlgebra.support_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [DecidableEq G'] [AddCommMonoid k'] {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'} : (f.sum g).support ⊆ f.support.biUnion fun (a : G) => (g a (f.coeff a)).support

theorem SkewMonoidAlgebra.support_neg {k : Type u_1} {G : Type u_2} [AddCommGroup k] (p : SkewMonoidAlgebra k G) : (-p).support = p.support

theorem SkewMonoidAlgebra.support_one_subset {k : Type u_1} {G : Type u_2} [One G] [AddCommMonoidWithOne k] : support 1 ⊆ 1

@[simp]

theorem SkewMonoidAlgebra.support_one {k : Type u_1} {G : Type u_2} [One G] [AddCommMonoidWithOne k] [NeZero 1] : support 1 = 1

theorem SkewMonoidAlgebra.support_mul {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f g : SkewMonoidAlgebra k G) [DecidableEq G] : (f * g).support ⊆ f.support * g.support

theorem SkewMonoidAlgebra.support_single_mul_subset {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] (r : k) (a : G) : (single a r * f).support ⊆ Finset.image (fun (x : G) => a * x) f.support

theorem SkewMonoidAlgebra.support_mul_single_subset {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] (r : k) (a : G) : (f * single a r).support ⊆ Finset.image (fun (x : G) => x * a) f.support

theorem SkewMonoidAlgebra.support_single_mul_eq_image {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] {r : k} {x : G} (lx : IsLeftRegular x) (hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0) : (single x r * f).support = Finset.image (fun (x_1 : G) => x * x_1) f.support

theorem SkewMonoidAlgebra.support_mul_single_eq_image {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] {r : k} {x : G} (rx : IsRightRegular x) (hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0) : (f * single x r).support = Finset.image (fun (x_1 : G) => x_1 * x) f.support

theorem SkewMonoidAlgebra.support_mul_single {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] [IsRightCancelMul G] (r : k) (x : G) (hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0) : (f * single x r).support = Finset.map (mulRightEmbedding x) f.support

theorem SkewMonoidAlgebra.support_single_mul {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) [DecidableEq G] [IsLeftCancelMul G] (r : k) (x : G) (hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0) : (single x r * f).support = Finset.map (mulLeftEmbedding x) f.support

theorem SkewMonoidAlgebra.mem_span_support {k : Type u_1} {G : Type u_2} [Monoid G] [Semiring k] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) : f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

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