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' := ⋯ }

@[simp]

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

Equations

• ⋯ = ⋯

instance IsWellFounded.onFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) [wfl : IsWellFounded β r] : IsWellFounded α (Function.onFun r f)

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

Equations

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

@[implicit_reducible]

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

Equations

• MonomialOrder.ofInjective.acm' m f = inferInstanceAs (AddCommMonoid (σ' →₀ ℕ))

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 (σ' →₀ ℕ)

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

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

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.

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:

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

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

@[implicit_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' := ⋯ }

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

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

@[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

@[simp]

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

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)

@[simp]

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

def 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)

Equations

• ⋯ = ⋯

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) ⋯

@[simp]

def 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

Equations

• ⋯ = ⋯

@[simp]

def 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

Equations

• ⋯ = ⋯

@[simp]

def 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

Equations

• ⋯ = ⋯

@[simp]

def 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

Equations

• ⋯ = ⋯

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' := ⋯ }

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

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.

@[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

@[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)

@[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

@[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)

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.

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))

@[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)

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)

@[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)

@[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)

@[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

@[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

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)

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)