Groebner.MonomialOrderEmbedding

source

def RelHom.onFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) :

Function.onFun r f →r r

Equations

RelHom.onFun r f = { toFun := f, map_rel' := ⋯ }

Instances For

source

@[simp]

theorem RelHom.coe_onFun {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (f : α → β) :

⇑(onFun r f) = f

source

def MonomialOrder.ofInjective.Syn {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} (f : σ' → σ) :

Type u_3

Equations

MonomialOrder.ofInjective.Syn m f = (σ' →₀ ℕ)

Instances For

source

@[instance_reducible]

noncomputable instance MonomialOrder.ofInjective.acm' {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) (f : σ' → σ) :

AddCommMonoid (Syn m f)

Equations

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

source

noncomputable def MonomialOrder.ofInjective.toSyn' {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} (f : σ' → σ) :

(σ' →₀ ℕ) ≃+ Syn m f

Equations

MonomialOrder.ofInjective.toSyn' m f = AddEquiv.refl (σ' →₀ ℕ)

Instances For

source

theorem MonomialOrder.toIsOrderedCancelMonoid' {α : Type u_3} [CancelCommMonoid α] [LinearOrder α] [IsOrderedMonoid α] :

IsOrderedCancelMonoid α

source

theorem MonomialOrder.toIsOrderedCancelAddMonoid' {α : Type u_3} [AddCancelCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] :

IsOrderedCancelAddMonoid α

source

noncomputable def MonomialOrder.ofInjective {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} {f : σ' → σ} (hf : Function.Injective f) :

MonomialOrder σ'

Equations

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

Instances For

source

structure MonomialOrder.Embedding {σ' : Type u_1} (m' : MonomialOrder σ') {σ : Type u_2} (m : MonomialOrder σ) extends σ' ↪ σ :

Type (max u_1 u_2)

An embedding from a monomial order m' : MonomialOrder σ' and m : MonomialOrder σ consists:

a injective mapping from index σ' of m' to σ of m.
this mapping "preserves" the order.

toFun : σ' → σ
inj' : Injective self.toFun
monotone' : Monotone (⇑m.toSyn ∘ Finsupp.mapDomain self.toFun ∘ ⇑m'.toSyn.symm)

Instances For

source

@[instance_reducible]

instance MonomialOrder.Embedding.instFunLike {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} :

FunLike (m'.Embedding m) σ' σ

Equations

MonomialOrder.Embedding.instFunLike = { coe := fun (m_1 : m'.Embedding m) => m_1.toFun, coe_injective := ⋯ }

source

theorem MonomialOrder.Embedding.ext {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} {e₁ e₂ : m'.Embedding m} (h : ⇑e₁ = ⇑e₂) :

e₁ = e₂

source

theorem MonomialOrder.Embedding.ext_iff {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} {e₁ e₂ : m'.Embedding m} :

e₁ = e₂ ↔ ⇑e₁ = ⇑e₂

source

@[simp]

theorem MonomialOrder.Embedding.coe_toEmbedding_eq_coe {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

⇑e.toEmbedding = ⇑e

source

@[simp]

theorem MonomialOrder.Embedding.toFun_eq_coe {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

e.toFun = ⇑e

source

theorem MonomialOrder.Embedding.monotone {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

Monotone (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm)

source

@[simp]

theorem MonomialOrder.Embedding.coe_injective {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

Function.Injective ⇑e

source

theorem MonomialOrder.Embedding.toStrictMono {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

StrictMono (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm)

source

noncomputable def MonomialOrder.Embedding.toOrderEmbedding {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) :

m'.syn ↪o m.syn

Equations

e.toOrderEmbedding = OrderEmbedding.ofStrictMono (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm) ⋯

Instances For

source

@[simp]

theorem MonomialOrder.Embedding.le_iff_le {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : m'.syn) :

m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm a)) ≤ m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm b)) ↔ a ≤ b

source

@[simp]

theorem MonomialOrder.Embedding.le_iff_le' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : σ' →₀ ℕ) :

m.toSyn (Finsupp.mapDomain (⇑e) a) ≤ m.toSyn (Finsupp.mapDomain (⇑e) b) ↔ m'.toSyn a ≤ m'.toSyn b

source

@[simp]

theorem MonomialOrder.Embedding.lt_iff_lt {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : m'.syn) :

m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm a)) < m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm b)) ↔ a < b

source

@[simp]

theorem MonomialOrder.Embedding.lt_iff_lt' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : σ' →₀ ℕ) :

m.toSyn (Finsupp.mapDomain (⇑e) a) < m.toSyn (Finsupp.mapDomain (⇑e) b) ↔ m'.toSyn a < m'.toSyn b

source

def MonomialOrder.Embedding.ofInjective {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) {f : σ' → σ} (hf : Function.Injective f) :

(m.ofInjective hf).Embedding m

Given a monomial order m : MonomialOrder σ and a injective function f : σ' → σ, there exists an embedding ofInjective, from an m' : MonomialOrder σ' to m : MonomialOrder σ with mapping f.

Equations

MonomialOrder.Embedding.ofInjective m hf = { toFun := f, inj' := hf, monotone' := ⋯ }

Instances For

source

theorem MonomialOrder.Embedding.coe_ofInjective {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) {f : σ' → σ} (hf : Function.Injective f) :

⇑(ofInjective m hf) = f

source

theorem MonomialOrder.Embedding.degree_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) :

m.degree ((MvPolynomial.rename ⇑e) p) = Finsupp.mapDomain (⇑e) (m'.degree p)

Renaming with an monomial ordering embedding preserves degree.

source

@[simp]

theorem MonomialOrder.Embedding.degree_eq_degree {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.degree ((MvPolynomial.rename ⇑e) p) = m.degree ((MvPolynomial.rename ⇑e) q) ↔ m'.degree p = m'.degree q

source

@[simp]

theorem MonomialOrder.Embedding.degree_le_degree {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.toSyn (m.degree ((MvPolynomial.rename ⇑e) p)) ≤ m.toSyn (m.degree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toSyn (m'.degree p) ≤ m'.toSyn (m'.degree q)

source

@[simp]

theorem MonomialOrder.Embedding.degree_le_degree' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.degree ((MvPolynomial.rename ⇑e) p) ≤ m.degree ((MvPolynomial.rename ⇑e) q) ↔ m'.degree p ≤ m'.degree q

source

@[simp]

theorem MonomialOrder.Embedding.degree_lt_degree {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.toSyn (m.degree ((MvPolynomial.rename ⇑e) p)) < m.toSyn (m.degree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toSyn (m'.degree p) < m'.toSyn (m'.degree q)

source

theorem MonomialOrder.Embedding.withBotDegree_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) :

m.withBotDegree ((MvPolynomial.rename ⇑e) p) = WithBot.map (fun (x : σ' →₀ ℕ) => Finsupp.mapDomain (⇑e) x) (m'.withBotDegree p)

Renaming with an monomial ordering embedding preserves degree.

source

theorem MonomialOrder.Embedding.toWithBotSyn_withBotDegree_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ' R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) p)) = WithBot.map (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm) (m'.toWithBotSyn (m'.withBotDegree p))

source

@[simp]

theorem MonomialOrder.Embedding.withBotDegree_le_withBotDegree_iff {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) p)) ≤ m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toWithBotSyn (m'.withBotDegree p) ≤ m'.toWithBotSyn (m'.withBotDegree q)

source

theorem MonomialOrder.Embedding.withBotDegree_add_withBotDegree_le_withBotDegree_iff {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (r p q : MvPolynomial σ' R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) r) + m.withBotDegree ((MvPolynomial.rename ⇑e) p)) ≤ m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toWithBotSyn (m'.withBotDegree r + m'.withBotDegree p) ≤ m'.toWithBotSyn (m'.withBotDegree q)

source

@[simp]

theorem MonomialOrder.Embedding.withBotDegree_add_withBotDegree_le_withBotDegree_iff' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (r p q : MvPolynomial σ' R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) r)) + m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) p)) ≤ m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toWithBotSyn (m'.withBotDegree r) + m'.toWithBotSyn (m'.withBotDegree p) ≤ m'.toWithBotSyn (m'.withBotDegree q)

source

@[simp]

theorem MonomialOrder.Embedding.withBotDegree_lt_withBotDegree_iff {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ' R) :

m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) p)) < m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename ⇑e) q)) ↔ m'.toWithBotSyn (m'.withBotDegree p) < m'.toWithBotSyn (m'.withBotDegree q)

source

@[simp]

theorem MonomialOrder.Embedding.leadingCoeff_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) :

m.leadingCoeff ((MvPolynomial.rename ⇑e) p) = m'.leadingCoeff p

source

@[simp]

theorem MonomialOrder.Embedding.monic_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) :

m.Monic ((MvPolynomial.rename ⇑e) p) = m'.Monic p

source

theorem MonomialOrder.Embedding.leadingTerm_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) :

m.leadingTerm ((MvPolynomial.rename ⇑e) p) = (MvPolynomial.rename ⇑e) (m'.leadingTerm p)

source

theorem MonomialOrder.Embedding.sPolynomial_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommRing R] (p q : MvPolynomial σ' R) :

m.sPolynomial ((MvPolynomial.rename ⇑e) p) ((MvPolynomial.rename ⇑e) q) = (MvPolynomial.rename ⇑e) (m'.sPolynomial p q)