# 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

• AddMonoidAlgebra.supDegree: the sup-degree taking values in WithBot A,
• AddMonoidAlgebra.infDegree: the inf-degree taking values in WithTop 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 ⊥, if f = 0;
• the inf-degree is the minimum of the exponents of the monomials that appear with non-zero coefficient in f, or ⊤, if f = 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, via OrderDual).

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_2} {B : Type u_4} [] [] [] (degb : AB) (f : ) (g : ) :
Finset.sup (f + g).support degb Finset.sup f.support degb Finset.sup g.support degb
theorem AddMonoidAlgebra.le_inf_support_add {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] (degt : AT) (f : ) (g : ) :
Finset.inf f.support degt Finset.inf g.support degt Finset.inf (f + g).support degt
theorem AddMonoidAlgebra.sup_support_mul_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [Add A] [Add B] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degb : AB} (degbm : ∀ {a b : A}, degb (a + b) degb a + degb b) (f : ) (g : ) :
Finset.sup (f * g).support degb Finset.sup f.support degb + Finset.sup g.support degb
theorem AddMonoidAlgebra.le_inf_support_mul {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [Add A] [Add T] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degt : AT} (degtm : ∀ {a b : A}, degt a + degt b degt (a + b)) (f : ) (g : ) :
Finset.inf f.support degt + Finset.inf g.support degt Finset.inf (f * g).support degt
theorem AddMonoidAlgebra.sup_support_list_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [] [] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (l : List ()) :
Finset.sup ().support degb List.sum (List.map (fun f => Finset.sup f.support degb) l)
theorem AddMonoidAlgebra.le_inf_support_list_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [] [] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (l : List ()) :
List.sum (List.map (fun f => Finset.inf f.support degt) l) Finset.inf ().support degt
theorem AddMonoidAlgebra.sup_support_pow_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [] [] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (n : ) (f : ) :
Finset.sup (f ^ n).support degb n Finset.sup f.support degb
theorem AddMonoidAlgebra.le_inf_support_pow {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [] [] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (n : ) (f : ) :
n Finset.inf f.support degt Finset.inf (f ^ n).support degt
theorem AddMonoidAlgebra.sup_support_multiset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [] [] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (m : Multiset ()) :
Finset.sup ().support degb Multiset.sum (Multiset.map (fun f => Finset.sup f.support degb) m)
theorem AddMonoidAlgebra.le_inf_support_multiset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [] [] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (m : Multiset ()) :
Multiset.sum (Multiset.map (fun f => Finset.inf f.support degt) m) Finset.inf ().support degt
theorem AddMonoidAlgebra.sup_support_finset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} {ι : Type u_5} [] [] [] [] [] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degb : AB} (degb0 : degb 0 0) (degbm : ∀ (a b : A), degb (a + b) degb a + degb b) (s : ) (f : ι) :
Finset.sup (Finset.prod s fun i => f i).support degb Finset.sum s fun i => Finset.sup (f i).support degb
theorem AddMonoidAlgebra.le_inf_support_finset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} {ι : Type u_5} [] [] [] [] [] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {degt : AT} (degt0 : 0 degt 0) (degtm : ∀ (a b : A), degt a + degt b degt (a + b)) (s : ) (f : ι) :
(Finset.sum s fun i => Finset.inf (f i).support degt) Finset.inf (Finset.prod s fun i => f i).support 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]
def AddMonoidAlgebra.supDegree {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] (D : AB) (f : ) :
B

Let R be a semiring, let A, B be two AddZeroClasses, let B be an OrderBot, and let D : A → B be a "degree" function. For an element f : R[A], the 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.

Instances For
theorem AddMonoidAlgebra.supDegree_add_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [] (D : AB) (f : ) (g : ) :
theorem AddMonoidAlgebra.supDegree_mul_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [] [] [] [] [] [CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (D : A →+ B) (f : ) (g : ) :
@[reducible]
def AddMonoidAlgebra.infDegree {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] (D : AT) (f : ) :
T

Let R be a semiring, let A, B be two AddZeroClasses, let T be an OrderTop, and let D : A → T be a "degree" function. For an element f : R[A], the 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.

Instances For
theorem AddMonoidAlgebra.le_infDegree_add {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [] (D : AT) (f : ) (g : ) :
theorem AddMonoidAlgebra.le_infDegree_mul {R : Type u_1} {A : Type u_2} {T : Type u_3} [] [] [] [] [] [CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (D : A →+ T) (f : ) (g : ) :