[Merged by Bors] - feat: cardinality of Hahn series

Mathlib.lean

@@ -5925,6 +5925,7 @@ public import Mathlib.RingTheory.Grassmannian
 public import Mathlib.RingTheory.HahnSeries.Addition
 public import Mathlib.RingTheory.HahnSeries.Basic
 public import Mathlib.RingTheory.HahnSeries.Binomial
+public import Mathlib.RingTheory.HahnSeries.Cardinal
 public import Mathlib.RingTheory.HahnSeries.HEval
 public import Mathlib.RingTheory.HahnSeries.HahnEmbedding
 public import Mathlib.RingTheory.HahnSeries.Lex

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -46,7 +46,10 @@ variable [PartialOrder Γ] {V : Type*} [Zero V] [SMulZeroClass R V]
 instance : SMul R (HahnSeries Γ V) :=
   ⟨fun r x =>
     { coeff := r • x.coeff
-      isPWO_support' := x.isPWO_support.mono (Function.support_const_smul_subset r x.coeff) }⟩
+      isPWO_support' := x.isPWO_support.mono (Function.support_const_smul_subset ..) }⟩
+
+theorem support_smul_subset (r : R) (x : HahnSeries Γ V) : (r • x).support ⊆ x.support :=
+  Function.support_const_smul_subset ..
 
 @[simp]
 theorem coeff_smul' (r : R) (x : HahnSeries Γ V) : (r • x).coeff = r • x.coeff :=
@@ -69,8 +72,7 @@ theorem orderTop_smul_not_lt (r : R) (x : HahnSeries Γ V) : ¬ (r • x).orderT
     exact not_top_lt
   · simp only [orderTop_of_ne_zero hrx, orderTop_of_ne_zero <| right_ne_zero_of_smul hrx,
       WithTop.coe_lt_coe]
-    exact Set.IsWF.min_of_subset_not_lt_min
-      (Function.support_smul_subset_right (fun _ => r) x.coeff)
+    exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)
 
 theorem orderTop_le_orderTop_smul {Γ} [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) :
     x.orderTop ≤ (r • x).orderTop :=
@@ -80,7 +82,7 @@ theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x 
     ¬ (r • x).order < x.order := by
   have hx : x ≠ 0 := right_ne_zero_of_smul h
   simp_all only [order, dite_false]
-  exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)
+  exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)
 
 theorem le_order_smul {Γ} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
     x.order ≤ (r • x).order :=
@@ -102,7 +104,10 @@ variable [AddMonoid R]
 instance : Add (HahnSeries Γ R) where
   add x y :=
     { coeff := x.coeff + y.coeff
-      isPWO_support' := (x.isPWO_support.union y.isPWO_support).mono (Function.support_add _ _) }
+      isPWO_support' := (x.isPWO_support.union y.isPWO_support).mono (Function.support_add ..) }
+
+theorem support_add_subset (x y : HahnSeries Γ R) : (x + y).support ⊆ x.support ∪ y.support :=
+  Function.support_add ..
 
 @[simp]
 theorem coeff_add' (x y : HahnSeries Γ R) : (x + y).coeff = x.coeff + y.coeff :=
@@ -185,13 +190,6 @@ lemma addOppositeEquiv_symm_leadingCoeff (x : (HahnSeries Γ R)ᵃᵒᵖ) :
   apply AddOpposite.unop_injective
   rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
 
-theorem support_add_subset {x y : HahnSeries Γ R} : support (x + y) ⊆ support x ∪ support y :=
-  fun a ha => by
-  rw [mem_support, coeff_add] at ha
-  rw [Set.mem_union, mem_support, mem_support]
-  contrapose! ha
-  rw [ha.1, ha.2, add_zero]
-
 protected theorem min_le_min_add {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hx : x ≠ 0)
     (hy : y ≠ 0) (hxy : x + y ≠ 0) :
     min (Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx))
@@ -333,16 +331,15 @@ theorem coeff_sum {s : Finset α} {x : α → HahnSeries Γ R} (g : Γ) :
 
 end AddCommMonoid
 
-section AddGroup
+section NegZeroClass
 
-variable [AddGroup R]
+variable [NegZeroClass R]
 
 instance : Neg (HahnSeries Γ R) where
-  neg x :=
-    { coeff := fun a => -x.coeff a
-      isPWO_support' := by
-        rw [Function.support_fun_neg]
-        exact x.isPWO_support }
+  neg x := x.map (-ZeroHom.id _)
+
+theorem support_neg_subset (x : HahnSeries Γ R) : (-x).support ⊆ x.support :=
+  support_map_subset ..
 
 @[simp]
 theorem coeff_neg' (x : HahnSeries Γ R) : (-x).coeff = -x.coeff :=
@@ -351,10 +348,19 @@ theorem coeff_neg' (x : HahnSeries Γ R) : (-x).coeff = -x.coeff :=
 theorem coeff_neg {x : HahnSeries Γ R} {a : Γ} : (-x).coeff a = -x.coeff a :=
   rfl
 
+end NegZeroClass
+
+section AddGroup
+
+variable [AddGroup R]
+
 instance : Sub (HahnSeries Γ R) where
   sub x y :=
     { coeff := x.coeff - y.coeff
-      isPWO_support' := (x.isPWO_support.union y.isPWO_support).mono (Function.support_sub _ _) }
+      isPWO_support' := (x.isPWO_support.union y.isPWO_support).mono (Function.support_sub ..) }
+
+theorem support_sub_subset (x y : HahnSeries Γ R) : (x - y).support ⊆ x.support ∪ y.support :=
+  Function.support_sub ..
 
 @[simp]
 theorem coeff_sub' (x y : HahnSeries Γ R) : (x - y).coeff = x.coeff - y.coeff :=
@@ -365,7 +371,7 @@ theorem coeff_sub {x y : HahnSeries Γ R} {a : Γ} : (x - y).coeff a = x.coeff a
 
 instance : AddGroup (HahnSeries Γ R) := fast_instance%
   coeff_injective.addGroup _
-    coeff_zero' coeff_add' (coeff_neg') (coeff_sub')
+    coeff_zero' coeff_add' coeff_neg' coeff_sub'
     (fun _ _ => coeff_smul' _ _) (fun _ _ => coeff_smul' _ _)
 
 @[simp]
@@ -383,7 +389,7 @@ theorem support_neg {x : HahnSeries Γ R} : (-x).support = x.support := by
 
 @[simp]
 protected lemma map_neg [AddGroup S] (f : R →+ S) {x : HahnSeries Γ R} :
-    ((-x).map f : HahnSeries Γ S) = -(x.map f) := by
+    ((-x).map f : HahnSeries Γ S) = -x.map f := by
   ext; simp
 
 @[simp]

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -71,6 +71,10 @@ theorem coeff_inj {x y : HahnSeries Γ R} : x.coeff = y.coeff ↔ x = y :=
 nonrec def support (x : HahnSeries Γ R) : Set Γ :=
   support x.coeff
 
+@[simp]
+theorem support_mk (f : Γ → R) (h) : support ⟨f, h⟩ = Function.support f :=
+  rfl
+
 @[simp]
 theorem isPWO_support (x : HahnSeries Γ R) : x.support.IsPWO :=
   x.isPWO_support'
@@ -81,7 +85,7 @@ theorem isWF_support (x : HahnSeries Γ R) : x.support.IsWF :=
 
 @[simp]
 theorem mem_support (x : HahnSeries Γ R) (a : Γ) : a ∈ x.support ↔ x.coeff a ≠ 0 :=
-  Iff.refl _
+  .rfl
 
 instance : Zero (HahnSeries Γ R) :=
   ⟨{  coeff := 0
@@ -131,6 +135,10 @@ protected lemma map_zero [Zero S] (f : ZeroHom R S) :
     (0 : HahnSeries Γ R).map f = 0 := by
   ext; simp
 
+theorem support_map_subset [Zero S] (x : HahnSeries Γ R) (f : ZeroHom R S) :
+    (x.map f).support ⊆ x.support :=
+  Function.support_comp_subset (ZeroHomClass.map_zero f) _
+
 /-- Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product. -/
 def ofIterate [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) :
     HahnSeries (Γ ×ₗ Γ') R where
@@ -568,10 +576,19 @@ def truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) :
       isPWO_support' := Set.IsPWO.mono x.isPWO_support (by simp) }
   map_zero' := by ext; simp
 
+theorem support_truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : HahnSeries Γ R) :
+    (truncLT c x).support = {y ∈ x.support | y < c} := by
+  simp [truncLT, Function.support, and_comm]
+
+theorem support_truncLT_subset [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : HahnSeries Γ R) :
+    (truncLT c x).support ⊆ x.support := by
+  rw [support_truncLT]
+  exact Set.sep_subset ..
+
 @[simp]
 protected theorem coeff_truncLT [PartialOrder Γ] [DecidableLT Γ]
     (c : Γ) (x : HahnSeries Γ R) (i : Γ) :
-    (truncLT c x).coeff i = if i < c then x.coeff i else 0  := rfl
+    (truncLT c x).coeff i = if i < c then x.coeff i else 0 := rfl
 
 theorem coeff_truncLT_of_lt [PartialOrder Γ] [DecidableLT Γ]
     {c i : Γ} (h : i < c) (x : HahnSeries Γ R) : (truncLT c x).coeff i = x.coeff i := by

Mathlib/RingTheory/HahnSeries/Cardinal.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2025 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import Mathlib.Algebra.Group.Pointwise.Set.Card
+public import Mathlib.RingTheory.HahnSeries.Multiplication
+
+/-!
+# Cardinality of Hahn series
+
+We define `HahnSeries.card` as the cardinality of the support of a Hahn series, and find bounds for
+the cardinalities of different operations.
+
+## Todo
+
+- Bound the cardinality of the inverse.
+- Build the subgroups, subrings, etc. of Hahn series with less than a given infinite cardinal.
+-/
+
+@[expose] public section
+
+open Cardinal
+
+namespace HahnSeries
+
+variable {Γ R S : Type*} [PartialOrder Γ]
+
+/-! ### Cardinality function -/
+
+section Zero
+variable [Zero R]
+
+/-- The cardinality of the support of a Hahn series. -/
+def card (x : HahnSeries Γ R) : Cardinal :=
+  #x.support
+
+theorem card_congr [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support = y.support) :
+    x.card = y.card := by
+  simp_rw [card, h]
+
+theorem card_mono [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support ⊆ y.support) :
+    x.card ≤ y.card :=
+  mk_le_mk_of_subset h
+
+@[simp]
+theorem card_zero : card (0 : HahnSeries Γ R) = 0 := by
+  simp [card]
+
+theorem card_single_of_ne (a : Γ) {r : R} (h : r ≠ 0) : card (single a r) = 1 := by
+  rw [card, support_single_of_ne h, mk_singleton]
+
+theorem card_single_le (a : Γ) (r : R) : card (single a r) ≤ 1 :=
+  (mk_le_mk_of_subset support_single_subset).trans_eq (mk_singleton a)
+
+theorem card_map_le [Zero S] (x : HahnSeries Γ R) (f : ZeroHom R S) : (x.map f).card ≤ x.card :=
+  card_mono <| support_map_subset ..
+
+theorem card_truncLT_le [DecidableLT Γ] (x : HahnSeries Γ R) (c : Γ) :
+    (truncLT c x).card ≤ x.card :=
+  card_mono <| support_truncLT_subset ..
+
+theorem card_smul_le (s : S) (x : HahnSeries Γ R) [SMulZeroClass S R] : (s • x).card ≤ x.card :=
+  card_mono <| support_smul_subset ..
+
+end Zero
+
+theorem card_neg_le [NegZeroClass R] (x : HahnSeries Γ R) : (-x).card ≤ x.card :=
+  card_mono <| support_neg_subset ..
+
+theorem card_add_le [AddMonoid R] (x y : HahnSeries Γ R) : (x + y).card ≤ x.card + y.card :=
+  (mk_le_mk_of_subset (support_add_subset ..)).trans (mk_union_le ..)
+
+@[simp]
+theorem card_neg [AddGroup R] (x : HahnSeries Γ R) : (-x).card = x.card :=
+  card_congr support_neg
+
+theorem card_sub_le [AddGroup R] (x y : HahnSeries Γ R) : (x - y).card ≤ x.card + y.card :=
+  (mk_le_mk_of_subset (support_sub_subset ..)).trans (mk_union_le ..)
+
+theorem card_mul_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R]
+    (x y : HahnSeries Γ R) : (x * y).card ≤ x.card * y.card :=
+  (mk_le_mk_of_subset (support_mul_subset ..)).trans mk_add_le
+
+end HahnSeries

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -492,11 +492,14 @@ theorem single_zero_mul_eq_smul [Semiring R] {r : R} {x : HahnSeries Γ R} :
   ext
   exact coeff_single_zero_mul
 
-theorem support_mul_subset_add_support [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
+theorem support_mul_subset [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
     support (x * y) ⊆ support x + support y := by
   rw [← of_symm_smul_of_eq_mul, ← vadd_eq_add]
   exact HahnModule.support_smul_subset_vadd_support
 
+@[deprecated (since := "2025-12-09")]
+alias support_mul_subset_add_support := support_mul_subset
+
 instance [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R) :=
   { inferInstanceAs (AddCommMonoid (HahnSeries Γ R)),
     inferInstanceAs (Distrib (HahnSeries Γ R)) with
@@ -530,7 +533,7 @@ theorem orderTop_mul_of_nonzero {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.
   refine le_antisymm (order_le_of_coeff_ne_zero this) ?_
   rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, HahnSeries.order_of_ne hxy,
     ← Set.IsWF.min_add]
-  exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
+  exact Set.IsWF.min_le_min_of_subset support_mul_subset
 
 theorem orderTop_add_le_mul {x y : HahnSeries Γ R} :
     x.orderTop + y.orderTop ≤ (x * y).orderTop := by
@@ -547,7 +550,7 @@ theorem order_mul_of_nonzero {x y : HahnSeries Γ R}
     (Eq.mpr (congrArg (fun _a ↦ _a ≠ 0) (coeff_mul_order_add_order x y)) h)) ?_
   rw [order_of_ne <| leadingCoeff_ne_zero.mp hx, order_of_ne <| leadingCoeff_ne_zero.mp hy,
     order_of_ne <| ne_zero_of_coeff_ne_zero hxy, ← Set.IsWF.min_add]
-  exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
+  exact Set.IsWF.min_le_min_of_subset support_mul_subset
 
 theorem leadingCoeff_mul_of_nonzero {x y : HahnSeries Γ R}
     (h : x.leadingCoeff * y.leadingCoeff ≠ 0) :
@@ -571,8 +574,8 @@ variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
 private theorem mul_assoc' [NonUnitalSemiring R] (x y z : HahnSeries Γ R) :
     x * y * z = x * (y * z) := by
   ext b
-  rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset_add_support,
-    coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset_add_support]
+  rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset,
+    coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset]
   simp only [coeff_mul, sum_mul, mul_sum, sum_sigma']
   apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
     (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
@@ -718,7 +721,7 @@ private theorem mul_smul' [Semiring R] [Module R V] (x y : HahnSeries Γ R)
     (z : HahnModule Γ' R V) : (x * y) • z = x • (y • z) := by
   ext b
   rw [coeff_smul_left (x.isPWO_support.add y.isPWO_support)
-    HahnSeries.support_mul_subset_add_support, coeff_smul_right
+    HahnSeries.support_mul_subset, coeff_smul_right
     (y.isPWO_support.vadd ((of R).symm z).isPWO_support) support_smul_subset_vadd_support]
   simp only [HahnSeries.coeff_mul, coeff_smul, sum_smul, smul_sum, sum_sigma']
   apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l +ᵥ j), (l, j)⟩)
@@ -793,7 +796,7 @@ theorem order_mul {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMo
     rw [coeff_mul_order_add_order x y]
     exact mul_ne_zero (leadingCoeff_ne_zero.mpr hx) (leadingCoeff_ne_zero.mpr hy)
   · rw [order_of_ne hx, order_of_ne hy, order_of_ne (mul_ne_zero hx hy), ← Set.IsWF.min_add]
-    exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
+    exact Set.IsWF.min_le_min_of_subset support_mul_subset
 
 @[simp]
 theorem order_pow {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ]
@@ -921,7 +924,7 @@ theorem embDomain_mul [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ')
       exact ⟨i, j, h1, rfl⟩
   · rw [embDomain_notin_range hg, eq_comm]
     contrapose! hg
-    obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset_add_support ((mem_support _ _).2 hg)
+    obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset ((mem_support _ _).2 hg)
     obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi
     obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj
     exact ⟨i + j, hf i j⟩

Mathlib/RingTheory/HahnSeries/Summable.lean

@@ -107,7 +107,7 @@ instance : Add (SummableFamily Γ R α) :=
         (x.isPWO_iUnion_support.union y.isPWO_iUnion_support).mono
           (by
             rw [← Set.iUnion_union_distrib]
-            exact Set.iUnion_mono fun a => support_add_subset)
+            exact Set.iUnion_mono fun a => support_add_subset ..)
       finite_co_support' := fun g =>
         ((x.finite_co_support g).union (y.finite_co_support g)).subset
           (by
@@ -657,7 +657,7 @@ theorem support_pow_subset_closure [AddCommMonoid Γ] [PartialOrder Γ] [IsOrder
     simp only [hn, SetLike.mem_coe]
     exact AddSubmonoid.zero_mem _
   | succ n ih =>
-    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset_add_support hn
+    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
     exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))
 
 theorem isPWO_iUnion_support_powers [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ]
@@ -695,7 +695,7 @@ theorem pow_finite_co_support {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : 
       order_le_of_coeff_ne_zero <| Function.mem_support.mp hi
   · rintro (_ | n) hn
     · exact Set.mem_union_right _ (Set.mem_singleton 0)
-    · obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset_add_support hn
+    · obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
       refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩
       simp only [mem_coe, mem_addAntidiagonal, mem_support, ne_eq, Set.mem_iUnion]
       exact ⟨hj, ⟨n, hi⟩, add_comm j i⟩