The degree over a subalgebra

Let ν be a max-additive degree on a commutative ring R and let P be a subalgebra of R. The level γ of the degree over P is the P-submodule generated by the elements of degree at most γ,

P · R_{ν ≤ γ}.

The degree over P, ν_P(t), is the least γ with t ∈ P · R_{ν ≤ γ}; for ν = deg on K((ℝ^{≤0})) and P = S, the series of finite degree, this is the paper's degree over S, deg_S. It is again a max-additive degree, it is bounded by ν, it is separated, and every non-zero element of P has degree zero over P.

def MaxAddDegree.degreeOverStage {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) (γ : M) : Submodule (↥P) R

The level P · R_{ν ≤ γ} of the degree over P: the P-submodule generated by the elements of degree at most γ.

Equations

• ν.degreeOverStage P γ = Submodule.span ↥P ↑(ν.filtrationLE γ)

theorem MaxAddDegree.degreeOverStage_le_iff {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) (N : Submodule (↥P) R) (γ : M) : ν.degreeOverStage P γ ≤ N ↔ ↑(ν.filtrationLE γ) ⊆ ↑N

theorem MaxAddDegree.mem_degreeOverStage_of_degree_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) {t : R} {γ : M} (ht : ν.toFun t ≤ ↑γ) : t ∈ ν.degreeOverStage P γ

theorem MaxAddDegree.degreeOverStage_mono {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) {γ γ' : M} (h : γ ≤ γ') : ν.degreeOverStage P γ ≤ ν.degreeOverStage P γ'

theorem MaxAddDegree.degreeOverStage_mul_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) (γ γ' : M) : ν.degreeOverStage P γ * ν.degreeOverStage P γ' ≤ ν.degreeOverStage P (γ + γ')

theorem MaxAddDegree.mul_mem_degreeOverStage {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) {γ γ' : M} {x y : R} (hx : x ∈ ν.degreeOverStage P γ) (hy : y ∈ ν.degreeOverStage P γ') : x * y ∈ ν.degreeOverStage P (γ + γ')

theorem MaxAddDegree.one_mem_degreeOverStage_zero {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) : 1 ∈ ν.degreeOverStage P 0

theorem MaxAddDegree.coe_mem_degreeOverStage_zero {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) (p : ↥P) : ↑p ∈ ν.degreeOverStage P 0

theorem MaxAddDegree.exists_mem_degreeOverStage {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) (t : R) : ∃ (γ : M), t ∈ ν.degreeOverStage P γ

noncomputable def MaxAddDegree.degreeOver {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] : MaxAddDegree R M

The degree over P, ν_P: the least γ with t ∈ P · R_{ν ≤ γ}, and -∞ at 0. For ν = deg and P = S this is the paper's deg_S.

Equations

• ν.degreeOver P = { toFun := MaxAddDegree.degreeOverFun✝ ν P, map_zero' := ⋯, map_one_le_zero' := ⋯, map_neg' := ⋯, map_add_le_max' := ⋯, map_mul_le_add' := ⋯ }

theorem MaxAddDegree.degreeOver_le_iff {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (t : R) (γ : M) : (ν.degreeOver P).toFun t ≤ ↑γ ↔ t ∈ ν.degreeOverStage P γ

theorem MaxAddDegree.degreeOver_eq_bot_iff {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (t : R) : (ν.degreeOver P).toFun t = ⊥ ↔ t = 0

theorem MaxAddDegree.degreeOver_isSeparated {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] : (ν.degreeOver P).IsSeparated

theorem MaxAddDegree.degreeOver_le_of_degree_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] {t : R} {γ : M} (ht : ν.toFun t ≤ ↑γ) : (ν.degreeOver P).toFun t ≤ ↑γ

theorem MaxAddDegree.degreeOver_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (hν : ν.IsSeparated) (t : R) : (ν.degreeOver P).toFun t ≤ ν.toFun t

theorem MaxAddDegree.degreeOver_coe_le_zero {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (p : ↥P) : (ν.degreeOver P).toFun ↑p ≤ 0

theorem MaxAddDegree.degreeOver_coe_mul_le_of_degree_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (p : ↥P) {t : R} {γ : M} (ht : ν.toFun t ≤ ↑γ) : (ν.degreeOver P).toFun (↑p * t) ≤ ↑γ

Multiplying an element of degree at most γ by an element of P keeps the degree over P at most γ.

theorem MaxAddDegree.coe_mul_mem_degreeOver_filtrationLE_of_degree_le {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (p : ↥P) {t : R} {γ : M} (ht : ν.toFun t ≤ ↑γ) : ↑p * t ∈ (ν.degreeOver P).filtrationLE γ

theorem MaxAddDegree.degreeOver_coe_eq_zero {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (h0 : ∀ (m : M), 0 ≤ m) {p : ↥P} (hp : ↑p ≠ 0) : (ν.degreeOver P).toFun ↑p = 0

When 0 is the least value, every non-zero element of P has degree exactly zero over P.

theorem MaxAddDegree.degreeOver_algebraMap_eq_zero {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] (h0 : ∀ (m : M), 0 ≤ m) {l : L} (hl : (algebraMap L R) l ≠ 0) : (ν.degreeOver P).toFun ((algebraMap L R) l) = 0

theorem MaxAddDegree.exists_mem_degreeOverStage_of_degreeOver_lt {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] {t : R} {γ : M} (ht : t ≠ 0) (h : (ν.degreeOver P).toFun t < ↑γ) : ∃ γ' < γ, t ∈ ν.degreeOverStage P γ'

Degree over P below γ means membership in a strictly lower level, for non-zero elements.

theorem MaxAddDegree.degreeOver_lt_of_mem_degreeOverStage_of_lt {R : Type u} {M : Type v} {L : Type w} [CommRing R] [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [CommRing L] [Algebra L R] (ν : MaxAddDegree R M) (P : Subalgebra L R) [WellFoundedLT M] {t : R} {γ' γ : M} (h : t ∈ ν.degreeOverStage P γ') (hlt : γ' < γ) : (ν.degreeOver P).toFun t < ↑γ