Documentation

TauCeti.RingTheory.HahnSeries.Twist

Twisting Hahn series by a character of the exponent monoid #

Let χ : Multiplicative Γ →* R be a character of the exponent monoid Γ with values in a commutative semiring R. Multiplying the coefficient of t ^ g by χ g is an R-algebra endomorphism of HahnSeries Γ R, the twist by χ: it can only shrink supports, and it is multiplicative because χ (g + h) = χ g * χ h for every pair of exponents (g, h) contributing to a coefficient of a product. Twisting by a product of characters is the composite of the twists, so unit-valued characters give R-algebra automorphisms.

For Laurent series and χ k = a ^ k this is the rescaling f (X) ↦ f (a X). For rational exponents, a character of ℚ trivial on ℤ built from a compatible system of roots of unity gives the coefficientwise Galois action on Puiseux series, t ^ (k / n) ↦ ζₙ ^ k t ^ (k / n).

Main definitions #

Main results #

source
noncomputable def HahnSeries.twist {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* R) :
HahnSeries Γ R →ₐ[R] HahnSeries Γ R

The twist of Hahn series by a character χ of the exponent monoid: the R-algebra endomorphism multiplying the coefficient of t ^ g by χ g.

Instances For
    source
    @[simp]
    theorem HahnSeries.coeff_twist {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* R) (x : HahnSeries Γ R) (g : Γ) :
    ((twist χ) x).coeff g = χ (Multiplicative.ofAdd g) * x.coeff g

    The twist by χ multiplies the coefficient of t ^ g by χ g.

    source
    theorem HahnSeries.support_twist_subset {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* R) (x : HahnSeries Γ R) :
    ((twist χ) x).support ⊆ x.support

    Twisting does not enlarge the support.

    source
    @[simp]
    theorem HahnSeries.twist_single {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* R) (g : Γ) (r : R) :
    (twist χ) ((single g) r) = (single g) (χ (Multiplicative.ofAdd g) * r)

    The twist of the monomial r t ^ g by χ is χ g r t ^ g.

    source
    @[simp]
    theorem HahnSeries.twist_one {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] :
    twist 1 = AlgHom.id R (HahnSeries Γ R)

    Twisting by the trivial character is the identity.

    source
    theorem HahnSeries.twist_mul {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ ψ : Multiplicative Γ →* R) :
    twist (χ * ψ) = (twist χ).comp (twist ψ)

    Twisting by a product of characters is the composite of the twists.

    source
    noncomputable def HahnSeries.twistEquiv {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] :
    (Multiplicative Γ →* Rˣ) →* HahnSeries Γ R ≃ₐ[R] HahnSeries Γ R

    The twists by unit-valued characters, as a homomorphism to the R-algebra automorphisms of HahnSeries Γ R: the automorphism attached to χ multiplies the coefficient of t ^ g by χ g, and its inverse twists by χ⁻¹.

    Instances For
      source
      theorem HahnSeries.twistEquiv_apply {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* Rˣ) (x : HahnSeries Γ R) :
      (twistEquiv χ) x = (twist ((Units.coeHom R).comp χ)) x

      The automorphism attached to a unit-valued character χ is the twist by χ.

      source
      @[simp]
      theorem HahnSeries.coeff_twistEquiv {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* Rˣ) (x : HahnSeries Γ R) (g : Γ) :
      ((twistEquiv χ) x).coeff g = ↑(χ (Multiplicative.ofAdd g)) * x.coeff g

      The automorphism attached to a unit-valued character χ multiplies the coefficient of t ^ g by χ g.

      source
      @[simp]
      theorem HahnSeries.support_twistEquiv {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* Rˣ) (x : HahnSeries Γ R) :
      ((twistEquiv χ) x).support = x.support

      Twisting by a unit-valued character preserves the support.

      source
      @[simp]
      theorem HahnSeries.orderTop_twistEquiv {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] (χ : Multiplicative Γ →* Rˣ) (x : HahnSeries Γ R) :
      ((twistEquiv χ) x).orderTop = x.orderTop

      Twisting by a unit-valued character preserves the order.