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.IsMinimal.isMinimal_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.IsMinimal ↔ (∀ p ∈ G, m.Monic p) ∧ G.Pairwise fun (x1 x2 : MvPolynomial σ R) => ¬m.degree x1 ≤ m.degree x2

Equations

⋯ = ⋯

Instances For

source

def MonomialOrder.IsGroebnerBasis.IsMinimal.monic {σ : 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) {p : MvPolynomial σ R} (h : p ∈ G) :

m.Monic p

Equations

⋯ = ⋯

Instances For

source

def MonomialOrder.IsGroebnerBasis.IsMinimal.pairwise {σ : 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) :

G.Pairwise fun (x1 x2 : MvPolynomial σ R) => ¬m.degree x1 ≤ m.degree x2

Equations

⋯ = ⋯

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.IsGroebnerBasis.isGroebnerBasis_minimal {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis G I) {G' : Set (MvPolynomial σ R)} (h : G' ⊆ ↑I) (hG' : ∀ g ∈ G', IsUnit (m.leadingCoeff g)) (h' : {a : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ m.degree '' (G \ {0})) a} ⊆ m.degree '' G') :

IsGroebnerBasis G' I

source

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (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

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.IsMinimal.isGroebnerBasis_of_isMinimal_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : IsGroebnerBasis (m.leadingTerm '' G) (Ideal.span (m.leadingTerm '' ↑I))) (hGsubset : G ⊆ ↑I) :

IsGroebnerBasis G I

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.injOn_degree {σ : 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) :

Set.InjOn m.degree G

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.minimal_degree {σ : 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) {g : MvPolynomial σ R} (h : g ∈ G) :

Minimal (fun (x : σ →₀ ℕ) => x ∈ m.degree '' G) (m.degree g)

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isMinimal_iff_monic_and_minimal_degree_and_injOn_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.IsMinimal ↔ (∀ g ∈ G, m.Monic g) ∧ (∀ g ∈ G, Minimal (fun (x : σ →₀ ℕ) => x ∈ m.degree '' G) (m.degree g)) ∧ Set.InjOn m.degree G

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.degree_image_eq_setOf_minimal {σ : 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.degree '' G = {a : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ m.degree '' G) a}

source

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

m.degree '' G = m.degree '' G₁

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.isMinimal_of_isMinimal_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {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.degree 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.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.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.withBotDegree_eq_of_isRemainder {σ : 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) {g : MvPolynomial σ R} (hg : g ∈ G) {r : MvPolynomial σ R} (hr : m.IsRemainder g (G \ {g}) r) :

m.withBotDegree r = m.withBotDegree g

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.degree_eq_of_isRemainder {σ : 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) {g : MvPolynomial σ R} (hg : g ∈ G) {r : MvPolynomial σ R} (hr : m.IsRemainder g (G \ {g}) r) :

m.degree r = m.degree g

source

theorem MonomialOrder.IsGroebnerBasis.IsMinimal.leadingTerm_eq_of_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) {g : MvPolynomial σ R} (hg : g ∈ G) (r : MvPolynomial σ R) (hr : m.IsRemainder g (G \ {g}) r) :

m.leadingTerm r = m.leadingTerm g

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

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.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) ∨ g = 0) :

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

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.exists_of_isGroebnerBasis' {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {I : Ideal (MvPolynomial σ k)} :

∃ (B : Set (MvPolynomial σ k)) (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

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) ∨ g = 0) :

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

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.uniqueExists {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (I : Ideal (MvPolynomial σ k)) :

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

source

theorem MonomialOrder.IsGroebnerBasis.isGroebnerBasis_minimalFor {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (I : Ideal (MvPolynomial σ k)) :

IsGroebnerBasis {g : MvPolynomial σ k | m.Monic g ∧ MinimalFor (fun (p : MvPolynomial σ k) => p ∈ ↑I \ {0}) (fun (x : MvPolynomial σ k) => m.degree x) g ∧ ∀ p ∈ I, p ≠ 0 → m.degree p ≠ m.degree g → ∀ a ∈ g.support, ¬m.degree p ≤ a} I

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_minimalFor {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (I : Ideal (MvPolynomial σ k)) :

⋯.IsReduced

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_iff_minimalFor {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (G : Set (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) :

(∃ (h : IsGroebnerBasis G I), h.IsReduced) ↔ ∀ (g : MvPolynomial σ k), g ∈ G ↔ m.Monic g ∧ MinimalFor (fun (p : MvPolynomial σ k) => p ∈ ↑I \ {0}) (fun (x : MvPolynomial σ k) => m.degree x) g ∧ ∀ p ∈ I, p ≠ 0 → m.degree p ≠ m.degree g → ∀ a ∈ g.support, ¬m.degree p ≤ a

source

theorem Filter.union_mem_of_mem {α : Type u_3} {a b : Set α} {f : Filter α} (ha : a ∈ f) (hb : b ∈ f) :

a ∪ b ∈ f

source

theorem Filter.biUnion_mem_of_mem {α : Type u_3} {ι : Type u_4} {f : Filter α} {s : Set ι} {t : ι → Set α} (hs : s.Nonempty) (hs' : s.Finite) (h : ∀ i ∈ s, t i ∈ f) :

⋃ i ∈ s, t i ∈ f

source

theorem Filter.sUnion_mem_of_mem {α : Type u_3} {f : Filter α} {s : Set (Set α)} (hs : s.Nonempty) (hs' : s.Finite) (h : ∀ a ∈ s, a ∈ f) :

⋃₀ s ∈ f

source

theorem Filter.iUnion_mem_of_mem {α : Type u_3} {ι : Type u_4} {f : Filter α} [Fintype ι] [nomempty : Nonempty ι] {s : ι → Set α} (h : ∀ (i : ι), s i ∈ f) :

Set.iUnion s ∈ f

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.subset_limsup {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_4} [Field k] {I : Ideal (MvPolynomial σ k)} {α : Type u_5} {σ' : α → Type u_3} {m' : (a : α) → MonomialOrder (σ' a)} {f : Filter α} {e : (a : α) → (m' a).Embedding m} (hI : Set.univ = Filter.liminf (fun (x : α) => Set.range ⇑(e x)) f) {G' : (a : α) → Set (MvPolynomial (σ' a) k)} (hG' : ∀ (a : α), IsGroebnerBasis (G' a) (Ideal.comap (MvPolynomial.rename ⇑(e a)) I)) (hG'' : ∀ (a : α), ⋯.IsReduced) {G : Set (MvPolynomial σ k)} {hG₀ : IsGroebnerBasis G I} (hG : hG₀.IsReduced) :

G ⊆ Filter.liminf (fun (a : α) => ⇑(MvPolynomial.rename ⇑(e a)) '' G' a) f

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_liminf {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_4} [Field k] {I : Ideal (MvPolynomial σ k)} {α : Type u_5} {σ' : α → Type u_3} {m' : (a : α) → MonomialOrder (σ' a)} {f : Filter α} [f.NeBot] {e : (a : α) → (m' a).Embedding m} (hI : Set.univ = Filter.liminf (fun (x : α) => Set.range ⇑(e x)) f) {G' : (a : α) → Set (MvPolynomial (σ' a) k)} (hG' : ∀ (a : α), IsGroebnerBasis (G' a) (Ideal.comap (MvPolynomial.rename ⇑(e a)) I)) (hG'' : ∀ (a : α), ⋯.IsReduced) :

∃ (h : IsGroebnerBasis (Filter.liminf (fun (a : α) => ⇑(MvPolynomial.rename ⇑(e a)) '' G' a) f) I), h.IsReduced

source

theorem MonomialOrder.IsGroebnerBasis.IsReduced.isReduced_liminf_nat {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {I : Ideal (MvPolynomial σ k)} {init : ℕ} {e : ℕ ≃ σ} {G' : (n : ℕ) → Set (MvPolynomial (Fin (n + init)) k)} (hG' : ∀ (n : ℕ), IsGroebnerBasis (G' n) (Ideal.comap (MvPolynomial.rename (⇑e ∘ Fin.val)) I)) (hG'' : ∀ (n : ℕ), ⋯.IsReduced) :

∃ (h : IsGroebnerBasis (Filter.liminf (fun (i : ℕ) => ⇑(MvPolynomial.rename (⇑e ∘ Fin.val)) '' G' i) Filter.cofinite) I), h.IsReduced