Documentation

Mathlib.RingTheory.Ideal.Basis

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.
Instances For
    @[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.