Absorption lemmas for the DGH stratification

Pointwise-set lemmas behind the Dubrovin–Gräter–Hanke stratification (Jakobs 2019, Def. 1.1.4): iterated sums sumPow, distributivity of a set over an n-term sum, absorption of a layer of inverses, the inverse of a sum of two inverses, and Hua's identity in a division ring.

Main results

• mul_sumPow_subset, inv_mul_subset_inv, inv_mul_sumPow_subset.
• inv_add_inv_inv, inv_add_inv_inv': (a⁻¹ + b⁻¹)⁻¹ = b (a + b)⁻¹ a = a (a + b)⁻¹ b (the "parallel sum"; one line from Mathlib's inv_add_inv').
• hua_classical: Hua's identity a − (a⁻¹ + (b⁻¹ − a)⁻¹)⁻¹ = a b a.

Related

The binary distributivity step is Mathlib's Set.mul_add_subset; the identity a⁻¹ + b⁻¹ = a⁻¹ (a + b) b⁻¹ is Mathlib's inv_add_inv' (invOf_add_invOf for Invertible).

References

• F. Jakobs, PhD thesis, 2019, Def. 1.1.4.
• L.-K. Hua, On the automorphisms of a sfield, Proc. Nat. Acad. Sci. USA 35 (1949), 386–389.

def DGH.sumPow {R : Type u_1} [Ring R] : ℕ → Set R → Set R

(a) sumPow n S = S + ⋯ + S (n summands), sumPow 0 S = {0}.

Equations

• DGH.sumPow 0 x✝ = {0}
• DGH.sumPow n.succ x✝ = x✝ + DGH.sumPow n x✝

@[simp]

theorem DGH.sumPow_zero {R : Type u_1} [Ring R] (S : Set R) : sumPow 0 S = {0}

@[simp]

theorem DGH.sumPow_succ {R : Type u_1} [Ring R] (n : ℕ) (S : Set R) : sumPow (n + 1) S = S + sumPow n S

theorem DGH.sumPow_mono {R : Type u_1} [Ring R] (n : ℕ) {S T : Set R} (h : S ⊆ T) : sumPow n S ⊆ sumPow n T

theorem DGH.mul_sumPow_subset {R : Type u_1} [Ring R] (X D : Set R) (n : ℕ) : X * sumPow n D ⊆ sumPow n (X * D)

(b) X * (D + ⋯ + D) ⊆ X*D + ⋯ + X*D (iterating Mathlib's Set.mul_add_subset).

theorem DGH.inv_mul_subset_inv {K : Type u_1} [DivisionRing K] {U S : Set K} (h : U⁻¹ * S ⊆ S) : S⁻¹ * U ⊆ S⁻¹

(c) If U⁻¹ * S ⊆ S then S⁻¹ * U ⊆ S⁻¹.

theorem DGH.inv_mul_sumPow_subset {K : Type u_1} [DivisionRing K] {U S : Set K} (h : U⁻¹ * S ⊆ S) (n : ℕ) : S⁻¹ * sumPow n U ⊆ sumPow n S⁻¹

(c) Corollary: a layer of inverses times an n-term polynomial in U stays in an n-term sum of inverses.

theorem DGH.inv_add_inv_inv {K : Type u_1} [DivisionRing K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : (a⁻¹ + b⁻¹)⁻¹ = b * (a + b)⁻¹ * a

(d) The inverse of a sum of two inverses ("parallel sum"), noncommutative form: (a⁻¹ + b⁻¹)⁻¹ = b (a + b)⁻¹ a. This is Mathlib's inv_add_inv' inverted with mul_inv_rev. It is not Hua's identity (that is hua_classical).

theorem DGH.inv_add_inv_inv' {K : Type u_1} [DivisionRing K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : (a⁻¹ + b⁻¹)⁻¹ = a * (a + b)⁻¹ * b

(d) The inverse of a sum of two inverses, symmetric form: (a⁻¹ + b⁻¹)⁻¹ = a (a + b)⁻¹ b.

@[deprecated DGH.inv_add_inv_inv (since := "2026-10-17")]

theorem DGH.hua_identity {K : Type u_1} [DivisionRing K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : (a⁻¹ + b⁻¹)⁻¹ = b * (a + b)⁻¹ * a

Alias of DGH.inv_add_inv_inv.

---

(d) The inverse of a sum of two inverses ("parallel sum"), noncommutative form: (a⁻¹ + b⁻¹)⁻¹ = b (a + b)⁻¹ a. This is Mathlib's inv_add_inv' inverted with mul_inv_rev. It is not Hua's identity (that is hua_classical).

@[deprecated DGH.inv_add_inv_inv' (since := "2026-10-17")]

theorem DGH.hua_identity' {K : Type u_1} [DivisionRing K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : (a⁻¹ + b⁻¹)⁻¹ = a * (a + b)⁻¹ * b

Alias of DGH.inv_add_inv_inv'.

---

(d) The inverse of a sum of two inverses, symmetric form: (a⁻¹ + b⁻¹)⁻¹ = a (a + b)⁻¹ b.

theorem DGH.hua_classical {K : Type u_1} [DivisionRing K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a * b ≠ 1) : a - (a⁻¹ + (b⁻¹ - a)⁻¹)⁻¹ = a * b * a

Hua's identity in a division ring: if a ≠ 0, b ≠ 0 and a b ≠ 1, then a − (a⁻¹ + (b⁻¹ − a)⁻¹)⁻¹ = a b a.