mathlib3 documentation

algebra.monoid_algebra.degree

Lemmas about the sup and inf of the support of add_monoid_algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Results about the finset.sup and finset.inf of finsupp.support #

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 add_monoid_algebra.sup_support_add_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [semilattice_sup B] [order_bot B] [semiring R] (degb : A B) (f g : add_monoid_algebra R A) :
(f + g).support.sup degb f.support.sup degb g.support.sup degb
theorem add_monoid_algebra.le_inf_support_add {R : Type u_1} {A : Type u_2} {T : Type u_3} [semilattice_inf T] [order_top T] [semiring R] (degt : A T) (f g : add_monoid_algebra R A) :
f.support.inf degt g.support.inf degt (f + g).support.inf degt
theorem add_monoid_algebra.sup_support_mul_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [semilattice_sup B] [order_bot B] [semiring R] [has_add A] [has_add B] [covariant_class B B has_add.add has_le.le] [covariant_class B B (function.swap has_add.add) has_le.le] {degb : A B} (degbm : {a b : A}, degb (a + b) degb a + degb b) (f g : add_monoid_algebra R A) :
(f * g).support.sup degb f.support.sup degb + g.support.sup degb
theorem add_monoid_algebra.le_inf_support_mul {R : Type u_1} {A : Type u_2} {T : Type u_3} [semilattice_inf T] [order_top T] [semiring R] [has_add A] [has_add T] [covariant_class T T has_add.add has_le.le] [covariant_class T T (function.swap has_add.add) has_le.le] {degt : A T} (degtm : {a b : A}, degt a + degt b degt (a + b)) (f g : add_monoid_algebra R A) :
f.support.inf degt + g.support.inf degt (f * g).support.inf degt
theorem add_monoid_algebra.sup_support_list_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [semilattice_sup B] [order_bot B] [semiring R] [add_monoid A] [add_monoid B] [covariant_class B B has_add.add has_le.le] [covariant_class B B (function.swap has_add.add) has_le.le] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (l : list (add_monoid_algebra R A)) :
l.prod.support.sup degb (list.map (λ (f : add_monoid_algebra R A), f.support.sup degb) l).sum
theorem add_monoid_algebra.le_inf_support_list_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [semilattice_inf T] [order_top T] [semiring R] [add_monoid A] [add_monoid T] [covariant_class T T has_add.add has_le.le] [covariant_class T T (function.swap has_add.add) has_le.le] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (l : list (add_monoid_algebra R A)) :
(list.map (λ (f : add_monoid_algebra R A), f.support.inf degt) l).sum l.prod.support.inf degt
theorem add_monoid_algebra.sup_support_pow_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [semilattice_sup B] [order_bot B] [semiring R] [add_monoid A] [add_monoid B] [covariant_class B B has_add.add has_le.le] [covariant_class B B (function.swap has_add.add) has_le.le] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (n : ) (f : add_monoid_algebra R A) :
(f ^ n).support.sup degb n f.support.sup degb
theorem add_monoid_algebra.le_inf_support_pow {R : Type u_1} {A : Type u_2} {T : Type u_3} [semilattice_inf T] [order_top T] [semiring R] [add_monoid A] [add_monoid T] [covariant_class T T has_add.add has_le.le] [covariant_class T T (function.swap has_add.add) has_le.le] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (n : ) (f : add_monoid_algebra R A) :
n f.support.inf degt (f ^ n).support.inf degt
theorem add_monoid_algebra.sup_support_multiset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} [semilattice_sup B] [order_bot B] [comm_semiring R] [add_comm_monoid A] [add_comm_monoid B] [covariant_class B B has_add.add has_le.le] [covariant_class B B (function.swap has_add.add) has_le.le] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (m : multiset (add_monoid_algebra R A)) :
m.prod.support.sup degb (multiset.map (λ (f : add_monoid_algebra R A), f.support.sup degb) m).sum
theorem add_monoid_algebra.le_inf_support_multiset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} [semilattice_inf T] [order_top T] [comm_semiring R] [add_comm_monoid A] [add_comm_monoid T] [covariant_class T T has_add.add has_le.le] [covariant_class T T (function.swap has_add.add) has_le.le] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (m : multiset (add_monoid_algebra R A)) :
(multiset.map (λ (f : add_monoid_algebra R A), f.support.inf degt) m).sum m.prod.support.inf degt
theorem add_monoid_algebra.sup_support_finset_prod_le {R : Type u_1} {A : Type u_2} {B : Type u_4} {ι : Type u_5} [semilattice_sup B] [order_bot B] [comm_semiring R] [add_comm_monoid A] [add_comm_monoid B] [covariant_class B B has_add.add has_le.le] [covariant_class B B (function.swap has_add.add) has_le.le] {degb : A B} (degb0 : degb 0 0) (degbm : (a b : A), degb (a + b) degb a + degb b) (s : finset ι) (f : ι add_monoid_algebra R A) :
(s.prod (λ (i : ι), f i)).support.sup degb s.sum (λ (i : ι), (f i).support.sup degb)
theorem add_monoid_algebra.le_inf_support_finset_prod {R : Type u_1} {A : Type u_2} {T : Type u_3} {ι : Type u_5} [semilattice_inf T] [order_top T] [comm_semiring R] [add_comm_monoid A] [add_comm_monoid T] [covariant_class T T has_add.add has_le.le] [covariant_class T T (function.swap has_add.add) has_le.le] {degt : A T} (degt0 : 0 degt 0) (degtm : (a b : A), degt a + degt b degt (a + b)) (s : finset ι) (f : ι add_monoid_algebra R A) :
s.sum (λ (i : ι), (f i).support.inf degt) (s.prod (λ (i : ι), f i)).support.inf degt