Documentation

Mathlib.Algebra.MonoidAlgebra.Degree

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

If the grading type A is a linearly ordered additive monoid, then these two notions of degree coincide with the standard one:

The main results are

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:

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 : AB) (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra R A) :
(f + g).support.sup degb f.support.sup degb g.support.sup degb
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 : AT) (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra R A) :
f.support.inf degt g.support.inf degt (f + g).support.inf degt
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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {degb : AB} (degbm : ∀ {a b : A}, degb (a + b) degb a + degb b) (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra R A) :
(f * g).support.sup degb f.support.sup degb + g.support.sup degb
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] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] {degt : AT} (degtm : ∀ {a b : A}, degt a + degt b degt (a + b)) (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra R A) :
f.support.inf degt + g.support.inf degt (f * g).support.inf degt
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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {degb : AB} (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] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] {degt : AT} (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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (n : ) (f : AddMonoidAlgebra R A) :
(f ^ n).support.sup degb n f.support.sup degb
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] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (n : ) (f : AddMonoidAlgebra R A) :
n f.support.inf degt (f ^ n).support.inf degt
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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {degb : AB} (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] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] {degt : AT} (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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (s : Finset ι) (f : ιAddMonoidAlgebra R A) :
(is, f i).support.sup degb is, (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] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (s : Finset ι) (f : ιAddMonoidAlgebra R A) :
is, (f i).support.inf degt (is, 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 : AB) (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.

Equations
Instances For
    @[simp]
    theorem AddMonoidAlgebra.supDegree_neg {R' : Type u_2} {A : Type u_3} {B : Type u_5} [Ring R'] [AddZeroClass A] [SemilatticeSup B] [OrderBot B] {D : AB} {f : AddMonoidAlgebra R' A} :
    theorem AddMonoidAlgebra.supDegree_sum_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : AB} {ι : Type u_7} {s : Finset ι} {f : ιAddMonoidAlgebra R A} :
    AddMonoidAlgebra.supDegree D (is, 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 : AB} (a : A) {r : R} (hr : r 0) :
    theorem AddMonoidAlgebra.supDegree_single {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : AB} (a : A) (r : R) :
    @[simp]
    theorem AddMonoidAlgebra.supDegree_zero {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [AddZeroClass A] [SemilatticeSup B] [OrderBot B] {D : AB} :
    theorem AddMonoidAlgebra.ne_zero_of_not_supDegree_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [AddZeroClass A] [SemilatticeSup B] [OrderBot B] {D : AB} {p : AddMonoidAlgebra R A} {b : B} (h : ¬AddMonoidAlgebra.supDegree D p b) :
    p 0
    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 : AB} {p : AddMonoidAlgebra R A} {a : A} (hlt : ¬D a AddMonoidAlgebra.supDegree D p) :
    p a = 0
    theorem AddMonoidAlgebra.supDegree_mul_le {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [AddZeroClass A] [SemilatticeSup B] [Add B] [OrderBot B] {D : AB} {p : AddMonoidAlgebra R A} {q : AddMonoidAlgebra R A} (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] :
    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] [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x x_1] {D : AB} (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 (is, f i) is, 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] [AddZeroClass A] [SemilatticeSup B] [Add B] [OrderBot B] {D : AB} {p : AddMonoidAlgebra R A} {q : AddMonoidAlgebra R A} (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [CovariantClass B B (fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x < x_1] [CovariantClass B B (Function.swap fun (x x_1 : B) => x + x_1) fun (x x_1 : B) => x < x_1] (hD : Function.Injective D) {ap : A} {aq : A} (hp : AddMonoidAlgebra.supDegree D p D ap) (hq : AddMonoidAlgebra.supDegree D q D aq) :
    (p * q) (ap + aq) = p ap * q aq
    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 : AB} {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    @[reducible, inline]
    abbrev AddMonoidAlgebra.infDegree {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [SemilatticeInf T] [OrderTop T] (D : AT) (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
    Instances For
      theorem AddMonoidAlgebra.le_infDegree_mul {R : Type u_1} {A : Type u_3} {T : Type u_4} [Semiring R] [AddZeroClass A] [SemilatticeInf T] [Add T] [OrderTop T] [CovariantClass T T (fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] [CovariantClass T T (Function.swap fun (x x_1 : T) => x + x_1) fun (x x_1 : T) => x x_1] (D : AddHom A T) (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra R A) :
      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 : AT} {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :