Lemmas about the sup and inf of the support of AddMonoidAlgebra #
TODO #
The current plan is to state and prove lemmas about Finset.sup (Finsupp.support f) D with a
"generic" degree/weight function D from the grading Type A to a somewhat ordered Type B.
Next, the general lemmas get specialized for some yet-to-be-defined degrees.
sup-degree and inf-degree of an AddMonoidAlgebra #
Let R be a semiring and let A be a SemilatticeSup.
For an element f : R[A], this file defines
AddMonoidAlgebra.supDegree: the sup-degree taking values inWithBot A,AddMonoidAlgebra.infDegree: the inf-degree taking values inWithTop A.
If the grading type A is a linearly ordered additive monoid, then these two notions of degree
coincide with the standard one:
- the sup-degree is the maximum of the exponents of the monomials that appear with non-zero
coefficient in
f, or⊥, iff = 0; - the inf-degree is the minimum of the exponents of the monomials that appear with non-zero
coefficient in
f, or⊤, iff = 0.
The main results are
AddMonoidAlgebra.supDegree_mul_le: the sup-degree of a product is at most the sum of the sup-degrees,AddMonoidAlgebra.le_infDegree_mul: the inf-degree of a product is at least the sum of the inf-degrees,AddMonoidAlgebra.supDegree_add_le: the sup-degree of a sum is at most the sup of the sup-degrees,AddMonoidAlgebra.le_infDegree_add: the inf-degree of a sum is at least the inf of the inf-degrees.
Implementation notes #
The current plan is to state and prove lemmas about Finset.sup (Finsupp.support f) D with a
"generic" degree/weight function D from the grading Type A to a somewhat ordered Type B.
Next, the general lemmas get specialized twice:
- once for
supDegree(essentially a simple application) and - once for
infDegree(a simple application, viaOrderDual).
These final lemmas are the ones that likely get used the most. The generic lemmas about
Finset.support.sup may not be used directly much outside of this file.
To see this in action, you can look at the triple
(sup_support_mul_le, maxDegree_mul_le, le_minDegree_mul).
In this section, we use degb and degt to denote "degree functions" on A with values in
a type with bot or top respectively.
theorem
AddMonoidAlgebra.sup_support_add_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[SemilatticeSup B]
[OrderBot B]
[Semiring R]
(degb : A → B)
(f g : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.le_inf_support_add
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[SemilatticeInf T]
[OrderTop T]
[Semiring R]
(degt : A → T)
(f g : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.sup_support_mul_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[SemilatticeSup B]
[OrderBot B]
[Semiring R]
[Add A]
[Add B]
[AddLeftMono B]
[AddRightMono B]
{degb : A → B}
(degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b)
(f g : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.le_inf_support_mul
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[SemilatticeInf T]
[OrderTop T]
[Semiring R]
[Add A]
[Add T]
[AddLeftMono T]
[AddRightMono T]
{degt : A → T}
(degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b))
(f g : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.sup_support_list_prod_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[SemilatticeSup B]
[OrderBot B]
[Semiring R]
[AddMonoid A]
[AddMonoid B]
[AddLeftMono B]
[AddRightMono B]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(l : List (AddMonoidAlgebra R A))
:
l.prod.support.sup degb ≤ (List.map (fun (f : AddMonoidAlgebra R A) => f.support.sup degb) l).sum
theorem
AddMonoidAlgebra.le_inf_support_list_prod
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[SemilatticeInf T]
[OrderTop T]
[Semiring R]
[AddMonoid A]
[AddMonoid T]
[AddLeftMono T]
[AddRightMono T]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(l : List (AddMonoidAlgebra R A))
:
(List.map (fun (f : AddMonoidAlgebra R A) => f.support.inf degt) l).sum ≤ l.prod.support.inf degt
theorem
AddMonoidAlgebra.sup_support_pow_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[SemilatticeSup B]
[OrderBot B]
[Semiring R]
[AddMonoid A]
[AddMonoid B]
[AddLeftMono B]
[AddRightMono B]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(n : ℕ)
(f : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.le_inf_support_pow
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[SemilatticeInf T]
[OrderTop T]
[Semiring R]
[AddMonoid A]
[AddMonoid T]
[AddLeftMono T]
[AddRightMono T]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(n : ℕ)
(f : AddMonoidAlgebra R A)
:
theorem
AddMonoidAlgebra.sup_support_multiset_prod_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[SemilatticeSup B]
[OrderBot B]
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[AddLeftMono B]
[AddRightMono B]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(m : Multiset (AddMonoidAlgebra R A))
:
m.prod.support.sup degb ≤ (Multiset.map (fun (f : AddMonoidAlgebra R A) => f.support.sup degb) m).sum
theorem
AddMonoidAlgebra.le_inf_support_multiset_prod
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[SemilatticeInf T]
[OrderTop T]
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid T]
[AddLeftMono T]
[AddRightMono T]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(m : Multiset (AddMonoidAlgebra R A))
:
(Multiset.map (fun (f : AddMonoidAlgebra R A) => f.support.inf degt) m).sum ≤ m.prod.support.inf degt
theorem
AddMonoidAlgebra.sup_support_finset_prod_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
{ι : Type u_6}
[SemilatticeSup B]
[OrderBot B]
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[AddLeftMono B]
[AddRightMono B]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(s : Finset ι)
(f : ι → AddMonoidAlgebra R A)
:
(∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb
theorem
AddMonoidAlgebra.le_inf_support_finset_prod
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
{ι : Type u_6}
[SemilatticeInf T]
[OrderTop T]
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid T]
[AddLeftMono T]
[AddRightMono T]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(s : Finset ι)
(f : ι → AddMonoidAlgebra R A)
:
∑ i ∈ s, (f i).support.inf degt ≤ (∏ i ∈ s, f i).support.inf degt
Shorthands for special cases #
Note that these definitions are reducible, in order to make it easier to apply the more generic lemmas above.
@[reducible, inline]
abbrev
AddMonoidAlgebra.supDegree
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
(D : A → B)
(f : AddMonoidAlgebra R A)
:
B
Let R be a semiring, let A be an AddZeroClass, let B be an OrderBot,
and let D : A → B be a "degree" function.
For an element f : R[A], the element supDegree f : B is the supremum of all the elements in the
support of f, or ⊥ if f is zero.
Often, the Type B is WithBot A,
If, further, A has a linear order, then this notion coincides with the usual one,
using the maximum of the exponents.
If A := σ →₀ ℕ then R[A] = MvPolynomial σ R, and if we equip σ with a linear order then
the induced linear order on Lex A equips MvPolynomial ring with a
monomial order (i.e. a linear order on A, the
type of (monic) monomials in R[A], that respects addition). We make use of this monomial order
by taking D := toLex, and different monomial orders could be accessed via different type
synonyms once they are added.
Equations
- AddMonoidAlgebra.supDegree D f = f.support.sup D
Instances For
theorem
AddMonoidAlgebra.supDegree_add_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{f g : AddMonoidAlgebra R A}
:
AddMonoidAlgebra.supDegree D (f + g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
@[simp]
theorem
AddMonoidAlgebra.supDegree_neg
{R' : Type u_2}
{A : Type u_3}
{B : Type u_5}
[Ring R']
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{f : AddMonoidAlgebra R' A}
:
theorem
AddMonoidAlgebra.supDegree_sub_le
{R' : Type u_2}
{A : Type u_3}
{B : Type u_5}
[Ring R']
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{f g : AddMonoidAlgebra R' A}
:
AddMonoidAlgebra.supDegree D (f - g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
theorem
AddMonoidAlgebra.supDegree_sum_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{ι : Type u_7}
{s : Finset ι}
{f : ι → AddMonoidAlgebra R A}
:
AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) ≤ s.sup fun (i : ι) => AddMonoidAlgebra.supDegree D (f i)
theorem
AddMonoidAlgebra.supDegree_single_ne_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
(a : A)
{r : R}
(hr : r ≠ 0)
:
AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = D a
theorem
AddMonoidAlgebra.supDegree_single
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
(a : A)
(r : R)
:
AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = if r = 0 then ⊥ else D a
theorem
AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{p : AddMonoidAlgebra R A}
{a : A}
(hlt : ¬D a ≤ AddMonoidAlgebra.supDegree D p)
:
p a = 0
theorem
AddMonoidAlgebra.supDegree_withBot_some_comp
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{s : AddMonoidAlgebra R A}
(hs : s.support.Nonempty)
:
AddMonoidAlgebra.supDegree (WithBot.some ∘ D) s = ↑(AddMonoidAlgebra.supDegree D s)
theorem
AddMonoidAlgebra.supDegree_eq_of_isMaxOn
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
{p : AddMonoidAlgebra R A}
{a : A}
(hmem : a ∈ p.support)
(hmax : IsMaxOn D (↑p.support) a)
:
AddMonoidAlgebra.supDegree D p = D a
@[simp]
theorem
AddMonoidAlgebra.supDegree_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
:
theorem
AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
{p : AddMonoidAlgebra R A}
:
AddMonoidAlgebra.supDegree D p ≠ ⊥ → p ≠ 0
theorem
AddMonoidAlgebra.ne_zero_of_not_supDegree_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
{p : AddMonoidAlgebra R A}
{b : B}
(h : ¬AddMonoidAlgebra.supDegree D p ≤ b)
:
p ≠ 0
theorem
AddMonoidAlgebra.supDegree_eq_of_max
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
{p : AddMonoidAlgebra R A}
{b : B}
(hb : b ∈ Set.range D)
(hmem : Function.invFun D b ∈ p.support)
(hmax : ∀ a ∈ p.support, D a ≤ b)
:
AddMonoidAlgebra.supDegree D p = b
theorem
AddMonoidAlgebra.supDegree_mul_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
{p q : AddMonoidAlgebra R A}
[Add B]
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
[AddLeftMono B]
[AddRightMono B]
:
AddMonoidAlgebra.supDegree D (p * q) ≤ AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.supDegree_prod_le
{R : Type u_7}
{A : Type u_8}
{B : Type u_9}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[SemilatticeSup B]
[OrderBot B]
[AddLeftMono B]
[AddRightMono B]
{D : A → B}
(hzero : D 0 = 0)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
{ι : Type u_10}
{s : Finset ι}
{f : ι → AddMonoidAlgebra R A}
:
AddMonoidAlgebra.supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, AddMonoidAlgebra.supDegree D (f i)
theorem
AddMonoidAlgebra.apply_add_of_supDegree_le
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[SemilatticeSup B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
{p q : AddMonoidAlgebra R A}
[Add B]
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
{ap aq : A}
(hp : AddMonoidAlgebra.supDegree D p ≤ D ap)
(hq : AddMonoidAlgebra.supDegree D q ≤ D aq)
:
noncomputable def
AddMonoidAlgebra.leadingCoeff
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
(D : A → B)
[Nonempty A]
(f : AddMonoidAlgebra R A)
:
R
If D is an injection into a linear order B, the leading coefficient of f : R[A] is the
nonzero coefficient of highest degree according to D, or 0 if f = 0. In general, it is defined
to be the coefficient at an inverse image of supDegree f (if such exists).
Equations
- AddMonoidAlgebra.leadingCoeff D f = f (Function.invFun D (AddMonoidAlgebra.supDegree D f))
Instances For
@[reducible]
def
AddMonoidAlgebra.Monic
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
(D : A → B)
[Nonempty A]
(f : AddMonoidAlgebra R A)
:
An element f : R[A] is monic if its leading coefficient is one.
Equations
- AddMonoidAlgebra.Monic D f = (AddMonoidAlgebra.leadingCoeff D f = 1)
Instances For
@[simp]
theorem
AddMonoidAlgebra.leadingCoeff_single
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
[Nonempty A]
(hD : Function.Injective D)
(a : A)
(r : R)
:
@[simp]
theorem
AddMonoidAlgebra.leadingCoeff_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
[Nonempty A]
:
theorem
AddMonoidAlgebra.Monic.ne_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
{D : A → B}
[Nonempty A]
[Nontrivial R]
(hp : AddMonoidAlgebra.Monic D p)
:
p ≠ 0
@[simp]
theorem
AddMonoidAlgebra.monic_one
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
(hD : Function.Injective D)
:
theorem
AddMonoidAlgebra.exists_supDegree_mem_support
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
(D : A → B)
(hp : p ≠ 0)
:
∃ a ∈ p.support, AddMonoidAlgebra.supDegree D p = D a
theorem
AddMonoidAlgebra.supDegree_mem_range
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
(D : A → B)
(hp : p ≠ 0)
:
theorem
AddMonoidAlgebra.supDegree_sum_lt
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
{ι : Type u_7}
{s : Finset ι}
{f : ι → AddMonoidAlgebra R A}
(hs : s.Nonempty)
{b : B}
(h : ∀ i ∈ s, AddMonoidAlgebra.supDegree D (f i) < b)
:
AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) < b
theorem
AddMonoidAlgebra.supDegree_add_eq_left
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(h : AddMonoidAlgebra.supDegree D q < AddMonoidAlgebra.supDegree D p)
:
AddMonoidAlgebra.supDegree D (p + q) = AddMonoidAlgebra.supDegree D p
theorem
AddMonoidAlgebra.supDegree_add_eq_right
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(h : AddMonoidAlgebra.supDegree D p < AddMonoidAlgebra.supDegree D q)
:
AddMonoidAlgebra.supDegree D (p + q) = AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.leadingCoeff_add_eq_left
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(h : AddMonoidAlgebra.supDegree D q < AddMonoidAlgebra.supDegree D p)
:
AddMonoidAlgebra.leadingCoeff D (p + q) = AddMonoidAlgebra.leadingCoeff D p
theorem
AddMonoidAlgebra.leadingCoeff_add_eq_right
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(h : AddMonoidAlgebra.supDegree D p < AddMonoidAlgebra.supDegree D q)
:
AddMonoidAlgebra.leadingCoeff D (p + q) = AddMonoidAlgebra.leadingCoeff D q
theorem
AddMonoidAlgebra.supDegree_mem_support
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(hD : Function.Injective D)
(hp : p ≠ 0)
:
Function.invFun D (AddMonoidAlgebra.supDegree D p) ∈ p.support
@[simp]
theorem
AddMonoidAlgebra.leadingCoeff_eq_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(hD : Function.Injective D)
:
AddMonoidAlgebra.leadingCoeff D p = 0 ↔ p = 0
theorem
AddMonoidAlgebra.leadingCoeff_ne_zero
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
(hD : Function.Injective D)
:
AddMonoidAlgebra.leadingCoeff D p ≠ 0 ↔ p ≠ 0
theorem
AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq
{A : Type u_3}
{B : Type u_5}
[LinearOrder B]
[OrderBot B]
{D : A → B}
[AddZeroClass A]
(hD : Function.Injective D)
{R : Type u_8}
[CommRing R]
{p q : AddMonoidAlgebra R A}
(hd : AddMonoidAlgebra.supDegree D p = AddMonoidAlgebra.supDegree D q)
(hc : AddMonoidAlgebra.leadingCoeff D p = AddMonoidAlgebra.leadingCoeff D q)
:
AddMonoidAlgebra.supDegree D (p - q) < AddMonoidAlgebra.supDegree D p ∨ p = q
theorem
AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
{ι : Type u_7}
{s : Finset ι}
{i : ι}
{f : ι → AddMonoidAlgebra R A}
[AddZeroClass A]
(hi : i ∈ s)
(hmax : ∀ j ∈ s, j ≠ i → AddMonoidAlgebra.supDegree D (f j) < AddMonoidAlgebra.supDegree D (f i))
:
AddMonoidAlgebra.supDegree D (∑ j ∈ s, f j) = AddMonoidAlgebra.supDegree D (f i) ∧ AddMonoidAlgebra.leadingCoeff D (∑ j ∈ s, f j) = AddMonoidAlgebra.leadingCoeff D (f i)
theorem
AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree'
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
{ι : Type u_7}
{s : Finset ι}
{f : ι → AddMonoidAlgebra R A}
[AddZeroClass A]
(hs : ∃ i ∈ s, f i ≠ 0)
(hd : Set.InjOn (AddMonoidAlgebra.supDegree D ∘ f) ↑s)
:
∑ i ∈ s, f i ≠ 0
theorem
AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{D : A → B}
{ι : Type u_7}
{s : Finset ι}
{f : ι → AddMonoidAlgebra R A}
[AddZeroClass A]
(hs : s ≠ ∅)
(hf : ∀ i ∈ s, f i ≠ 0)
(hd : Set.InjOn (AddMonoidAlgebra.supDegree D ∘ f) ↑s)
:
∑ i ∈ s, f i ≠ 0
theorem
AddMonoidAlgebra.apply_supDegree_add_supDegree
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
:
(p * q) (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
theorem
AddMonoidAlgebra.supDegree_mul
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hpq : AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q ≠ 0)
(hp : p ≠ 0)
(hq : q ≠ 0)
:
AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hq : AddMonoidAlgebra.Monic D q)
(hp : p ≠ 0)
:
AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hp : AddMonoidAlgebra.Monic D p)
(hq : q ≠ 0)
:
AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.Monic.supDegree_mul
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hbot : ⊥ + ⊥ = ⊥)
(hp : AddMonoidAlgebra.Monic D p)
(hq : AddMonoidAlgebra.Monic D q)
:
AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
theorem
AddMonoidAlgebra.leadingCoeff_mul
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
[NoZeroDivisors R]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
:
theorem
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hq : AddMonoidAlgebra.Monic D q)
:
AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p
theorem
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hp : AddMonoidAlgebra.Monic D p)
:
AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D q
theorem
AddMonoidAlgebra.Monic.mul
{R : Type u_1}
{A : Type u_3}
{B : Type u_5}
[Semiring R]
[LinearOrder B]
[OrderBot B]
{p q : AddMonoidAlgebra R A}
{D : A → B}
[AddZeroClass A]
[Add B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
(hD : Function.Injective D)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hp : AddMonoidAlgebra.Monic D p)
(hq : AddMonoidAlgebra.Monic D q)
:
AddMonoidAlgebra.Monic D (p * q)
theorem
AddMonoidAlgebra.Monic.pow
{R : Type u_1}
[Semiring R]
{A : Type u_8}
{B : Type u_9}
[AddMonoid A]
[AddMonoid B]
[LinearOrder B]
[OrderBot B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
{D : A → B}
{p : AddMonoidAlgebra R A}
{n : ℕ}
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hD : Function.Injective D)
(hp : AddMonoidAlgebra.Monic D p)
:
AddMonoidAlgebra.Monic D (p ^ n)
theorem
AddMonoidAlgebra.Monic.supDegree_pow
{R : Type u_1}
[Semiring R]
{A : Type u_8}
{B : Type u_9}
[AddMonoid A]
[AddMonoid B]
[LinearOrder B]
[OrderBot B]
[AddLeftStrictMono B]
[AddRightStrictMono B]
{D : A → B}
{p : AddMonoidAlgebra R A}
{n : ℕ}
(hzero : D 0 = 0)
(hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2)
(hD : Function.Injective D)
[Nontrivial R]
(hp : AddMonoidAlgebra.Monic D p)
:
AddMonoidAlgebra.supDegree D (p ^ n) = n • AddMonoidAlgebra.supDegree D p
@[reducible, inline]
abbrev
AddMonoidAlgebra.infDegree
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[Semiring R]
[SemilatticeInf T]
[OrderTop T]
(D : A → T)
(f : AddMonoidAlgebra R A)
:
T
Let R be a semiring, let A be an AddZeroClass, let T be an OrderTop,
and let D : A → T be a "degree" function.
For an element f : R[A], the element infDegree f : T is the infimum of all the elements in the
support of f, or ⊤ if f is zero.
Often, the Type T is WithTop A,
If, further, A has a linear order, then this notion coincides with the usual one,
using the minimum of the exponents.
Equations
- AddMonoidAlgebra.infDegree D f = f.support.inf D
Instances For
theorem
AddMonoidAlgebra.le_infDegree_add
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[Semiring R]
[SemilatticeInf T]
[OrderTop T]
(D : A → T)
(f g : AddMonoidAlgebra R A)
:
AddMonoidAlgebra.infDegree D f ⊓ AddMonoidAlgebra.infDegree D g ≤ AddMonoidAlgebra.infDegree D (f + g)
theorem
AddMonoidAlgebra.infDegree_withTop_some_comp
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[Semiring R]
[SemilatticeInf T]
[OrderTop T]
{D : A → T}
{s : AddMonoidAlgebra R A}
(hs : s.support.Nonempty)
:
AddMonoidAlgebra.infDegree (WithTop.some ∘ D) s = ↑(AddMonoidAlgebra.infDegree D s)
theorem
AddMonoidAlgebra.le_infDegree_mul
{R : Type u_1}
{A : Type u_3}
{T : Type u_4}
[Semiring R]
[SemilatticeInf T]
[OrderTop T]
[AddZeroClass A]
[Add T]
[AddLeftMono T]
[AddRightMono T]
(D : AddHom A T)
(f g : AddMonoidAlgebra R A)
:
AddMonoidAlgebra.infDegree (⇑D) f + AddMonoidAlgebra.infDegree (⇑D) g ≤ AddMonoidAlgebra.infDegree (⇑D) (f * g)