Lemmas about ideals of MonoidAlgebra and AddMonoidAlgebra #
theorem
MonoidAlgebra.mem_ideal_span_of_image
{k : Type u_1}
{G : Type u_3}
[Monoid G]
[Semiring k]
{s : Set G}
{x : MonoidAlgebra k G}
:
x ∈ Ideal.span (⇑(MonoidAlgebra.of k G) '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'
If x belongs to the ideal generated by generators in s, then every element of the support of
x factors through an element of s.
We could spell ∃ d, m = d * m as MulOpposite.op m' ∣ MulOpposite.op m but this would be worse.
theorem
AddMonoidAlgebra.mem_ideal_span_of'_image
{k : Type u_1}
{A : Type u_2}
[AddMonoid A]
[Semiring k]
{s : Set A}
{x : AddMonoidAlgebra k A}
:
x ∈ Ideal.span (AddMonoidAlgebra.of' k A '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : A), m = d + m'
If x belongs to the ideal generated by generators in s, then every element of the support of
x factors additively through an element of s.