feat(ring_theory/hahn_series): Hahn series form a field (#7495)

Uses Higman's Lemma to define `summable_family.powers`, a summable family consisting of the powers of a Hahn series of positive valuation
Uses `summable_family.powers` to define inversion on Hahn series over a field and linear-ordered value group, making the type of Hahn series a field.
Shows that a Hahn series over an integral domain and linear-ordered value group  `is_unit` if and only if its lowest coefficient is.

Author: awainverse

src/order/well_founded_set.lean

@@ -68,6 +68,17 @@ begin
     exact ⟨m, mt, λ x xt ⟨xm, xs, ms⟩, hst ⟨m, ⟨ms, mt⟩⟩⟩ }
 end
 
+lemma well_founded_on.induction {s : set α} {r : α → α → Prop} (hs : s.well_founded_on r) {x : α}
+  (hx : x ∈ s) {P : α → Prop} (hP : ∀ (y ∈ s), (∀ (z ∈ s), r z y → P z) → P y) :
+  P x :=
+begin
+  let Q : s → Prop := λ y, P y,
+  change Q ⟨x, hx⟩,
+  refine well_founded.induction hs ⟨x, hx⟩ _,
+  rintros ⟨y, ys⟩ ih,
+  exact hP _ ys (λ z zs zy, ih ⟨z, zs⟩ zy),
+end
+
 instance is_strict_order.subset {s : set α} {r : α → α → Prop} [is_strict_order α r] :
   is_strict_order α (λ (a b : α), r a b ∧ a ∈ s ∧ b ∈ s) :=
 { to_is_irrefl := ⟨λ a con, irrefl_of r a con.1 ⟩,
@@ -176,17 +187,18 @@ theorem partially_well_ordered_on.mono {s t : set α} {r : α → α → Prop}
   s.partially_well_ordered_on r :=
 λ f hf, ht f (set.subset.trans hf hsub)
 
-theorem partially_well_ordered_on.image_of_monotone {s : set α}
+theorem partially_well_ordered_on.image_of_monotone_on {s : set α}
   {r : α → α → Prop} {β : Type*} {r' : β → β → Prop}
-  (hs : s.partially_well_ordered_on r) {f : α → β} (hf : ∀ a1 a2 : α, r a1 a2 → r' (f a1) (f a2)) :
+  (hs : s.partially_well_ordered_on r) {f : α → β}
+  (hf : ∀ a1 a2 : α, a1 ∈ s → a2 ∈ s → r a1 a2 → r' (f a1) (f a2)) :
   (f '' s).partially_well_ordered_on r' :=
 λ g hg, begin
   have h := λ (n : ℕ), ((mem_image _ _ _).1 (hg (mem_range_self n))),
   obtain ⟨m, n, hlt, hmn⟩ := hs (λ n, classical.some (h n)) _,
   { refine ⟨m, n, hlt, _⟩,
     rw [← (classical.some_spec (h m)).2,
       ← (classical.some_spec (h n)).2],
-    apply hf _ _ hmn },
+    exact hf _ _ (classical.some_spec (h m)).1 (classical.some_spec (h n)).1 hmn },
   { rintros _ ⟨n, rfl⟩,
     exact (classical.some_spec (h n)).1 }
 end
@@ -282,7 +294,7 @@ end
 theorem is_pwo.image_of_monotone {β : Type*} [partial_order β]
   (hs : s.is_pwo) {f : α → β} (hf : monotone f) :
   is_pwo (f '' s) :=
-hs.image_of_monotone hf
+hs.image_of_monotone_on (λ _ _ _ _ ab, hf ab)
 
 theorem is_pwo.union (hs : is_pwo s) (ht : is_pwo t) : is_pwo (s ∪ t) :=
 begin
@@ -635,6 +647,41 @@ end
 
 end partially_well_ordered_on
 
+namespace is_pwo
+
+@[to_additive]
+lemma submonoid_closure [ordered_cancel_comm_monoid α] {s : set α} (hpos : ∀ x : α, x ∈ s → 1 ≤ x)
+  (h : s.is_pwo) : is_pwo ((submonoid.closure s) : set α) :=
+begin
+  have hl : ((submonoid.closure s) : set α) ⊆ list.prod '' { l : list α | ∀ x, x ∈ l → x ∈ s },
+  { intros x hx,
+    rw set_like.mem_coe at hx,
+    refine submonoid.closure_induction hx (λ x hx, ⟨_, λ y hy, _, list.prod_singleton⟩)
+      ⟨_, λ y hy, (list.not_mem_nil _ hy).elim, list.prod_nil⟩ _,
+    { rwa list.mem_singleton.1 hy },
+    rintros _ _ ⟨l, hl, rfl⟩ ⟨l', hl', rfl⟩,
+    refine ⟨_, λ y hy, _, list.prod_append⟩,
+    cases list.mem_append.1 hy with hy hy,
+    { exact hl _ hy },
+    { exact hl' _ hy } },
+  apply ((h.partially_well_ordered_on_sublist_forall₂ (≤)).image_of_monotone_on _).mono hl,
+  intros l1 l2 hl1 hl2 h12,
+  obtain ⟨l, hll1, hll2⟩ := list.sublist_forall₂_iff.1 h12,
+  refine le_trans (list.rel_prod (le_refl 1) (λ a b ab c d cd, mul_le_mul' ab cd) hll1) _,
+  obtain ⟨l', hl'⟩ := hll2.exists_perm_append,
+  rw [hl'.prod_eq, list.prod_append, ← mul_one l.prod, mul_assoc, one_mul],
+  apply mul_le_mul_left',
+  have hl's := λ x hx, hl2 x (list.subset.trans (l.subset_append_right _) hl'.symm.subset hx),
+  clear hl',
+  induction l' with x1 x2 x3 x4 x5,
+  { refl },
+  rw [list.prod_cons, ← one_mul (1 : α)],
+  exact mul_le_mul' (hpos x1 (hl's x1 (list.mem_cons_self x1 x2)))
+    (x3 (λ x hx, hl's x (list.mem_cons_of_mem _ hx)))
+end
+
+end is_pwo
+
 /-- `set.mul_antidiagonal s t a` is the set of all pairs of an element in `s` and an element in `t`
   that multiply to `a`. -/
 @[to_additive "`set.add_antidiagonal s t a` is the set of all pairs of an element in `s`

src/ring_theory/hahn_series.lean

@@ -762,7 +762,7 @@ end algebra
 
 section valuation
 
-variables [linear_ordered_add_comm_group Γ] [integral_domain R] [nontrivial R]
+variables [linear_ordered_add_comm_group Γ] [integral_domain R]
 
 instance : linear_ordered_comm_group (multiplicative Γ) :=
 { .. (infer_instance : linear_order (multiplicative Γ)),
@@ -822,6 +822,24 @@ end
 
 end valuation
 
+lemma is_pwo_Union_support_powers [linear_ordered_add_comm_group Γ] [integral_domain R]
+  {x : hahn_series Γ R} (hx : 0 < add_val Γ R x) :
+  (⋃ n : ℕ, (x ^ n).support).is_pwo :=
+begin
+  apply (x.is_wf_support.is_pwo.add_submonoid_closure (λ g hg, _)).mono _,
+  { exact with_top.coe_le_coe.1 (le_trans (le_of_lt hx) (add_val_le_of_coeff_ne_zero hg)) },
+  refine set.Union_subset (λ n, _),
+  induction n with n ih;
+  intros g hn,
+  { simp only [exists_prop, and_true, set.mem_singleton_iff, set.set_of_eq_eq_singleton,
+      mem_support, ite_eq_right_iff, ne.def, not_false_iff, one_ne_zero,
+      pow_zero, not_forall, one_coeff] at hn,
+    rw [hn, set_like.mem_coe],
+    exact add_submonoid.zero_mem _ },
+  { obtain ⟨i, j, hi, hj, rfl⟩ := support_mul_subset_add_support hn,
+    exact set_like.mem_coe.2 (add_submonoid.add_mem _ (add_submonoid.subset_closure hi) (ih hj)) }
+end
+
 section
 variables (Γ) (R) [partial_order Γ] [add_comm_monoid R]
 
@@ -1129,6 +1147,133 @@ end
 
 end emb_domain
 
+section powers
+
+variables [linear_ordered_add_comm_group Γ] [integral_domain R]
+
+/-- The powers of an element of positive valuation form a summable family. -/
+def powers (x : hahn_series Γ R) (hx : 0 < add_val Γ R x) :
+  summable_family Γ R ℕ :=
+{ to_fun := λ n, x ^ n,
+  is_pwo_Union_support' := is_pwo_Union_support_powers hx,
+  finite_co_support' := λ g, begin
+    have hpwo := (is_pwo_Union_support_powers hx),
+    by_cases hg : g ∈ ⋃ n : ℕ, {g | (x ^ n).coeff g ≠ 0 },
+    swap, { exact set.finite_empty.subset (λ n hn, hg (set.mem_Union.2 ⟨n, hn⟩)) },
+    apply hpwo.is_wf.induction hg,
+    intros y ys hy,
+    refine ((((add_antidiagonal x.is_pwo_support hpwo y).finite_to_set.bUnion (λ ij hij,
+      hy ij.snd _ _)).image nat.succ).union (set.finite_singleton 0)).subset _,
+    { exact (mem_add_antidiagonal.1 (mem_coe.1 hij)).2.2 },
+    { obtain ⟨rfl, hi, hj⟩ := mem_add_antidiagonal.1 (mem_coe.1 hij),
+      rw [← zero_add ij.snd, ← add_assoc, add_zero],
+      exact add_lt_add_right (with_top.coe_lt_coe.1
+        (lt_of_lt_of_le hx (add_val_le_of_coeff_ne_zero hi))) _, },
+    { intros n hn,
+      cases n,
+      { exact set.mem_union_right _ (set.mem_singleton 0) },
+      { obtain ⟨i, j, hi, hj, rfl⟩ := support_mul_subset_add_support hn,
+        refine set.mem_union_left _ ⟨n, set.mem_Union.2 ⟨⟨i, j⟩, set.mem_Union.2 ⟨_, hj⟩⟩, rfl⟩,
+        simp only [true_and, set.mem_Union, mem_add_antidiagonal, mem_coe, eq_self_iff_true,
+          ne.def, mem_support, set.mem_set_of_eq],
+        exact ⟨hi, ⟨n, hj⟩⟩ } }
+  end }
+
+variables {x : hahn_series Γ R} (hx : 0 < add_val Γ R x)
+
+@[simp] lemma coe_powers : ⇑(powers x hx) = pow x := rfl
+
+lemma emb_domain_succ_smul_powers :
+  (x • powers x hx).emb_domain ⟨nat.succ, nat.succ_injective⟩ =
+    powers x hx - of_finsupp (finsupp.single 0 1) :=
+begin
+  apply summable_family.ext (λ n, _),
+  cases n,
+  { rw [emb_domain_notin_range, sub_apply, coe_powers, pow_zero, coe_of_finsupp,
+      finsupp.single_eq_same, sub_self],
+    rw [set.mem_range, not_exists],
+    exact nat.succ_ne_zero },
+  { refine eq.trans (emb_domain_image _ ⟨nat.succ, nat.succ_injective⟩) _,
+    simp only [pow_succ, coe_powers, coe_sub, smul_apply, coe_of_finsupp, pi.sub_apply],
+    rw [finsupp.single_eq_of_ne (n.succ_ne_zero).symm, sub_zero] }
+end
+
+lemma one_sub_self_mul_hsum_powers :
+  (1 - x) * (powers x hx).hsum = 1 :=
+begin
+  rw [← hsum_smul, sub_smul, one_smul, hsum_sub,
+    ← hsum_emb_domain (x • powers x hx) ⟨nat.succ, nat.succ_injective⟩,
+    emb_domain_succ_smul_powers],
+  simp,
+end
+
+end powers
+
 end summable_family
 
+section inversion
+
+variables [linear_ordered_add_comm_group Γ]
+
+section integral_domain
+variable [integral_domain R]
+
+lemma unit_aux (x : hahn_series Γ R) {r : R} (hr : r * x.coeff x.order = 1) :
+  0 < add_val Γ R (1 - C r * (single (- x.order) 1) * x) :=
+begin
+  have h10 : (1 : R) ≠ 0 := one_ne_zero,
+  have x0 : x ≠ 0 := ne_zero_of_coeff_ne_zero (right_ne_zero_of_mul_eq_one hr),
+  refine lt_of_le_of_ne ((add_val Γ R).map_le_sub (ge_of_eq (add_val Γ R).map_one) _) _,
+  { simp only [add_valuation.map_mul],
+    rw [add_val_apply_of_ne x0, add_val_apply_of_ne (single_ne_zero h10),
+      add_val_apply_of_ne _, order_C, order_single h10, with_top.coe_zero, zero_add,
+      ← with_top.coe_add, neg_add_self, with_top.coe_zero],
+    { exact le_refl 0 },
+    { exact C_ne_zero (left_ne_zero_of_mul_eq_one hr) } },
+  { rw [add_val_apply, ← with_top.coe_zero],
+    split_ifs,
+    { apply with_top.coe_ne_top },
+    rw [ne.def, with_top.coe_eq_coe],
+    intro con,
+    apply coeff_order_ne_zero h,
+    rw [← con, mul_assoc, sub_coeff, one_coeff, if_pos rfl, C_mul_eq_smul, smul_coeff, smul_eq_mul,
+      ← add_neg_self x.order, single_mul_coeff_add, one_mul, hr, sub_self] }
+end
+
+lemma is_unit_iff {x : hahn_series Γ R} :
+  is_unit x ↔ is_unit (x.coeff x.order) :=
+begin
+  split,
+  { rintro ⟨⟨u, i, ui, iu⟩, rfl⟩,
+    refine is_unit_of_mul_eq_one (u.coeff u.order) (i.coeff i.order)
+      ((mul_coeff_order_add_order (left_ne_zero_of_mul_eq_one ui)
+      (right_ne_zero_of_mul_eq_one ui)).symm.trans _),
+    rw [ui, one_coeff, if_pos],
+    rw [← order_mul (left_ne_zero_of_mul_eq_one ui)
+      (right_ne_zero_of_mul_eq_one ui), ui, order_one] },
+  { rintro ⟨⟨u, i, ui, iu⟩, h⟩,
+    rw [units.coe_mk] at h,
+    rw h at iu,
+    have h := summable_family.one_sub_self_mul_hsum_powers (unit_aux x iu),
+    rw [sub_sub_cancel] at h,
+    exact is_unit_of_mul_is_unit_right (is_unit_of_mul_eq_one _ _ h) },
+end
+
+end integral_domain
+
+instance [field R] : field (hahn_series Γ R) :=
+{ inv := λ x, if x0 : x = 0 then 0 else (C (x.coeff x.order)⁻¹ * (single (-x.order)) 1 *
+      (summable_family.powers _ (unit_aux x (inv_mul_cancel (coeff_order_ne_zero x0)))).hsum),
+  inv_zero := dif_pos rfl,
+  mul_inv_cancel := λ x x0, begin
+    refine (congr rfl (dif_neg x0)).trans _,
+    have h := summable_family.one_sub_self_mul_hsum_powers
+      (unit_aux x (inv_mul_cancel (coeff_order_ne_zero x0))),
+    rw [sub_sub_cancel] at h,
+    rw [← mul_assoc, mul_comm x, h],
+  end,
+  .. hahn_series.integral_domain }
+
+end inversion
+
 end hahn_series