A max-additive degree from a separated multiplicative filtration

A decreasing, multiplicative filtration by ideals which is separated — every nonzero element eventually leaves it — determines a max-additive degree, valued in OrderDual ℕ because the filtration decreases. The generic construction can be reused for scalar extensions and quotient filtrations.

The file also proves that a ring with a separated multiplicative filtration and domain associated graded ring is itself a domain. The proof avoids MaxAddDegree.quotient_isDomain_of_associatedGraded_isDomain, whose [WellFoundedLT M] hypothesis fails for M = ℕᵒᵈ — precisely the value monoid of a decreasing ℕ-indexed filtration. The elementary route needs no well-foundedness.

structure IsSeparatedFiltration {R : Type u} [CommRing R] (F : ℕ → Ideal R) : Prop

A decreasing multiplicative filtration by ideals, separated in the sense that every nonzero element eventually leaves it.

• antitone : Antitone F

  The filtration is decreasing.

• top : F 0 = ⊤

  The zeroth stage is everything.

• mul_le (a b : ℕ) : F a * F b ≤ F (a + b)

  The filtration is multiplicative: F a · F b ⊆ F (a + b).

• exists_not_mem {x : R} : x ≠ 0 → ∃ (j : ℕ), x ∉ F j

  Every nonzero element eventually leaves the filtration.

noncomputable def IsSeparatedFiltration.firstExcluded {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) : ℕ

The first stage a nonzero element is absent from.

Equations

• hF.firstExcluded hx = Nat.find ⋯

theorem IsSeparatedFiltration.not_mem_firstExcluded {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) : x ∉ F (hF.firstExcluded hx)

theorem IsSeparatedFiltration.firstExcluded_le {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) {j : ℕ} (hj : x ∉ F j) : hF.firstExcluded hx ≤ j

theorem IsSeparatedFiltration.firstExcluded_pos {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) : 0 < hF.firstExcluded hx

theorem IsSeparatedFiltration.mem_iff_lt_firstExcluded {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) (j : ℕ) : x ∈ F j ↔ j < hF.firstExcluded hx

noncomputable def IsSeparatedFiltration.index {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) : ℕ

The largest stage containing a nonzero element.

Equations

• hF.index hx = hF.firstExcluded hx - 1

theorem IsSeparatedFiltration.mem_iff_le_index {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) (j : ℕ) : x ∈ F j ↔ j ≤ hF.index hx

noncomputable def IsSeparatedFiltration.value {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) : WithBot ℕᵒᵈ

The filtration index as a max-additive degree value, order-reversed.

Equations

• hF.value x = if hx : x = 0 then ⊥ else ↑(OrderDual.toDual (hF.index hx))

@[simp]

theorem IsSeparatedFiltration.value_zero {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) : hF.value 0 = ⊥

theorem IsSeparatedFiltration.value_of_ne_zero {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) {x : R} (hx : x ≠ 0) : hF.value x = ↑(OrderDual.toDual (hF.index hx))

theorem IsSeparatedFiltration.value_eq_bot_iff {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) : hF.value x = ⊥ ↔ x = 0

theorem IsSeparatedFiltration.value_le_toDual_iff {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) (j : ℕ) : hF.value x ≤ ↑(OrderDual.toDual j) ↔ x ∈ F j

theorem IsSeparatedFiltration.value_neg {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) : hF.value (-x) = hF.value x

theorem IsSeparatedFiltration.value_add_le_max {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x y : R) : hF.value (x + y) ≤ max (hF.value x) (hF.value y)

The ultrametric inequality, from additivity of each stage.

theorem IsSeparatedFiltration.value_mul_le_add {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x y : R) : hF.value (x * y) ≤ hF.value x + hF.value y

Subadditivity under multiplication, from the multiplicativity hypothesis.

theorem IsSeparatedFiltration.value_lt_toDual_iff {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) (j : ℕ) : hF.value x < ↑(OrderDual.toDual j) ↔ x ∈ F (j + 1)

noncomputable def IsSeparatedFiltration.degree {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) : MaxAddDegree R ℕᵒᵈ

The max-additive degree attached to a separated multiplicative filtration.

Equations

• hF.degree = { toFun := hF.value, map_zero' := ⋯, map_one_le_zero' := ⋯, map_neg' := ⋯, map_add_le_max' := ⋯, map_mul_le_add' := ⋯ }

@[simp]

theorem IsSeparatedFiltration.degree_apply {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (x : R) : hF.degree.toFun x = hF.value x

theorem IsSeparatedFiltration.degree_isSeparated {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) : hF.degree.IsSeparated

The attached degree is separated.

theorem IsSeparatedFiltration.isDomain_of_associatedGraded_isDomain {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) [IsDomain hF.degree.AssociatedGraded] : IsDomain R

A ring with a separated multiplicative filtration and domain associated graded ring is a domain.

The proof does not use MaxAddDegree.quotient_isDomain_of_associatedGraded_isDomain, whose [WellFoundedLT M] hypothesis fails for M = ℕᵒᵈ. Instead it obtains multiplicativity of the attached degree directly from the domain associated graded ring.

theorem IsSeparatedFiltration.mem_degree_filtrationLE_iff {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (j : ℕ) (x : R) : x ∈ hF.degree.filtrationLE (OrderDual.toDual j) ↔ x ∈ F j

The degree's weak filtration at dual index j is the stage F j.

theorem IsSeparatedFiltration.mem_degree_lowerFiltration_iff {R : Type u} [CommRing R] {F : ℕ → Ideal R} (hF : IsSeparatedFiltration F) (j : ℕ) (x : ↥(hF.degree.filtrationLE (OrderDual.toDual j))) : x ∈ hF.degree.lowerFiltration (OrderDual.toDual j) ↔ ↑x ∈ F (j + 1)

The degree's strict filtration at dual index j is the stage F (j+1).