Finite strata of the DGH stratification

With L = layer1 M and the hypothesis that the chain of iterated sums sumPow n L grows strictly for n ≥ 1:

Main results

• D_natCast_eq: D M n = sumPow n L for every natural n (the minimal case-1 multiset at stratum n ≥ 1 is n+1 copies of 1, via Jakobs' order);
• D_omega_eq, D_omega_sumClosed: D M ω = ⋃ n, sumPow n L, closed under sums;
• D_omega_subring: if moreover L * L ⊆ L, D M ω is the carrier of a subring of R;
• A3, A4: associativity and sum over a union, as set identities.

Iterated sums

theorem DGH.sumPow_one {R : Type} [Ring R] (S : Set R) : sumPow 1 S = S

theorem DGH.sumPow_add {R : Type} [Ring R] (a b : ℕ) (S : Set R) : sumPow (a + b) S = sumPow a S + sumPow b S

theorem DGH.sumPow_subset_succ {R : Type} [Ring R] {S : Set R} (h0 : 0 ∈ S) (n : ℕ) : sumPow n S ⊆ sumPow (n + 1) S

theorem DGH.sumPow_mono_le {R : Type} [Ring R] {S : Set R} (h0 : 0 ∈ S) {m n : ℕ} (h : m ≤ n) : sumPow m S ⊆ sumPow n S

theorem DGH.zero_mem_layer1 {R : Type} [Ring R] (M : Set R) : 0 ∈ layer1 M

theorem DGH.one_mem_layer1 {R : Type} [Ring R] (M : Set R) : 1 ∈ layer1 M

theorem DGH.neg_layer1_subset {R : Type} [Ring R] (M : Set R) : -layer1 M ⊆ layer1 M

theorem DGH.neg_sumPow_subset {R : Type} [Ring R] {S : Set R} (hS : -S ⊆ S) (n : ℕ) : -sumPow n S ⊆ sumPow n S

Lifting multisets of finite ordinals to ℕ

theorem DGH.exists_natCast_multiset (s : Multiset Ordinal.{0}) (n : ℕ) (h : ∀ x ∈ s, x ≤ ↑n) : ∃ (s' : Multiset ℕ), (∀ k ∈ s', k ≤ n) ∧ s = Multiset.map Nat.cast s'

theorem DGH.sumSets_map_natCast {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (S : Set R) (s' : Multiset ℕ) (hE : ∀ k ∈ s', E ↑k = sumPow k S) : sumSets E (Multiset.map Nat.cast s') = sumPow s'.sum S

theorem DGH.sum_le_count_one (s : Multiset ℕ) (h : ∀ k ∈ s, k ≤ 1) : s.sum ≤ Multiset.count 1 s

(1) Finite strata

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

Hypothesis H: the chain sumPow n (layer1 M) grows strictly from n = 1 on.

Equations

• DGH.StrictChain M = ∀ (n : ℕ), 1 ≤ n → ¬DGH.sumPow (n + 1) (DGH.layer1 M) ⊆ DGH.sumPow n (DGH.layer1 M)

theorem DGH.D_natCast_eq_aux {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) (n k : ℕ) : k ≤ n → D M ↑k = sumPow k (layer1 M)

(1) Under H, every finite stratum D M k (k ≤ n) is sumPow k (layer1 M).

theorem DGH.D_natCast_eq {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) (n : ℕ) : D M ↑n = sumPow n (layer1 M)

(1) Under H, D M n = sumPow n (layer1 M) for every n ≥ 1 (in fact for all n).

(2) The stratum ω

theorem DGH.omega0_not_succ : ¬∃ (a : Ordinal.{0}), Ordinal.omega0 = Order.succ a

theorem DGH.D_omega_eq {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) : D M Ordinal.omega0 = ⋃ (n : ℕ), sumPow n (layer1 M)

(2) Under H, D M ω = ⋃ n, sumPow n (layer1 M).

theorem DGH.D_omega_sumClosed {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) : SumClosed (D M Ordinal.omega0)

(2) Under H, D M ω is closed under sums.

(3) Products

theorem DGH.sumPow_mul_subset {R : Type} [Ring R] {L : Set R} (hLL : L * L ⊆ L) (a b : ℕ) : sumPow a L * sumPow b L ⊆ sumPow (a * b) L

theorem DGH.D_omega_mulClosed {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) (hLL : layer1 M * layer1 M ⊆ layer1 M) : MulClosed (D M Ordinal.omega0)

(3) Under H and L * L ⊆ L, D M ω is closed under products.

theorem DGH.D_omega_subring {R : Type} [Ring R] (M : Set R) (hH : StrictChain M) (hLL : layer1 M * layer1 M ⊆ layer1 M) : ∃ (S : Subring R), ↑S = D M Ordinal.omega0

(3) Under H and L * L ⊆ L, D M ω is a subring of R (contains 1).

(4) Set identities A3, A4

theorem DGH.A3 {R : Type} [Ring R] (X A B : Set R) : X * (A * B) = X * A * B

A3: X (A B) = (X A) B for pointwise products of sets; this is Mathlib's mul_assoc for Set R (a semigroup under Pointwise), kept under the label of the proof it belongs to.

theorem DGH.A4_eq {R : Type} [Ring R] {P D' E A B : Set R} (h : D' = E ∪ (A + B)) : P + D' = P + E ∪ (P + A + B)

A4: if D' = E ∪ (A + B) then P + D' ⊆ (P + E) ∪ (P + A + B) (indeed equal).

theorem DGH.A4 {R : Type} [Ring R] {P D' E A B : Set R} (h : D' = E ∪ (A + B)) : P + D' ⊆ P + E ∪ (P + A + B)