Groebner.Reduced

source

def MonomialOrder.IsGroebnerBasis.IsMinimal {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) :

Prop

Equations

hG.IsMinimal = ((∀ p ∈ G, m.Monic p) ∧ ∀ p ∈ G, ∀ q ∈ G, q ≠ p → ¬m.degree q ≤ m.degree p)

Instances For

source

def MonomialOrder.IsGroebnerBasis.IsReduced {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) :

Prop

Equations

hG.IsReduced = ((∀ p ∈ G, m.Monic p) ∧ ∀ p ∈ G, m.IsRemainder p (G \ {p}) p)

Instances For

source

theorem MonomialOrder.le_degree_of_mem_support {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {p : MvPolynomial σ R} {a : σ →₀ ℕ} (ha : a ∈ p.support) :

m.toSyn a ≤ m.toSyn (m.degree p)

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.singleton_zero_bot {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} :

IsGroebnerBasis {0} ⊥

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.empty_bot {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} :

IsGroebnerBasis ∅ ⊥

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.singleton_zero_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (I : Ideal (MvPolynomial σ R)) :

IsGroebnerBasis {0} I ↔ I = ⊥

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.empty_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (I : Ideal (MvPolynomial σ R)) :

IsGroebnerBasis ∅ I ↔ I = ⊥

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.of_subsingleton {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} [Subsingleton (MvPolynomial σ R)] {s : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} :

IsGroebnerBasis s I

source

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (s : Set (σ →₀ ℕ)) :

IsGroebnerBasis ((fun (x : σ →₀ ℕ) => (MvPolynomial.monomial x) 1) '' s) (Ideal.span ((fun (x : σ →₀ ℕ) => (MvPolynomial.monomial x) 1) '' s))

source

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_monomial_minimal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (s : Set (σ →₀ ℕ)) :

IsGroebnerBasis ((fun (x : σ →₀ ℕ) => (MvPolynomial.monomial x) 1) '' {x : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x}) (Ideal.span ((fun (x : σ →₀ ℕ) => (MvPolynomial.monomial x) 1) '' s))

source

theorem MonomialOrder.IsGroebnerBasis.smul {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {I : Ideal (MvPolynomial σ R)} {ι : Type u_3} (f : ι → R) (f' : ι → MvPolynomial σ R) (hf : ∀ (i : ι), IsUnit (f i)) (hG : IsGroebnerBasis (Set.range f') I) :

IsGroebnerBasis (Set.range fun (i : ι) => f i • f' i) I

source

theorem MonomialOrder.IsGroebnerBasis.smul_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {I : Ideal (MvPolynomial σ R)} {ι : Type u_3} (f : ι → R) (f' : ι → MvPolynomial σ R) (hf : ∀ (i : ι), IsUnit (f i)) :

IsGroebnerBasis (Set.range fun (i : ι) => f i • f' i) I ↔ IsGroebnerBasis (Set.range f') I

source

theorem MonomialOrder.IsGroebnerBasis.inv {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) (hG' : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :

IsGroebnerBasis (Set.range fun (g : ↑G) => ⋯.unit⁻¹ • ↑g) I

source

theorem MonomialOrder.IsGroebnerBasis.span_image_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) (hG' : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :

IsGroebnerBasis (m.leadingTerm '' G) (Ideal.span (m.leadingTerm '' ↑I))

source

theorem MonomialOrder.IsGroebnerBasis.IsRemainder.self_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (p : MvPolynomial σ R) (G : Set (MvPolynomial σ R)) :

m.IsRemainder p G p ↔ ∀ a ∈ p.support, ∀ q ∈ G, q ≠ 0 → ¬m.degree q ≤ a

source

theorem MonomialOrder.IsGroebnerBasis.IsRemainder.self_tfae {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (p : MvPolynomial σ R) (G : Set (MvPolynomial σ R)) :

[m.IsRemainder p G p, ∀ B' ⊆ G, m.IsRemainder p B' p, ∀ q ∈ G, m.IsRemainder p {q} p, ∀ a ∈ p.support, ∀ q ∈ G, q ≠ 0 → ¬m.degree q ≤ a].TFAE

source

theorem MonomialOrder.IsGroebnerBasis.IsRemainder.self {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {p r : MvPolynomial σ R} (h : m.IsRemainder p G r) :

m.IsRemainder r G r

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_def {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} :

hG.IsReduced ↔ (∀ p ∈ G, m.Monic p) ∧ ∀ p ∈ G, ∀ a ∈ p.support, ∀ q ∈ G, q ≠ p → ¬m.degree q ≤ a

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isMinimal {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} :

hG.IsReduced → hG.IsMinimal

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.IsReduced.of_subsingleton {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} [Subsingleton (MvPolynomial σ R)] {s : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} :

⋯.IsReduced

source

@[simp]

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.of_subsingleton {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} [Subsingleton (MvPolynomial σ R)] {s : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} :

⋯.IsMinimal

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {s : Set (σ →₀ ℕ)} {I : Ideal (MvPolynomial σ R)} (h : IsGroebnerBasis ((fun (x : σ →₀ ℕ) => (MvPolynomial.monomial x) 1) '' {x : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x}) I) :

h.IsReduced

source

@[simp]

theorem MonomialOrder.monic_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (p : MvPolynomial σ R) :

m.Monic (m.leadingTerm p) ↔ m.Monic p

source

theorem MonomialOrder.support_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (p : MvPolynomial σ R) [Decidable (p = 0)] :

(m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}

source

theorem MonomialOrder.support_leadingTerm' {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {p : MvPolynomial σ R} :

p ≠ 0 → (m.leadingTerm p).support = {m.degree p}

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.image_leadingTerm_eq_image_monomial_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} (hG' : hG.IsMinimal) :

m.leadingTerm '' G = (fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' G

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isReduced_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} (hG' : hG.IsMinimal) :

⋯.IsReduced

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.unique {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] [Nontrivial R] {G₁ G₂ : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG₁ : IsGroebnerBasis G₁ I} (hG₁' : hG₁.IsReduced) {hG₂ : IsGroebnerBasis G₂ I} (hG₂' : hG₂.IsReduced) :

G₁ = G₂

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isGroebnerBasis_of_isMinimal_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis (m.leadingTerm '' G) (Ideal.span (m.leadingTerm '' ↑I))) (hG' : hG.IsMinimal) (hGsubset : G ⊆ ↑I) :

IsGroebnerBasis G I

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isMinimal_of_isMinimal_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis (m.leadingTerm '' G) (Ideal.span (m.leadingTerm '' ↑I))} (hG' : hG.IsMinimal) (hGsubset : G ⊆ ↑I) (hLT : Set.InjOn m.leadingTerm G) :

⋯.IsMinimal

source

theorem MonomialOrder.IsGroebnerBasis.leadingCoeff_add_of_lt_right {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (f g : MvPolynomial σ R) (h : m.toSyn (m.degree f) < m.toSyn (m.degree g)) :

m.leadingCoeff (f + g) = m.leadingCoeff g

source

theorem MonomialOrder.IsGroebnerBasis.MonomialOrder.degree_le_mul_left {σ : Type u_3} {R : Type u_4} [CommRing R] [IsDomain R] (m : MonomialOrder σ) (p q : MvPolynomial σ R) (hq : q ≠ 0) :

m.degree p ≤ m.degree (p * q)

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isGroebnerBasis_image_isRemainder {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} (hG' : hG.IsMinimal) (f : ↑G → MvPolynomial σ R) (hf : ∀ (g : ↑G), m.IsRemainder (↑g) (G \ {↑g}) (f g)) :

IsGroebnerBasis (Set.range f) I

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_image_isRemainder_of_IsMinimal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {hG : IsGroebnerBasis G I} (hG' : hG.IsMinimal) (f : ↑G → MvPolynomial σ R) (hf : ∀ (g : ↑G), m.IsRemainder (↑g) (G \ {↑g}) (f g)) :

⋯.IsReduced

source

@[simp]

theorem MonomialOrder.leadingCoeff_mul' {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} [NoZeroDivisors R] {f g : MvPolynomial σ R} :

m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.exists_of_isGroebnerBasis {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) (hG' : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :

∃ (B : Set (MvPolynomial σ R)) (h : IsGroebnerBasis B I), h.IsReduced

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.uniqueExists_of_isGroebnerBasis {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [Nontrivial R] [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) (hG' : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :

∃! B : Set (MvPolynomial σ R), ∃ (h : IsGroebnerBasis B I), h.IsReduced