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

Mathlib.lean

@@ -5899,6 +5899,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 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 : V⟦Γ⟧) : (r • x).coeff = r • x.coeff :=
@@ -67,8 +70,7 @@ theorem orderTop_smul_not_lt (r : R) (x : V⟦Γ⟧) : ¬ (r • x).orderTop < x
     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 : V⟦Γ⟧) :
     x.orderTop ≤ (r • x).orderTop :=
@@ -78,7 +80,7 @@ theorem order_smul_not_lt [Zero Γ] (r : R) (x : V⟦Γ⟧) (h : r • x ≠ 0)
     ¬ (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 : V⟦Γ⟧) (h : r • x ≠ 0) :
     x.order ≤ (r • x).order :=
@@ -100,7 +102,10 @@ variable [AddMonoid R]
 instance : Add 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 : R⟦Γ⟧) : (x + y).support ⊆ x.support ∪ y.support :=
+  Function.support_add ..
 
 @[simp]
 theorem coeff_add' (x y : R⟦Γ⟧) : (x + y).coeff = x.coeff + y.coeff :=
@@ -183,13 +188,6 @@ lemma addOppositeEquiv_symm_leadingCoeff (x : R⟦Γ⟧ᵃᵒᵖ) :
   apply AddOpposite.unop_injective
   rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
 
-theorem support_add_subset {x y : 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 : R⟦Γ⟧} (hx : x ≠ 0)
     (hy : y ≠ 0) (hxy : x + y ≠ 0) :
     min (Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx))
@@ -330,16 +328,15 @@ theorem coeff_sum {s : Finset α} {x : α → R⟦Γ⟧} (g : Γ) :
 
 end AddCommMonoid
 
-section AddGroup
+section NegZeroClass
 
-variable [AddGroup R]
+variable [NegZeroClass R]
 
 instance : Neg 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 : R⟦Γ⟧) : (-x).support ⊆ x.support :=
+  support_map_subset ..
 
 @[simp]
 theorem coeff_neg' (x : R⟦Γ⟧) : (-x).coeff = -x.coeff :=
@@ -348,10 +345,19 @@ theorem coeff_neg' (x : R⟦Γ⟧) : (-x).coeff = -x.coeff :=
 theorem coeff_neg {x : R⟦Γ⟧} {a : Γ} : (-x).coeff a = -x.coeff a :=
   rfl
 
+end NegZeroClass
+
+section AddGroup
+
+variable [AddGroup R]
+
 instance : Sub 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 : R⟦Γ⟧) : (x - y).support ⊆ x.support ∪ y.support :=
+  Function.support_sub ..
 
 @[simp]
 theorem coeff_sub' (x y : R⟦Γ⟧) : (x - y).coeff = x.coeff - y.coeff :=
@@ -362,7 +368,7 @@ theorem coeff_sub {x y : R⟦Γ⟧} {a : Γ} : (x - y).coeff a = x.coeff a - y.c
 
 instance : AddGroup 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]
@@ -380,7 +386,7 @@ theorem support_neg {x : R⟦Γ⟧} : (-x).support = x.support := by
 
 @[simp]
 protected lemma map_neg [AddGroup S] (f : R →+ S) {x : R⟦Γ⟧} :
-    ((-x).map f : S⟦Γ⟧) = -(x.map f) := by
+    ((-x).map f : S⟦Γ⟧) = -x.map f := by
   ext; simp
 
 @[simp]

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -86,6 +86,10 @@ theorem coeff_inj {x y : R⟦Γ⟧} : x.coeff = y.coeff ↔ x = y :=
 nonrec def support (x : R⟦Γ⟧) : Set Γ :=
   support x.coeff
 
+@[simp]
+theorem support_mk (f : Γ → R) (h) : support ⟨f, h⟩ = Function.support f :=
+  rfl
+
 @[simp]
 theorem isPWO_support (x : R⟦Γ⟧) : x.support.IsPWO :=
   x.isPWO_support'
@@ -96,7 +100,7 @@ theorem isWF_support (x : R⟦Γ⟧) : x.support.IsWF :=
 
 @[simp]
 theorem mem_support (x : R⟦Γ⟧) (a : Γ) : a ∈ x.support ↔ x.coeff a ≠ 0 :=
-  Iff.refl _
+  .rfl
 
 instance : Zero R⟦Γ⟧ :=
   ⟨{  coeff := 0
@@ -144,6 +148,10 @@ def map [Zero S] (x : R⟦Γ⟧) {F : Type*} [FunLike F R S] [ZeroHomClass F R S
 protected lemma map_zero [Zero S] (f : ZeroHom R S) : (0 : R⟦Γ⟧).map f = 0 := by
   ext; simp
 
+theorem support_map_subset [Zero S] (x : 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 a `HahnSeries` to a `HahnSeries` on a Lex product. -/
 def ofIterate [PartialOrder Γ'] (x : R⟦Γ'⟧⟦Γ⟧) : R⟦Γ ×ₗ Γ'⟧ where
   coeff := fun g => coeff (coeff x g.1) g.2
@@ -576,9 +584,18 @@ def truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) : ZeroHom R⟦Γ⟧ R⟦
       isPWO_support' := Set.IsPWO.mono x.isPWO_support (by simp) }
   map_zero' := by ext; simp
 
+theorem support_truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : 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 : R⟦Γ⟧) :
+    (truncLT c x).support ⊆ x.support := by
+  rw [support_truncLT]
+  exact Set.sep_subset ..
+
 @[simp]
 protected theorem coeff_truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : 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 : R⟦Γ⟧) :
     (truncLT c x).coeff i = x.coeff i := by

Mathlib/RingTheory/HahnSeries/Cardinal.lean

@@ -0,0 +1,88 @@
+/-
+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.cardSupp` 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 support 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 cardSupp (x : R⟦Γ⟧) : Cardinal :=
+  #x.support
+
+theorem cardSupp_congr [Zero S] {x : R⟦Γ⟧} {y : S⟦Γ⟧} (h : x.support = y.support) :
+    x.cardSupp = y.cardSupp := by
+  simp_rw [cardSupp, h]
+
+theorem cardSupp_mono [Zero S] {x : R⟦Γ⟧} {y : S⟦Γ⟧} (h : x.support ⊆ y.support) :
+    x.cardSupp ≤ y.cardSupp :=
+  mk_le_mk_of_subset h
+
+@[simp]
+theorem cardSupp_zero : cardSupp (0 : R⟦Γ⟧) = 0 := by
+  simp [cardSupp]
+
+theorem cardSupp_single_of_ne (a : Γ) {r : R} (h : r ≠ 0) : cardSupp (single a r) = 1 := by
+  rw [cardSupp, support_single_of_ne h, mk_singleton]
+
+theorem cardSupp_single_le (a : Γ) (r : R) : cardSupp (single a r) ≤ 1 :=
+  (mk_le_mk_of_subset support_single_subset).trans_eq (mk_singleton a)
+
+theorem cardSupp_map_le [Zero S] (x : R⟦Γ⟧) (f : ZeroHom R S) : (x.map f).cardSupp ≤ x.cardSupp :=
+  cardSupp_mono <| support_map_subset ..
+
+theorem cardSupp_truncLT_le [DecidableLT Γ] (x : R⟦Γ⟧) (c : Γ) :
+    (truncLT c x).cardSupp ≤ x.cardSupp :=
+  cardSupp_mono <| support_truncLT_subset ..
+
+theorem cardSupp_smul_le (s : S) (x : R⟦Γ⟧) [SMulZeroClass S R] : (s • x).cardSupp ≤ x.cardSupp :=
+  cardSupp_mono <| support_smul_subset ..
+
+end Zero
+
+theorem cardSupp_neg_le [NegZeroClass R] (x : R⟦Γ⟧) : (-x).cardSupp ≤ x.cardSupp :=
+  cardSupp_mono <| support_neg_subset ..
+
+theorem cardSupp_add_le [AddMonoid R] (x y : R⟦Γ⟧) : (x + y).cardSupp ≤ x.cardSupp + y.cardSupp :=
+  (mk_le_mk_of_subset (support_add_subset ..)).trans (mk_union_le ..)
+
+@[simp]
+theorem cardSupp_neg [AddGroup R] (x : R⟦Γ⟧) : (-x).cardSupp = x.cardSupp :=
+  cardSupp_congr support_neg
+
+theorem cardSupp_sub_le [AddGroup R] (x y : R⟦Γ⟧) : (x - y).cardSupp ≤ x.cardSupp + y.cardSupp :=
+  (mk_le_mk_of_subset (support_sub_subset ..)).trans (mk_union_le ..)
+
+theorem cardSupp_mul_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R]
+    (x y : R⟦Γ⟧) : (x * y).cardSupp ≤ x.cardSupp * y.cardSupp :=
+  (mk_le_mk_of_subset (support_mul_subset ..)).trans mk_add_le
+
+end HahnSeries

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -486,11 +486,14 @@ theorem single_zero_mul_eq_smul [Semiring R] {r : R} {x : R⟦Γ⟧} : single 0
   ext
   exact coeff_single_zero_mul
 
-theorem support_mul_subset_add_support [NonUnitalNonAssocSemiring R] {x y : R⟦Γ⟧} :
+theorem support_mul_subset [NonUnitalNonAssocSemiring R] {x y : 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 R⟦Γ⟧ where
   zero_mul _ := by
     ext
@@ -522,7 +525,7 @@ theorem orderTop_mul_of_nonzero {x y : R⟦Γ⟧} (h : x.leadingCoeff * y.leadin
   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 : R⟦Γ⟧} : x.orderTop + y.orderTop ≤ (x * y).orderTop := by
   rw [← smul_eq_mul]
@@ -538,7 +541,7 @@ theorem order_mul_of_nonzero {x y : 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 : R⟦Γ⟧} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) :
     (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff := by
@@ -560,8 +563,8 @@ variable [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
 
 private theorem mul_assoc' [NonUnitalSemiring R] (x y z : 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)⟩) <;>
@@ -681,7 +684,7 @@ private theorem mul_smul' [Semiring R] [Module R V] (x y : 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)⟩)
@@ -756,7 +759,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 Γ]
@@ -884,7 +887,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 : 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⟩