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.

Cardinality function

def HahnSeries.cardSupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) : Cardinal.{u_1}

The cardinality of the support of a Hahn series.

Equations

• x.cardSupp = Cardinal.mk ↑x.support

theorem HahnSeries.cardSupp_congr {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support = y.support) : x.cardSupp = y.cardSupp

theorem HahnSeries.cardSupp_mono {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support ⊆ y.support) : x.cardSupp ≤ y.cardSupp

@[simp]

theorem HahnSeries.cardSupp_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] : cardSupp 0 = 0

theorem HahnSeries.cardSupp_single_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) {r : R} (h : r ≠ 0) : ((single a) r).cardSupp = 1

theorem HahnSeries.cardSupp_single_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) (r : R) : ((single a) r).cardSupp ≤ 1

theorem HahnSeries.cardSupp_map_le {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) (f : ZeroHom R S) : (x.map f).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_truncLT_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [DecidableLT Γ] (x : HahnSeries Γ R) (c : Γ) : ((truncLT c) x).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_smul_le {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] (s : S) (x : HahnSeries Γ R) [SMulZeroClass S R] : (s • x).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_neg_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [NegZeroClass R] (x : HahnSeries Γ R) : (-x).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_add_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (x y : HahnSeries Γ R) : (x + y).cardSupp ≤ x.cardSupp + y.cardSupp

@[simp]

theorem HahnSeries.cardSupp_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] (x : HahnSeries Γ R) : (-x).cardSupp = x.cardSupp

theorem HahnSeries.cardSupp_sub_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] (x y : HahnSeries Γ R) : (x - y).cardSupp ≤ x.cardSupp + y.cardSupp

theorem HahnSeries.cardSupp_mul_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) : (x * y).cardSupp ≤ x.cardSupp * y.cardSupp