The Dubrovin–Gräter–Hanke stratification

The stratification D : Ordinal → Set R of a ring R generated by M ⊆ R, defined by well-founded recursion on ordinals. The minimal multiset of indices in cases 1–2 is chosen with WellFounded.min for Mathlib's Dershowitz–Manna order (Multiset.wellFounded_isDershowitzMannaLT).

Main results

• D_zero, D_one, D_succ, D_limit: the unfolding equations.
• D_succ_case1 … D_succ_case4: the four successor cases with their minimality specification.
• D_mono; D_ssubset_case1, D_ssubset_case2, D_ssubset_case3: monotonicity and strict growth.

References

• F. Jakobs, PhD thesis, 2019, Def. 1.1.4.
• N. Dubrovin, J. Gräter, T. Hanke.

theorem DGH.ord_succ_zero : Order.succ 0 = 1

theorem DGH.ord_succ_ne_zero (a : Ordinal.{0}) : Order.succ a ≠ 0

def DGH.sumSets {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (s : Multiset Ordinal.{0}) : Set R

D_{α₁} + ⋯ + D_{αₙ} for the multiset {α₁,…,αₙ}.

Equations

• DGH.sumSets E s = (Multiset.map E s).sum

def DGH.prodSets {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (s : Multiset Ordinal.{0}) : Set R

⋃ over all orderings l of the multiset s of D_{l₁} ⋯ D_{lₙ}.

Equations

• DGH.prodSets E s = ⋃ (l : List Ordinal.{0}), ⋃ (_ : ↑l = s), (List.map E l).prod

def DGH.invSet {R : Type} [Ring R] (S : Set R) : Set R

Inverses of the units of R lying in S.

Equations

• DGH.invSet S = {x : R | ∃ (u : Rˣ), ↑u ∈ S ∧ x = ↑u⁻¹}

def DGH.SumClosed {R : Type} [Ring R] (S : Set R) : Prop

Equations

• DGH.SumClosed S = (S + S ⊆ S)

def DGH.MulClosed {R : Type} [Ring R] (S : Set R) : Prop

Equations

• DGH.MulClosed S = (S * S ⊆ S)

def DGH.InvClosed {R : Type} [Ring R] (S : Set R) : Prop

"rationally closed": contains the inverse of each unit of R it contains.

Equations

• DGH.InvClosed S = (DGH.invSet S ⊆ S)

def DGH.sumCand {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Set (Multiset Ordinal.{0})

Candidates for case 1.

Equations

• DGH.sumCand E a = {s : Multiset Ordinal.{0} | s ≠ 0 ∧ (∀ x ∈ s, x ≤ a) ∧ ¬DGH.sumSets E s ⊆ E a}

def DGH.prodCand {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Set (Multiset Ordinal.{0})

Candidates for case 2.

Equations

• DGH.prodCand E a = {s : Multiset Ordinal.{0} | s ≠ 0 ∧ (∀ x ∈ s, x ≤ a) ∧ ¬DGH.prodSets E s ⊆ E a}

def DGH.invCand {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Set Ordinal.{0}

Candidates for case 3.

Equations

• DGH.invCand E a = {b : Ordinal.{0} | b ≤ a ∧ ¬DGH.invSet (E b) ⊆ E a}

theorem DGH.sumSets_pair {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : sumSets E {a, a} = E a + E a

theorem DGH.prodSets_pair {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : E a * E a ⊆ prodSets E {a, a}

theorem DGH.sumCand_nonempty {R : Type} [Ring R] {E : Ordinal.{0} → Set R} {a : Ordinal.{0}} (h : ¬SumClosed (E a)) : (sumCand E a).Nonempty

theorem DGH.prodCand_nonempty {R : Type} [Ring R] {E : Ordinal.{0} → Set R} {a : Ordinal.{0}} (h : ¬MulClosed (E a)) : (prodCand E a).Nonempty

theorem DGH.invCand_nonempty {R : Type} [Ring R] {E : Ordinal.{0} → Set R} {a : Ordinal.{0}} (h : ¬InvClosed (E a)) : (invCand E a).Nonempty

noncomputable def DGH.succStep₀ {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Set R

Successor step on an arbitrary family E (raw form).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DGH.restr {R : Type} (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Ordinal.{0} → Set R

Restriction of a family to indices ≤ a.

Equations

• DGH.restr E a b = if b ≤ a then E b else ∅

noncomputable def DGH.succStep {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : Set R

Successor step: only looks at E b for b ≤ a.

Equations

• DGH.succStep E a = DGH.succStep₀ (DGH.restr E a) a

theorem DGH.succStep_congr {R : Type} [Ring R] {E F : Ordinal.{0} → Set R} {a : Ordinal.{0}} (h : ∀ b ≤ a, E b = F b) : succStep E a = succStep F a

def DGH.layer1 {R : Type} [Ring R] (M : Set R) : Set R

D_1 = {0, 1, -1} ∪ M ∪ -M.

Equations

• DGH.layer1 M = {0, 1, -1} ∪ M ∪ -M

noncomputable def DGH.core {R : Type} [Ring R] (M : Set R) (α : Ordinal.{0}) (E : Ordinal.{0} → Set R) : Set R

One step of the recursion, given the family E of earlier strata.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DGH.D {R : Type} [Ring R] (M : Set R) : Ordinal.{0} → Set R

The DGH stratification.

Equations

• DGH.D M = DGH.succStep₀._proof_2.fix fun (α : Ordinal.{0}) (IH : (y : Ordinal.{0}) → y < α → Set R) => DGH.core M α fun (b : Ordinal.{0}) => if h : b < α then IH b h else ∅

theorem DGH.D_eq {R : Type} [Ring R] (M : Set R) (α : Ordinal.{0}) : D M α = core M α fun (b : Ordinal.{0}) => if b < α then D M b else ∅

Unfolding equations

theorem DGH.D_zero {R : Type} [Ring R] (M : Set R) : D M 0 = {0}

theorem DGH.D_one {R : Type} [Ring R] (M : Set R) : D M 1 = layer1 M

theorem DGH.D_succ {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (ha : a ≠ 0) : D M (Order.succ a) = succStep (D M) a

theorem DGH.D_limit {R : Type} [Ring R] (M : Set R) {α : Ordinal.{0}} (h0 : α ≠ 0) (hs : ¬∃ (a : Ordinal.{0}), α = Order.succ a) : D M α = ⋃ (b : Ordinal.{0}), ⋃ (_ : b < α), D M b

The four successor cases (for a ≠ 0)

theorem DGH.restr_self {R : Type} (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : restr E a a = E a

theorem DGH.sumSets_restr {R : Type} [Ring R] {E : Ordinal.{0} → Set R} {a : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : ∀ x ∈ s, x ≤ a) : sumSets (restr E a) s = sumSets E s

theorem DGH.prodSets_restr {R : Type} [Ring R] {E : Ordinal.{0} → Set R} {a : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : ∀ x ∈ s, x ≤ a) : prodSets (restr E a) s = prodSets E s

theorem DGH.sumCand_restr {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : sumCand (restr E a) a = sumCand E a

theorem DGH.prodCand_restr {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : prodCand (restr E a) a = prodCand E a

theorem DGH.invCand_restr {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : invCand (restr E a) a = invCand E a

theorem DGH.D_succ_case1 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (ha : a ≠ 0) (h1 : ¬SumClosed (D M a)) : ∃ s ∈ sumCand (D M) a, (∀ t ∈ sumCand (D M) a, ¬t.IsDershowitzMannaLT s) ∧ D M (Order.succ a) = D M a ∪ sumSets (D M) s

Case 1: D a not closed under sums.

theorem DGH.D_succ_case2 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (ha : a ≠ 0) (h1 : SumClosed (D M a)) (h2 : ¬MulClosed (D M a)) : ∃ s ∈ prodCand (D M) a, (∀ t ∈ prodCand (D M) a, ¬t.IsDershowitzMannaLT s) ∧ D M (Order.succ a) = D M a ∪ prodSets (D M) s

Case 2: D a closed under sums, not under products.

theorem DGH.D_succ_case3 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (ha : a ≠ 0) (h1 : SumClosed (D M a)) (h2 : MulClosed (D M a)) (h3 : ¬InvClosed (D M a)) : ∃ b ∈ invCand (D M) a, (∀ c ∈ invCand (D M) a, ¬c < b) ∧ D M (Order.succ a) = D M a ∪ invSet (D M b)

Case 3: D a closed under sums and products, not rationally closed.

theorem DGH.D_succ_case4 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (ha : a ≠ 0) (h1 : SumClosed (D M a)) (h2 : MulClosed (D M a)) (h3 : InvClosed (D M a)) : D M (Order.succ a) = D M a

Case 4: otherwise the stratum does not grow.

Monotonicity

theorem DGH.D_subset_succ {R : Type} [Ring R] (M : Set R) (a : Ordinal.{0}) : D M a ⊆ D M (Order.succ a)

theorem DGH.D_mono {R : Type} [Ring R] (M : Set R) {b α : Ordinal.{0}} (h : b ≤ α) : D M b ⊆ D M α

Strict growth

theorem DGH.D_ssubset_case1 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (h1 : ¬SumClosed (D M a)) : D M a ⊂ D M (Order.succ a)

theorem DGH.D_ssubset_case2 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (h1 : SumClosed (D M a)) (h2 : ¬MulClosed (D M a)) : D M a ⊂ D M (Order.succ a)

theorem DGH.D_ssubset_case3 {R : Type} [Ring R] (M : Set R) {a : Ordinal.{0}} (h1 : SumClosed (D M a)) (h2 : MulClosed (D M a)) (h3 : ¬InvClosed (D M a)) : D M a ⊂ D M (Order.succ a)