Additive properties of Hahn series

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R. When R has an addition operation, HahnSeries Γ R also has addition by adding coefficients.

Main Definitions

• If R is a (commutative) additive monoid or group, then so is HahnSeries Γ R.

References

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]

instance HahnSeries.instAddHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] : Add (HahnSeries Γ R)

Equations

• HahnSeries.instAddHahnSeriesToZero = { add := fun (x y : HahnSeries Γ R) => { coeff := x.coeff + y.coeff, isPWO_support' := ⋯ } }

instance HahnSeries.instAddMonoidHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] : AddMonoid (HahnSeries Γ R)

Equations

• HahnSeries.instAddMonoidHahnSeriesToZero = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

@[simp]

theorem HahnSeries.add_coeff' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : (x + y).coeff = x.coeff + y.coeff

theorem HahnSeries.add_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : (x + y).coeff a = x.coeff a + y.coeff a

theorem HahnSeries.support_add_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : HahnSeries.support (x + y) ⊆ HahnSeries.support x ∪ HahnSeries.support y

theorem HahnSeries.min_order_le_order_add {R : Type u_2} [AddMonoid R] {Γ : Type u_3} [Zero Γ] [LinearOrder Γ] {x : HahnSeries Γ R} {y : HahnSeries Γ R} (hxy : x + y ≠ 0) : min (HahnSeries.order x) (HahnSeries.order y) ≤ HahnSeries.order (x + y)

@[simp]

theorem HahnSeries.single.addMonoidHom_apply_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (a : Γ) (r : R) (j : Γ) : ((HahnSeries.single.addMonoidHom a) r).coeff j = Pi.single a r j

def HahnSeries.single.addMonoidHom {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (a : Γ) : R →+ HahnSeries Γ R

single as an additive monoid/group homomorphism

Equations

• HahnSeries.single.addMonoidHom a = let __src := HahnSeries.single a; { toZeroHom := __src, map_add' := ⋯ }

@[simp]

theorem HahnSeries.coeff.addMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (g : Γ) (f : HahnSeries Γ R) : (HahnSeries.coeff.addMonoidHom g) f = f.coeff g

def HahnSeries.coeff.addMonoidHom {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (g : Γ) : HahnSeries Γ R →+ R

coeff g as an additive monoid/group homomorphism

Equations

• HahnSeries.coeff.addMonoidHom g = { toZeroHom := { toFun := fun (f : HahnSeries Γ R) => f.coeff g, map_zero' := ⋯ }, map_add' := ⋯ }

theorem HahnSeries.embDomain_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {Γ' : Type u_3} [PartialOrder Γ'] (f : Γ ↪o Γ') (x : HahnSeries Γ R) (y : HahnSeries Γ R) : HahnSeries.embDomain f (x + y) = HahnSeries.embDomain f x + HahnSeries.embDomain f y

instance HahnSeries.instAddCommMonoidHahnSeriesToZeroToAddMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] : AddCommMonoid (HahnSeries Γ R)

Equations

• HahnSeries.instAddCommMonoidHahnSeriesToZeroToAddMonoid = let __src := inferInstanceAs (AddMonoid (HahnSeries Γ R)); AddCommMonoid.mk ⋯

instance HahnSeries.instNegHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] : Neg (HahnSeries Γ R)

Equations

• HahnSeries.instNegHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = { neg := fun (x : HahnSeries Γ R) => { coeff := fun (a : Γ) => -x.coeff a, isPWO_support' := ⋯ } }

instance HahnSeries.instAddGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] : AddGroup (HahnSeries Γ R)

Equations

• HahnSeries.instAddGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = let __src := inferInstanceAs (AddMonoid (HahnSeries Γ R)); AddGroup.mk ⋯

@[simp]

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

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

@[simp]

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

@[simp]

theorem HahnSeries.sub_coeff' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : (x - y).coeff = x.coeff - y.coeff

theorem HahnSeries.sub_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : (x - y).coeff a = x.coeff a - y.coeff a

@[simp]

theorem HahnSeries.order_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] [Zero Γ] {f : HahnSeries Γ R} : HahnSeries.order (-f) = HahnSeries.order f

instance HahnSeries.instAddCommGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] : AddCommGroup (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] : SMul R (HahnSeries Γ V)

Equations

• HahnSeries.instSMulHahnSeriesToZero = { smul := fun (r : R) (x : HahnSeries Γ V) => { coeff := r • x.coeff, isPWO_support' := ⋯ } }

@[simp]

theorem HahnSeries.smul_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {r : R} {x : HahnSeries Γ V} {a : Γ} : (r • x).coeff a = r • x.coeff a

instance HahnSeries.instDistribMulActionHahnSeriesToZeroInstAddMonoidHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] : DistribMulAction R (HahnSeries Γ V)

Equations

• HahnSeries.instDistribMulActionHahnSeriesToZeroInstAddMonoidHahnSeriesToZero = DistribMulAction.mk ⋯ ⋯

theorem HahnSeries.order_smul_not_lt {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) : ¬HahnSeries.order (r • x) < HahnSeries.order x

theorem HahnSeries.le_order_smul {R : Type u_2} {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {Γ : Type u_4} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) : HahnSeries.order x ≤ HahnSeries.order (r • x)

instance HahnSeries.instIsScalarTowerHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_4} [Monoid S] [DistribMulAction S V] [SMul R S] [IsScalarTower R S V] : IsScalarTower R S (HahnSeries Γ V)

Equations

• ⋯ = ⋯

instance HahnSeries.instSMulCommClassHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_4} [Monoid S] [DistribMulAction S V] [SMulCommClass R S V] : SMulCommClass R S (HahnSeries Γ V)

Equations

• ⋯ = ⋯

instance HahnSeries.instModuleHahnSeriesToZeroToAddMonoidInstAddCommMonoidHahnSeriesToZeroToAddMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] : Module R (HahnSeries Γ V)

Equations

• HahnSeries.instModuleHahnSeriesToZeroToAddMonoidInstAddCommMonoidHahnSeriesToZeroToAddMonoid = let __src := inferInstanceAs (DistribMulAction R (HahnSeries Γ V)); Module.mk ⋯ ⋯

@[simp]

theorem HahnSeries.single.linearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (a : Γ) : ∀ (a_1 : V), (HahnSeries.single.linearMap a) a_1 = (HahnSeries.single.addMonoidHom a).toFun a_1

def HahnSeries.single.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (a : Γ) : V →ₗ[R] HahnSeries Γ V

single as a linear map

Equations

• HahnSeries.single.linearMap a = let __src := HahnSeries.single.addMonoidHom a; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem HahnSeries.coeff.linearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (g : Γ) : ∀ (a : HahnSeries Γ V), (HahnSeries.coeff.linearMap g) a = (HahnSeries.coeff.addMonoidHom g).toFun a

def HahnSeries.coeff.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (g : Γ) : HahnSeries Γ V →ₗ[R] V

coeff g as a linear map

Equations

• HahnSeries.coeff.linearMap g = let __src := HahnSeries.coeff.addMonoidHom g; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

theorem HahnSeries.embDomain_smul {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') (r : R) (x : HahnSeries Γ R) : HahnSeries.embDomain f (r • x) = r • HahnSeries.embDomain f x

@[simp]

theorem HahnSeries.embDomainLinearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') : ∀ (a : HahnSeries Γ R), (HahnSeries.embDomainLinearMap f) a = HahnSeries.embDomain f a

def HahnSeries.embDomainLinearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') : HahnSeries Γ R →ₗ[R] HahnSeries Γ' R

Extending the domain of Hahn series is a linear map.

Equations

• HahnSeries.embDomainLinearMap f = { toAddHom := { toFun := HahnSeries.embDomain f, map_add' := ⋯ }, map_smul' := ⋯ }