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. We also build the subgroups, subrings, etc. of Hahn series bounded by 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

@[simp]

theorem HahnSeries.cardSupp_one_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] [One R] : cardSupp 1 ≤ 1

@[simp]

theorem HahnSeries.cardSupp_one {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] [One R] [NeZero 1] : cardSupp 1 = 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

theorem HahnSeries.cardSupp_single_mul_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R) : ((single a) r * x).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_mul_single_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R) : (x * (single a) r).cardSupp ≤ x.cardSupp

theorem HahnSeries.cardSupp_pow_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (x : HahnSeries Γ R) (n : ℕ) : (x ^ n).cardSupp ≤ x.cardSupp ^ n

theorem HahnSeries.cardSupp_hsum_le {Γ : Type u_1} {R : Type u_2} {α : Type u_4} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) : Cardinal.lift.{u_4, u_1} s.hsum.cardSupp ≤ Cardinal.sum fun (a : α) => (s a).cardSupp

theorem HahnSeries.cardSupp_hsum_powers_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) : (SummableFamily.powers x).hsum.cardSupp ≤ max Cardinal.aleph0 x.cardSupp

theorem HahnSeries.cardSupp_inv_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x : HahnSeries Γ R) : x⁻¹.cardSupp ≤ max Cardinal.aleph0 x.cardSupp

theorem HahnSeries.cardSupp_div_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x y : HahnSeries Γ R) : (x / y).cardSupp ≤ x.cardSupp * max Cardinal.aleph0 y.cardSupp

Substructures

def HahnSeries.cardSuppLTAddSubmonoid (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] : AddSubmonoid (HahnSeries Γ R)

The κ-bounded submonoid of Hahn series with less than κ terms.

Equations

• HahnSeries.cardSuppLTAddSubmonoid Γ R κ = { carrier := {x : HahnSeries Γ R | x.cardSupp < κ}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem HahnSeries.coe_cardSuppLTAddSubmonoid (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] : ↑(cardSuppLTAddSubmonoid Γ R κ) = {x : HahnSeries Γ R | x.cardSupp < κ}

@[simp]

theorem HahnSeries.mem_cardSuppLTAddSubmonoid {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} : x ∈ cardSuppLTAddSubmonoid Γ R κ ↔ x.cardSupp < κ

def HahnSeries.cardSuppLTAddSubgroup (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] : AddSubgroup (HahnSeries Γ R)

The κ-bounded subgroup of Hahn series with less than κ terms.

Equations

• HahnSeries.cardSuppLTAddSubgroup Γ R κ = { toAddSubmonoid := HahnSeries.cardSuppLTAddSubmonoid Γ R κ, neg_mem' := ⋯ }

@[simp]

theorem HahnSeries.coe_cardSuppLTAddSubgroup (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] : ↑(cardSuppLTAddSubgroup Γ R κ) = {x : HahnSeries Γ R | x.cardSupp < κ}

@[simp]

theorem HahnSeries.mem_cardSuppLTAddSubgroup {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} : x ∈ cardSuppLTAddSubgroup Γ R κ ↔ x.cardSupp < κ

def HahnSeries.cardSuppLTSubring (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] : Subring (HahnSeries Γ R)

The κ-bounded subring of Hahn series with less than κ terms.

Equations

• HahnSeries.cardSuppLTSubring Γ R κ = { carrier := (HahnSeries.cardSuppLTAddSubgroup Γ R κ).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem HahnSeries.mem_cardSuppLTSubring {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} : x ∈ cardSuppLTSubring Γ R κ ↔ x.cardSupp < κ

def HahnSeries.cardSuppLTSubfield (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] : Subfield (HahnSeries Γ R)

The κ-bounded subfield of Hahn series with less than κ terms.

Equations

• HahnSeries.cardSuppLTSubfield Γ R κ = { toSubring := have this := ⋯; HahnSeries.cardSuppLTSubring Γ R κ, inv_mem' := ⋯ }

@[simp]

theorem HahnSeries.cardSuppLTSubfield_carrier (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] : ↑(cardSuppLTSubfield Γ R κ) = (cardSuppLTAddSubgroup Γ R κ).carrier

@[simp]

theorem HahnSeries.mem_cardSuppLTSubfield {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] {x : HahnSeries Γ R} : x ∈ cardSuppLTSubfield Γ R κ ↔ x.cardSupp < κ