Documentation

Mathlib.Algebra.MonoidAlgebra.Support

Lemmas about the support of a finitely supported function #

theorem MonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (a : MonoidAlgebra k G) (b : MonoidAlgebra k G) :
(a * b).support a.support * b.support
theorem MonoidAlgebra.support_single_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
(MonoidAlgebra.single a r * f).support Finset.image (fun (x : G) => a * x) f.support
theorem MonoidAlgebra.support_mul_single_subset {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
(f * MonoidAlgebra.single a r).support Finset.image (fun (x : G) => x * a) f.support
theorem MonoidAlgebra.support_single_mul_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ (y : k), r * y = 0 y = 0) {x : G} (lx : IsLeftRegular x) :
(MonoidAlgebra.single x r * f).support = Finset.image (fun (x_1 : G) => x * x_1) f.support
theorem MonoidAlgebra.support_mul_single_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ (y : k), y * r = 0 y = 0) {x : G} (rx : IsRightRegular x) :
(f * MonoidAlgebra.single x r).support = Finset.image (fun (x_1 : G) => x_1 * x) f.support
theorem MonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
(f * MonoidAlgebra.single x r).support = Finset.map (mulRightEmbedding x) f.support
theorem MonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ (y : k), r * y = 0 y = 0) (x : G) :
(MonoidAlgebra.single x r * f).support = Finset.map (mulLeftEmbedding x) f.support
theorem MonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :
1.support 1
@[simp]
theorem MonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] [NeZero 1] :
1.support = 1
theorem MonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) :
f Submodule.span k ((MonoidAlgebra.of k G) '' f.support)

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

theorem AddMonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Add G] (a : AddMonoidAlgebra k G) (b : AddMonoidAlgebra k G) :
(a * b).support a.support + b.support
theorem AddMonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [IsRightCancelAdd G] (f : AddMonoidAlgebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
theorem AddMonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [IsLeftCancelAdd G] (f : AddMonoidAlgebra k G) (r : k) (hr : ∀ (y : k), r * y = 0 y = 0) (x : G) :
(AddMonoidAlgebra.single x r * f).support = Finset.map (addLeftEmbedding x) f.support
theorem AddMonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :
1.support 0
@[simp]
theorem AddMonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] [NeZero 1] :
1.support = 0
theorem AddMonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) :
f Submodule.span k ((AddMonoidAlgebra.of k G) '' f.support)

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

theorem AddMonoidAlgebra.mem_span_support' {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) :
f Submodule.span k (AddMonoidAlgebra.of' k G '' f.support)

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