Multiplicative 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. We prove some facts about multiplying Hahn series.

Main Definitions

• HahnModule is a type alias for HahnSeries, which we use for defining scalar multiplication of HahnSeries Γ R on HahnModule Γ V for an R-module V.
• If R is a (commutative) (semi-)ring, then so is HahnSeries Γ R.

References

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

instance HahnSeries.instOneHahnSeriesToPartialOrderToOrderedAddCommMonoid {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Zero R] [One R] : One (HahnSeries Γ R)

Equations

• HahnSeries.instOneHahnSeriesToPartialOrderToOrderedAddCommMonoid = { one := (HahnSeries.single 0) 1 }

@[simp]

theorem HahnSeries.one_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Zero R] [One R] {a : Γ} : 1.coeff a = if a = 0 then 1 else 0

@[simp]

theorem HahnSeries.single_zero_one {R : Type u_2} [Zero R] [One R] : (HahnSeries.single 0) 1 = 1

@[simp]

theorem HahnSeries.support_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [MulZeroOneClass R] [Nontrivial R] : HahnSeries.support 1 = {0}

@[simp]

theorem HahnSeries.order_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [MulZeroOneClass R] : HahnSeries.order 1 = 0

def HahnModule (Γ : Type u_3) (R : Type u_4) (V : Type u_5) [PartialOrder Γ] [Zero V] [SMul R V] : Type (max u_3 u_5)

We introduce a type alias for HahnSeries in order to work with scalar multiplication by series. If we wrote a SMul (HahnSeries Γ R) (HahnSeries Γ V) instance, then when V = HahnSeries Γ R, we would have two different actions of HahnSeries Γ R on HahnSeries Γ V. See Mathlib.Algebra.Polynomial.Module for more discussion on this problem.

Equations

• HahnModule Γ R V = HahnSeries Γ V

def HahnModule.of {Γ : Type u_3} (R : Type u_4) {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] : HahnSeries Γ V ≃ HahnModule Γ R V

The casting function to the type synonym.

Equations

• HahnModule.of R = Equiv.refl (HahnSeries Γ V)

def HahnModule.rec {Γ : Type u_3} {R : Type u_4} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R V → Sort u_6} (h : (x : HahnSeries Γ V) → motive ((HahnModule.of R) x)) (x : HahnModule Γ R V) : motive x

Recursion principle to reduce a result about the synonym to the original type.

Equations

• HahnModule.rec h x = h ((HahnModule.of R).symm x)

theorem HahnModule.ext {Γ : Type u_3} {R : Type u_4} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] (x : HahnModule Γ R V) (y : HahnModule Γ R V) (h : ((HahnModule.of R).symm x).coeff = ((HahnModule.of R).symm y).coeff) : x = y

instance HahnModule.instAddCommMonoid {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] : AddCommMonoid (HahnModule Γ R V)

Equations

• HahnModule.instAddCommMonoid = inferInstanceAs (AddCommMonoid (HahnSeries Γ V))

@[simp]

theorem HahnModule.of_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] : (HahnModule.of R) 0 = 0

@[simp]

theorem HahnModule.of_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] (x : HahnSeries Γ V) (y : HahnSeries Γ V) : (HahnModule.of R) (x + y) = (HahnModule.of R) x + (HahnModule.of R) y

@[simp]

theorem HahnModule.of_symm_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] : (HahnModule.of R).symm 0 = 0

@[simp]

theorem HahnModule.of_symm_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] (x : HahnModule Γ R V) (y : HahnModule Γ R V) : (HahnModule.of R).symm (x + y) = (HahnModule.of R).symm x + (HahnModule.of R).symm y

instance HahnModule.instSMul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V)

Equations

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

theorem HahnModule.smul_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ R V) (a : Γ) : ((HahnModule.of R).symm (x • y)).coeff a = Finset.sum (Finset.addAntidiagonal ⋯ ⋯ a) fun (ij : Γ × Γ) => x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2

instance HahnModule.instSMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {W : Type u_4} [Zero R] [AddCommMonoid W] [SMulZeroClass R W] : SMulZeroClass (HahnSeries Γ R) (HahnModule Γ R W)

Equations

• HahnModule.instSMulZeroClass = SMulZeroClass.mk ⋯

theorem HahnModule.smul_coeff_right {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {W : Type u_4} [Zero R] [AddCommMonoid W] [SMulZeroClass R W] {x : HahnSeries Γ R} {y : HahnModule Γ R W} {a : Γ} {s : Set Γ} (hs : Set.IsPWO s) (hys : HahnSeries.support ((HahnModule.of R).symm y) ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = Finset.sum (Finset.addAntidiagonal ⋯ hs a) fun (ij : Γ × Γ) => x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2

theorem HahnModule.smul_coeff_left {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {W : Type u_4} [Zero R] [AddCommMonoid W] [SMulWithZero R W] {x : HahnSeries Γ R} {y : HahnModule Γ R W} {a : Γ} {s : Set Γ} (hs : Set.IsPWO s) (hxs : HahnSeries.support x ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = Finset.sum (Finset.addAntidiagonal hs ⋯ a) fun (ij : Γ × Γ) => x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2

instance HahnSeries.instMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R)

Equations

• HahnSeries.instMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass = { mul := fun (x y : HahnSeries Γ R) => (HahnModule.of R).symm (x • (HahnModule.of R) y) }

theorem HahnSeries.of_symm_smul_of_eq_mul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : (HahnModule.of R).symm (x • (HahnModule.of R) y) = x * y

theorem HahnSeries.mul_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : (x * y).coeff a = Finset.sum (Finset.addAntidiagonal ⋯ ⋯ a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff ij.2

theorem HahnSeries.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : Set.IsPWO s) (hys : HahnSeries.support y ⊆ s) : (x * y).coeff a = Finset.sum (Finset.addAntidiagonal ⋯ hs a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff ij.2

theorem HahnSeries.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : Set.IsPWO s) (hxs : HahnSeries.support x ⊆ s) : (x * y).coeff a = Finset.sum (Finset.addAntidiagonal hs ⋯ a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff ij.2

instance HahnSeries.instDistribHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : Distrib (HahnSeries Γ R)

Equations

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

theorem HahnSeries.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} : ((HahnSeries.single b) r * x).coeff (a + b) = r * x.coeff a

theorem HahnSeries.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} : (x * (HahnSeries.single b) r).coeff (a + b) = x.coeff a * r

@[simp]

theorem HahnSeries.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : (x * (HahnSeries.single 0) r).coeff a = x.coeff a * r

theorem HahnSeries.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : ((HahnSeries.single 0) r * x).coeff a = r * x.coeff a

@[simp]

theorem HahnSeries.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : (HahnSeries.single 0) r * x = r • x

theorem HahnSeries.support_mul_subset_add_support {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : HahnSeries.support (x * y) ⊆ HahnSeries.support x + HahnSeries.support y

theorem HahnSeries.mul_coeff_order_add_order {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (y : HahnSeries Γ R) : (x * y).coeff (HahnSeries.order x + HahnSeries.order y) = x.coeff (HahnSeries.order x) * y.coeff (HahnSeries.order y)

instance HahnSeries.instNonUnitalNonAssocSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonUnitalSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalSemiring R] : NonUnitalSemiring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonAssocSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroOneClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : NonAssocSemiring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] : Semiring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonUnitalCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R)

Equations

• HahnSeries.instNonUnitalCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring = let __spread.0 := inferInstance; NonUnitalCommSemiring.mk ⋯

instance HahnSeries.instCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] : CommSemiring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonUnitalNonAssocRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClassToNonUnitalNonAssocSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonUnitalRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalRing R] : NonUnitalRing (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonAssocRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroOneClassToNonAssocSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocRing R] : NonAssocRing (HahnSeries Γ R)

Equations

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

instance HahnSeries.instRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroToSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Ring R] : Ring (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNonUnitalCommRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalCommSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalCommRing R] : NonUnitalCommRing (HahnSeries Γ R)

Equations

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

instance HahnSeries.instCommRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZeroToCommSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommRing R] : CommRing (HahnSeries Γ R)

Equations

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

instance HahnSeries.instNoZeroDivisorsHahnSeriesToPartialOrderToOrderedAddCommMonoidToLinearOrderedAddCommMonoidToZeroToMulZeroClassInstMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClassToOrderedCancelAddCommMonoidInstZeroHahnSeries {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] : NoZeroDivisors (HahnSeries Γ R)

Equations

• ⋯ = ⋯

instance HahnSeries.instIsDomainHahnSeriesToPartialOrderToOrderedAddCommMonoidToLinearOrderedAddCommMonoidToZeroToMonoidWithZeroToSemiringInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroToOrderedCancelAddCommMonoid {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] : IsDomain (HahnSeries Γ R)

Equations

• ⋯ = ⋯

@[simp]

theorem HahnSeries.order_mul {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) : HahnSeries.order (x * y) = HahnSeries.order x + HahnSeries.order y

@[simp]

theorem HahnSeries.order_pow {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [Semiring R] [NoZeroDivisors R] (x : HahnSeries Γ R) (n : ℕ) : HahnSeries.order (x ^ n) = n • HahnSeries.order x

@[simp]

theorem HahnSeries.single_mul_single {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {a : Γ} {b : Γ} {r : R} {s : R} : (HahnSeries.single a) r * (HahnSeries.single b) s = (HahnSeries.single (a + b)) (r * s)

@[simp]

theorem HahnSeries.single_pow {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] (a : Γ) (n : ℕ) (r : R) : (HahnSeries.single a) r ^ n = (HahnSeries.single (n • a)) (r ^ n)

@[simp]

theorem HahnSeries.C_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] (a : R) : HahnSeries.C a = (HahnSeries.single 0) a

def HahnSeries.C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : R →+* HahnSeries Γ R

C a is the constant Hahn Series a. C is provided as a ring homomorphism.

Equations

• HahnSeries.C = { toMonoidHom := { toOneHom := { toFun := ⇑(HahnSeries.single 0), map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

theorem HahnSeries.C_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : HahnSeries.C 0 = 0

theorem HahnSeries.C_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : HahnSeries.C 1 = 1

theorem HahnSeries.C_injective {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : Function.Injective ⇑HahnSeries.C

theorem HahnSeries.C_ne_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] {r : R} (h : r ≠ 0) : HahnSeries.C r ≠ 0

theorem HahnSeries.order_C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] {r : R} : HahnSeries.order (HahnSeries.C r) = 0

theorem HahnSeries.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : HahnSeries.C r * x = r • x

theorem HahnSeries.embDomain_mul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ') (hf : ∀ (x y : Γ), f (x + y) = f x + f y) (x : HahnSeries Γ R) (y : HahnSeries Γ R) : HahnSeries.embDomain f (x * y) = HahnSeries.embDomain f x * HahnSeries.embDomain f y

theorem HahnSeries.embDomain_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ ↪o Γ') (hf : f 0 = 0) : HahnSeries.embDomain f 1 = 1

@[simp]

theorem HahnSeries.embDomainRingHom_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : ∀ (a : HahnSeries Γ R), (HahnSeries.embDomainRingHom f hfi hf) a = HahnSeries.embDomain { toEmbedding := { toFun := ⇑f, inj' := hfi }, map_rel_iff' := ⋯ } a

def HahnSeries.embDomainRingHom {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : HahnSeries Γ R →+* HahnSeries Γ' R

Extending the domain of Hahn series is a ring homomorphism.

Equations

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

theorem HahnSeries.embDomainRingHom_C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective ⇑f} {hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'} {r : R} : (HahnSeries.embDomainRingHom f hfi hf) (HahnSeries.C r) = HahnSeries.C r

instance HahnSeries.instAlgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] : Algebra R (HahnSeries Γ A)

Equations

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

theorem HahnSeries.C_eq_algebraMap {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] : HahnSeries.C = algebraMap R (HahnSeries Γ R)

theorem HahnSeries.algebraMap_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {r : R} : (algebraMap R (HahnSeries Γ A)) r = HahnSeries.C ((algebraMap R A) r)

instance HahnSeries.instNontrivialSubalgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroToSemiringInstAlgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroId {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] [Nontrivial Γ] [Nontrivial R] : Nontrivial (Subalgebra R (HahnSeries Γ R))

Equations

• ⋯ = ⋯

@[simp]

theorem HahnSeries.embDomainAlgHom_apply_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {Γ' : Type u_4} [OrderedCancelAddCommMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : ∀ (a : HahnSeries Γ A) (b : Γ'), ((HahnSeries.embDomainAlgHom f hfi hf) a).coeff b = if h : ∃ (x : Γ), ¬a.coeff x = 0 ∧ f x = b then a.coeff (Classical.choose ⋯) else 0

def HahnSeries.embDomainAlgHom {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {Γ' : Type u_4} [OrderedCancelAddCommMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') : HahnSeries Γ A →ₐ[R] HahnSeries Γ' A

Extending the domain of Hahn series is an algebra homomorphism.

Equations

• HahnSeries.embDomainAlgHom f hfi hf = let __src := HahnSeries.embDomainRingHom f hfi hf; { toRingHom := __src, commutes' := ⋯ }