Documentation

Mathlib.RingTheory.HahnSeries.Basic

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, with the most studied case being when Γ is a linearly ordered abelian group and R is a field, in which case HahnSeries Γ R is a valued field, with value group Γ. These generalize Laurent series (with value group ), and Laurent series are implemented that way in the file RingTheory/LaurentSeries.

Main Definitions #

References #

structure HahnSeries (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [Zero R] :
Type (max u_1 u_2)

If Γ is linearly ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are well-founded.

  • coeff : ΓR

    The coefficient function of a Hahn Series.

  • isPWO_support' : (Function.support self.coeff).IsPWO
Instances For
    theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} :
    ∀ {inst : PartialOrder Γ} {inst_1 : Zero R} {x y : HahnSeries Γ R}, x.coeff = y.coeffx = y
    theorem HahnSeries.isPWO_support' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (self : HahnSeries Γ R) :
    (Function.support self.coeff).IsPWO
    theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :
    Function.Injective HahnSeries.coeff
    @[simp]
    theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} :
    x.coeff = y.coeff x = y
    def HahnSeries.support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :
    Set Γ

    The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.

    Equations
    Instances For
      @[simp]
      theorem HahnSeries.isPWO_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :
      x.support.IsPWO
      @[simp]
      theorem HahnSeries.isWF_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :
      x.support.IsWF
      @[simp]
      theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) (a : Γ) :
      a x.support x.coeff a 0
      instance HahnSeries.instZero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :
      Equations
      • HahnSeries.instZero = { zero := { coeff := 0, isPWO_support' := } }
      instance HahnSeries.instInhabited {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :
      Equations
      • HahnSeries.instInhabited = { default := 0 }
      instance HahnSeries.instSubsingleton {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Subsingleton R] :
      Equations
      • =
      @[simp]
      theorem HahnSeries.zero_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} :
      @[simp]
      theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
      x.coeff = 0 x = 0
      theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g 0) :
      x 0
      @[simp]
      theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :
      @[simp]
      theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
      x.support.Nonempty x 0
      @[simp]
      theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
      x.support = x = 0
      def HahnSeries.map {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) {F : Type u_5} [FunLike F R S] [ZeroHomClass F R S] (f : F) :

      The map of Hahn series induced by applying a zero-preserving map to each coefficient.

      Equations
      • x.map f = { coeff := fun (g : Γ) => f (x.coeff g), isPWO_support' := }
      Instances For
        @[simp]
        theorem HahnSeries.map_coeff {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) {F : Type u_5} [FunLike F R S] [ZeroHomClass F R S] (f : F) (g : Γ) :
        (x.map f).coeff g = f (x.coeff g)
        @[simp]
        theorem HahnSeries.map_zero {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (f : ZeroHom R S) :
        def HahnSeries.ofIterate {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) :
        HahnSeries (Lex (Γ × Γ')) R

        Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product.

        Equations
        • x.ofIterate = { coeff := fun (g : Lex (Γ × Γ')) => (x.coeff g.1).coeff g.2, isPWO_support' := }
        Instances For
          @[simp]
          theorem HahnSeries.mk_eq_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (f : ΓR) (h : (Function.support f).IsPWO) :
          { coeff := f, isPWO_support' := h } = 0 f = 0
          def HahnSeries.toIterate {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries (Lex (Γ × Γ')) R) :

          Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series.

          Equations
          • x.toIterate = { coeff := fun (g : Γ) => { coeff := fun (g' : Γ') => x.coeff (g, g'), isPWO_support' := }, isPWO_support' := }
          Instances For
            def HahnSeries.iterateEquiv {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] :
            HahnSeries Γ (HahnSeries Γ' R) HahnSeries (Lex (Γ × Γ')) R

            The equivalence between iterated Hahn series and Hahn series on the lex product.

            Equations
            • HahnSeries.iterateEquiv = { toFun := HahnSeries.ofIterate, invFun := HahnSeries.toIterate, left_inv := , right_inv := }
            Instances For
              @[simp]
              theorem HahnSeries.iterateEquiv_symm_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries (Lex (Γ × Γ')) R) :
              HahnSeries.iterateEquiv.symm x = x.toIterate
              @[simp]
              theorem HahnSeries.iterateEquiv_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) :
              HahnSeries.iterateEquiv x = x.ofIterate
              def HahnSeries.single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (a : Γ) :

              single a r is the Hahn series which has coefficient r at a and zero otherwise.

              Equations
              Instances For
                @[simp]
                theorem HahnSeries.single_coeff_same {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (a : Γ) (r : R) :
                ((HahnSeries.single a) r).coeff a = r
                @[simp]
                theorem HahnSeries.single_coeff_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} (h : b a) :
                ((HahnSeries.single a) r).coeff b = 0
                theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} :
                ((HahnSeries.single a) r).coeff b = if b = a then r else 0
                @[simp]
                theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r 0) :
                ((HahnSeries.single a) r).support = {a}
                theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :
                ((HahnSeries.single a) r).support {a}
                theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b ((HahnSeries.single a) r).support) :
                b = a
                theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} :
                theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r 0) :
                @[simp]
                theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :
                (HahnSeries.single a) r = 0 r = 0
                @[simp]
                theorem HahnSeries.map_single {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero S] (f : ZeroHom R S) :
                ((HahnSeries.single a) r).map f = (HahnSeries.single a) (f r)
                Equations
                • =
                def HahnSeries.orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

                The orderTop of a Hahn series x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is when x = 0.

                Equations
                • x.orderTop = if h : x = 0 then else (.min )
                Instances For
                  @[simp]
                  theorem HahnSeries.orderTop_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :
                  theorem HahnSeries.orderTop_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x 0) :
                  x.orderTop = (.min )
                  @[simp]
                  theorem HahnSeries.ne_zero_iff_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
                  x 0 x.orderTop
                  theorem HahnSeries.orderTop_eq_top_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
                  x.orderTop = x = 0
                  theorem HahnSeries.untop_orderTop_of_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x 0) :
                  x.orderTop.untop = .min
                  theorem HahnSeries.coeff_orderTop_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (hg : x.orderTop = g) :
                  x.coeff g 0
                  theorem HahnSeries.orderTop_le_of_coeff_ne_zero {R : Type u_3} [Zero R] {Γ : Type u_5} [LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g 0) :
                  x.orderTop g
                  @[simp]
                  theorem HahnSeries.orderTop_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r 0) :
                  ((HahnSeries.single a) r).orderTop = a
                  theorem HahnSeries.orderTop_single_le {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :
                  a ((HahnSeries.single a) r).orderTop
                  theorem HahnSeries.lt_orderTop_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {r : R} {g : Γ} {g' : Γ} (hgg' : g < g') :
                  g < ((HahnSeries.single g') r).orderTop
                  theorem HahnSeries.coeff_eq_zero_of_lt_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {i : Γ} (hi : i < x.orderTop) :
                  x.coeff i = 0
                  def HahnSeries.leadingCoeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :
                  R

                  A leading coefficient of a Hahn series is the coefficient of a lowest-order nonzero term, or zero if the series vanishes.

                  Equations
                  • x.leadingCoeff = if h : x = 0 then 0 else x.coeff (.min )
                  Instances For
                    @[simp]
                    theorem HahnSeries.leadingCoeff_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x 0) :
                    x.leadingCoeff = x.coeff (.min )
                    theorem HahnSeries.leadingCoeff_eq_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
                    x.leadingCoeff = 0 x = 0
                    theorem HahnSeries.leadingCoeff_ne_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :
                    x.leadingCoeff 0 x 0
                    theorem HahnSeries.leadingCoeff_of_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :
                    ((HahnSeries.single a) r).leadingCoeff = r
                    def HahnSeries.order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] (x : HahnSeries Γ R) :
                    Γ

                    The order of a nonzero Hahn series x is a minimal element of Γ where x has a nonzero coefficient, the order of 0 is 0.

                    Equations
                    • x.order = if h : x = 0 then 0 else .min
                    Instances For
                      @[simp]
                      theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] :
                      theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x 0) :
                      x.order = .min
                      theorem HahnSeries.order_eq_orderTop_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x 0) :
                      x.order = x.orderTop
                      theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x 0) :
                      x.coeff x.order 0
                      theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_3} [Zero R] {Γ : Type u_5} [AddMonoid Γ] [LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g 0) :
                      x.order g
                      @[simp]
                      theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r 0) :
                      ((HahnSeries.single a) r).order = a
                      theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} {i : Γ} (hi : i < x.order) :
                      x.coeff i = 0
                      theorem HahnSeries.zero_lt_orderTop_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x 0) :
                      0 < x.orderTop 0 < x.order
                      theorem HahnSeries.zero_lt_orderTop_of_order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : 0 < x.order) :
                      0 < x.orderTop
                      theorem HahnSeries.zero_le_orderTop_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} :
                      0 x.orderTop 0 x.order
                      theorem HahnSeries.leadingCoeff_eq {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} :
                      x.leadingCoeff = x.coeff x.order
                      def HahnSeries.embDomain {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (f : Γ ↪o Γ') :
                      HahnSeries Γ RHahnSeries Γ' R

                      Extends the domain of a HahnSeries by an OrderEmbedding.

                      Equations
                      Instances For
                        @[simp]
                        theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} :
                        (HahnSeries.embDomain f x).coeff (f a) = x.coeff a
                        @[simp]
                        theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : ΓΓ'} (hfi : Function.Injective f) (hf : ∀ (g g' : Γ), f g f g' g g') {x : HahnSeries Γ R} {a : Γ} :
                        (HahnSeries.embDomain { toFun := f, inj' := hfi, map_rel_iff' := } x).coeff (f a) = x.coeff a
                        theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : bf '' x.support) :
                        (HahnSeries.embDomain f x).coeff b = 0
                        theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :
                        (HahnSeries.embDomain f x).support f '' x.support
                        theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : bSet.range f) :
                        (HahnSeries.embDomain f x).coeff b = 0
                        @[simp]
                        theorem HahnSeries.embDomain_zero {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} :
                        @[simp]
                        theorem HahnSeries.embDomain_single {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {g : Γ} {r : R} :
                        theorem HahnSeries.embDomain_injective {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} :
                        theorem HahnSeries.forallLTEqZero_supp_BddBelow {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] (f : ΓR) (n : Γ) (hn : m < n, f m = 0) :
                        theorem HahnSeries.suppBddBelow_supp_PWO {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : ΓR) (hf : BddBelow (Function.support f)) :
                        def HahnSeries.ofSuppBddBelow {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : ΓR) (hf : BddBelow (Function.support f)) :

                        Construct a Hahn series from any function whose support is bounded below.

                        Equations
                        Instances For
                          @[simp]
                          theorem HahnSeries.ofSuppBddBelow_coeff {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : ΓR) (hf : BddBelow (Function.support f)) :
                          ∀ (a : Γ), (HahnSeries.ofSuppBddBelow f hf).coeff a = f a
                          theorem HahnSeries.order_ofForallLtEqZero {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] [Zero Γ] (f : ΓR) (hf : f 0) (n : Γ) (hn : m < n, f m = 0) :