The basis of ideals

Some results involving Ideal and Basis.

noncomputable def Ideal.basisSpanSingleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] (b : Basis ι R S) {x : S} (hx : x ≠ 0) : Basis ι R ↥(Ideal.span {x})

A basis on S gives a basis on Ideal.span {x}, by multiplying everything by x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.basisSpanSingleton_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) : ↑((Ideal.basisSpanSingleton b hx) i) = x * b i

@[simp]

theorem Ideal.constr_basisSpanSingleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] {N : Type u_4} [Semiring N] [Module N S] [SMulCommClass R N S] (b : Basis ι R S) {x : S} (hx : x ≠ 0) : (↑(b.constr N)).toFun (Subtype.val ∘ ⇑(Ideal.basisSpanSingleton b hx)) = (Algebra.lmul R S) x

theorem Basis.mem_ideal_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S} (b : Basis ι R ↥I) {x : S} : x ∈ I ↔ ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) => x • ↑(b i)

If I : Ideal S has a basis over R, x ∈ I iff it is a linear combination of basis vectors.

theorem Basis.mem_ideal_iff' {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype ι] [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S} (b : Basis ι R ↥I) {x : S} : x ∈ I ↔ ∃ (c : ι → R), x = ∑ i : ι, c i • ↑(b i)

If I : Ideal S has a finite basis over R, x ∈ I iff it is a linear combination of basis vectors.