Documentation

Mathlib.RingTheory.HahnSeries.Multiplication

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 #

References #

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] :
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.Data.Polynomial.Module for more discussion on this problem.

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

    The casting function to the type synonym.

    Equations
    Instances For
      def HahnModule.rec {Γ : Type u_3} {R : Type u_4} {V : Type u_5} [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R VSort 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
      Instances For
        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] :
        Equations
        @[simp]
        theorem HahnModule.of_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {V : Type u_3} [AddCommMonoid V] [SMul R V] :
        @[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) :
        @[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] :
        Equations
        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
        Equations
        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
        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
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • HahnSeries.instNonUnitalCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring = let __spread.0 := inferInstance; NonUnitalCommSemiring.mk
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem HahnSeries.single_mul_single {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {a : Γ} {b : Γ} {r : R} {s : R} :
        @[simp]
        theorem HahnSeries.C_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] (a : R) :
        HahnSeries.C a = (HahnSeries.single 0) a

        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' := }
        Instances For
          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_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) :
          theorem HahnSeries.embDomain_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ ↪o Γ') (hf : f 0 = 0) :
          @[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') :

          Extending the domain of Hahn series is a ring homomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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
            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)
            @[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') :

            Extending the domain of Hahn series is an algebra homomorphism.

            Equations
            Instances For