Documentation

TauCeti.RingTheory.LaurentSeries.Substitution.Basic

Substitution into formal Laurent series #

Let K be a field and φ ∈ K⟦X⟧ a nonzero power series with zero constant coefficient. Mathlib's PowerSeries.subst substitutes φ into power series, f ↦ f (φ). Since φ is nonzero, this is injective (PowerSeries.subst_eq_zero_iff), and so it extends uniquely to a K-algebra map f ↦ f (φ) of the fraction field K⸨X⸩. This file constructs that extension and computes its effect on orders, valuations and coefficients.

Writing a Laurent series as f = X ^ N * f₊ with N ∈ ℤ and f₊ ∈ K⟦X⟧, the substitution is f (φ) = φ ^ N * f₊ (φ), for every such representation (TauCeti.LaurentSeries.substAlgHom_single_mul_coe). If φ has order e ≥ 1, then ord (f (φ)) = e * ord f, so the valuation is raised to the power e. In particular the substitution is injective and continuous for the valuation topology. Substitutions compose as power series do: substituting φ and then ψ is substituting φ (ψ). The ramified substitution X ↦ X ^ e is the exponent embedding n ↦ e * n of Hahn series. Formal differentiation obeys the chain rule D(f (φ)) = (Df)(φ) Dφ, and the residue obeys the finite-map formula Res(f (φ) Dφ dX) = ord φ • Res(f dX) in all characteristics (in particular, coordinate changes of order 1 preserve the residue). A formal coordinate φ = u X + ⋯, u ≠ 0, gives a substitution automorphism of K⸨X⸩, inverse to that of φ⁻¹. Substitution is natural in the coefficient field: a field embedding K → L, applied to every coefficient, carries f (φ) to the substitution of the image of φ into the image of f.

Main definitions #

Main results #

source
noncomputable def TauCeti.LaurentSeries.substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) :
LaurentSeries K →ₐ[K] LaurentSeries K

Substitution f ↦ f (φ) of a nonzero power series φ with zero constant coefficient into Laurent series, as a K-algebra map. It is the unique extension of PowerSeries.subst to the fraction field K⸨X⸩ of K⟦X⟧.

Instances For
    source
    @[simp]
    theorem TauCeti.LaurentSeries.substAlgHom_coe {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : PowerSeries K) :
    (substAlgHom hφ hφ₀) ((HahnSeries.ofPowerSeries ℤ K) f) = (HahnSeries.ofPowerSeries ℤ K) (PowerSeries.subst φ f)

    On power series, substitution into Laurent series is PowerSeries.subst.

    source
    theorem TauCeti.LaurentSeries.substAlgHom_single_one {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) :
    (substAlgHom hφ hφ₀) ((HahnSeries.single 1) 1) = (HahnSeries.ofPowerSeries ℤ K) φ

    Substitution sends the variable X = single 1 1 to φ.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.substAlgHom_single {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (n : ℤ) (a : K) :
    (substAlgHom hφ hφ₀) ((HahnSeries.single n) a) = HahnSeries.C a * (HahnSeries.ofPowerSeries ℤ K) φ ^ n

    Substitution sends the monomial a X ^ n, for every integer n, to a φ ^ n.

    source
    theorem TauCeti.LaurentSeries.substAlgHom_single_mul_coe {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (N : ℤ) (f : PowerSeries K) :
    (substAlgHom hφ hφ₀) ((HahnSeries.single N) 1 * (HahnSeries.ofPowerSeries ℤ K) f) = (HahnSeries.ofPowerSeries ℤ K) φ ^ N * (HahnSeries.ofPowerSeries ℤ K) (PowerSeries.subst φ f)

    Writing a Laurent series as X ^ N * f₊ with f₊ a power series, its substitution is φ ^ N * f₊ (φ). Since substAlgHom does not depend on the representation, neither does this expression.

    source
    theorem TauCeti.LaurentSeries.substAlgHom_injective {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) :
    Function.Injective ⇑(substAlgHom hφ hφ₀)

    Substitution into Laurent series is injective.

    source
    theorem TauCeti.LaurentSeries.valuation_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : LaurentSeries K) :
    Valued.v ((substAlgHom hφ hφ₀) f) = Valued.v f ^ φ.order.toNat

    Substituting φ raises the valuation to the power ord φ.

    source
    theorem TauCeti.LaurentSeries.order_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : LaurentSeries K) :
    HahnSeries.order ((substAlgHom hφ hφ₀) f) = ↑φ.order.toNat * HahnSeries.order f

    Substituting φ multiplies the order by ord φ.

    source
    theorem TauCeti.LaurentSeries.orderTop_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : LaurentSeries K) :
    HahnSeries.orderTop ((substAlgHom hφ hφ₀) f) = φ.order.toNat • HahnSeries.orderTop f

    Substituting φ multiplies the order by ord φ: ord (f (φ)) = ord φ * ord f, including ord 0 = ⊤.

    source
    theorem TauCeti.LaurentSeries.continuous_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) :
    Continuous ⇑(substAlgHom hφ hφ₀)

    Substitution into Laurent series is continuous for the valuation topology.

    source
    theorem TauCeti.LaurentSeries.derivative_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : LaurentSeries K) :
    (LaurentSeries.derivative K) ((substAlgHom hφ hφ₀) f) = (substAlgHom hφ hφ₀) ((LaurentSeries.derivative K) f) * (LaurentSeries.derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)

    Chain rule for Laurent series substitution. The derivative of f (φ) is (Df)(φ) * Dφ.

    source
    theorem TauCeti.LaurentSeries.coeff_neg_one_substAlgHom_mul_derivative_eq_nsmul {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f : LaurentSeries K) :
    ((substAlgHom hφ hφ₀) f * (LaurentSeries.derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)).coeff (-1) = φ.order.toNat • f.coeff (-1)

    Finite-map residue formula for Laurent series substitution. Substituting a nonzero power series φ of zero constant coefficient multiplies the residue of f dX by φ.order.toNat, in all characteristics: Res(f(φ) Dφ dX) = φ.order.toNat • Res(f dX).

    source
    theorem TauCeti.LaurentSeries.coeff_neg_one_substAlgHom_mul_derivative {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (hφ₁ : φ.order = 1) (f : LaurentSeries K) :
    ((substAlgHom hφ hφ₀) f * (LaurentSeries.derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)).coeff (-1) = f.coeff (-1)

    Coordinate-change invariance of the residue (ord φ = 1). If φ has order one, then Res(f(φ) Dφ dX) = Res(f dX).

    source
    theorem TauCeti.LaurentSeries.substAlgHom_comp_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) {ψ : PowerSeries K} (hψ : PowerSeries.constantCoeff ψ = 0) (hψ₀ : ψ ≠ 0) :
    (substAlgHom hψ hψ₀).comp (substAlgHom hφ hφ₀) = substAlgHom ⋯ ⋯

    Substituting φ and then ψ is substituting φ (ψ). The hypotheses on φ (ψ) follow from those on φ and ψ (PowerSeries.constantCoeff_subst_eq_zero, PowerSeries.subst_eq_zero_iff).

    source
    theorem TauCeti.LaurentSeries.substAlgHom_comp_substAlgHom_apply {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) {ψ : PowerSeries K} (hψ : PowerSeries.constantCoeff ψ = 0) (hψ₀ : ψ ≠ 0) (f : LaurentSeries K) :
    (substAlgHom hψ hψ₀) ((substAlgHom hφ hφ₀) f) = (substAlgHom ⋯ ⋯) f

    Substituting φ and then ψ is substituting φ (ψ).

    source
    @[simp]
    theorem TauCeti.LaurentSeries.substAlgHom_X {K : Type u_1} [Field K] :
    substAlgHom ⋯ ⋯ = AlgHom.id K (LaurentSeries K)

    Substituting X is the identity.

    source
    theorem TauCeti.LaurentSeries.substAlgHom_X_pow {K : Type u_1} [Field K] {e : ℕ} (he : e ≠ 0) :
    ↑(substAlgHom ⋯ ⋯) = HahnSeries.embDomainRingHom (AddMonoidHom.mulLeft ↑e) ⋯ ⋯

    The ramified substitution X ↦ X ^ e, for e ≠ 0, multiplies all exponents by e: it is the exponent embedding HahnSeries.embDomainRingHom along n ↦ e * n.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.coeff_substAlgHom_X_pow_mul {K : Type u_1} [Field K] {e : ℕ} (he : e ≠ 0) (f : LaurentSeries K) (n : ℤ) :
    ((substAlgHom ⋯ ⋯) f).coeff (↑e * n) = f.coeff n

    The ramified substitution X ↦ X ^ e moves the coefficient of Xⁿ to X ^ (e * n).

    source
    theorem TauCeti.LaurentSeries.coeff_substAlgHom_X_pow_of_not_dvd {K : Type u_1} [Field K] {e : ℕ} (he : e ≠ 0) (f : LaurentSeries K) {n : ℤ} (hn : ¬↑e ∣ n) :
    ((substAlgHom ⋯ ⋯) f).coeff n = 0

    After the ramified substitution X ↦ X ^ e, only exponents divisible by e occur.

    source
    theorem TauCeti.LaurentSeries.substAlgHom_X_pow_eq_expand {K : Type u_1} [Field K] (d : ℕ+) :
    substAlgHom ⋯ ⋯ = LaurentSeries.expand K d

    The ramified substitution X ↦ X ^ d, for d > 0, is the expansion LaurentSeries.expand K d.

    source
    theorem TauCeti.LaurentSeries.rescale_toAlgHom {K : Type u_1} [Field K] (a : Kˣ) :
    ↑(rescale a) = substAlgHom ⋯ ⋯

    Rescaling by a is the substitution X ↦ a X, so it inherits, for instance, continuity and the chain rule from substAlgHom.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.coeff_substAlgHom_C_mul_X {K : Type u_1} [Field K] {a : K} (ha : a ≠ 0) (f : LaurentSeries K) (n : ℤ) :
    ((substAlgHom ⋯ ⋯) f).coeff n = a ^ n * f.coeff n

    Substituting X ↦ a X, for a ≠ 0, multiplies the coefficient of Xⁿ by a ^ n, for every integer n.

    Naturality in the coefficient field #

    source
    theorem TauCeti.LaurentSeries.mapRingHom_substAlgHom {K : Type u_1} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) {L : Type u_2} [Field L] (σ : K →+* L) {ψ : PowerSeries L} (hψ : PowerSeries.constantCoeff ψ = 0) (hψ₀ : ψ ≠ 0) (h : (PowerSeries.map σ) φ = ψ) (f : LaurentSeries K) :
    (HahnSeries.mapRingHom σ) ((substAlgHom hφ hφ₀) f) = (substAlgHom hψ hψ₀) ((HahnSeries.mapRingHom σ) f)

    Substitution into Laurent series is natural in the coefficient field: applying a field embedding σ : K →+* L to the coefficients of f (φ) gives the substitution of the image ψ of φ into the image of f. The image ψ is passed explicitly, with its (automatic) side conditions, so that it can be given in normal form, such as X ^ e for the ramified substitution.

    Substitution of formal coordinates #

    source
    noncomputable def TauCeti.LaurentSeries.substAlgEquiv {K : Type u_1} [Field K] (φ : FormalCoordinate K) :
    Gal(LaurentSeries K/K)

    The substitution automorphism f ↦ f (φ) of K⸨X⸩ attached to a formal coordinate φ, with inverse the substitution of the compositional inverse φ⁻¹. It extends the substitution automorphism TauCeti.FormalCoordinate.substAlgEquiv of K⟦X⟧ to Laurent series.

    Instances For
      source
      @[simp]
      theorem TauCeti.LaurentSeries.coe_substAlgEquiv {K : Type u_1} [Field K] (φ : FormalCoordinate K) :
      ⇑(substAlgEquiv φ) = ⇑(substAlgHom ⋯ ⋯)

      The substitution automorphism of a formal coordinate is the substitution substAlgHom.

      source
      theorem TauCeti.LaurentSeries.substAlgEquiv_coe {K : Type u_1} [Field K] (φ : FormalCoordinate K) (f : PowerSeries K) :
      (substAlgEquiv φ) ((HahnSeries.ofPowerSeries ℤ K) f) = (HahnSeries.ofPowerSeries ℤ K) (φ.substAlgEquiv f)

      On power series, the substitution automorphism of K⸨X⸩ is that of K⟦X⟧.

      source
      @[simp]
      theorem TauCeti.LaurentSeries.substAlgEquiv_symm {K : Type u_1} [Field K] (φ : FormalCoordinate K) :
      (substAlgEquiv φ).symm = substAlgEquiv φ⁻¹
      source
      @[simp]
      theorem TauCeti.LaurentSeries.substAlgEquiv_mul {K : Type u_1} [Field K] (φ ψ : FormalCoordinate K) :
      substAlgEquiv (φ * ψ) = substAlgEquiv ψ * substAlgEquiv φ

      Substitution automorphisms reverse composition: σ_(φ ∘ ψ) = σ_ψ ∘ σ_φ.

      source
      @[simp]
      theorem TauCeti.LaurentSeries.substAlgEquiv_one {K : Type u_1} [Field K] :
      substAlgEquiv 1 = 1
      source
      theorem TauCeti.LaurentSeries.mapRingHom_substAlgEquiv {K : Type u_1} [Field K] {L : Type u_2} [Field L] (σ : K →+* L) (φ : FormalCoordinate K) (f : LaurentSeries K) :
      (HahnSeries.mapRingHom σ) ((substAlgEquiv φ) f) = (substAlgEquiv ((FormalCoordinate.map σ) φ)) ((HahnSeries.mapRingHom σ) f)

      Substitution automorphisms are natural in the coefficient field: applying a field embedding σ : K →+* L to the coefficients intertwines σ_φ with the substitution automorphism of the base-changed coordinate.

      source
      instance TauCeti.LaurentSeries.instRingHomInvPairLaurentSeriesToRingHomRingEquivToRingEquivSubstAlgEquivSymm {K : Type u_1} [Field K] (φ : FormalCoordinate K) :
      RingHomInvPair ↑(substAlgEquiv φ).toRingEquiv ↑(substAlgEquiv φ).toRingEquiv.symm

      The ring homomorphisms underlying σ_φ and its inverse are inverse to each other, so that σ_φ-semilinear equivalences can be formed.

      source
      instance TauCeti.LaurentSeries.instRingHomInvPairLaurentSeriesToRingHomRingEquivSymmToRingEquivSubstAlgEquiv {K : Type u_1} [Field K] (φ : FormalCoordinate K) :
      RingHomInvPair ↑(substAlgEquiv φ).toRingEquiv.symm ↑(substAlgEquiv φ).toRingEquiv

      The ring homomorphisms underlying the inverse of σ_φ and σ_φ are inverse to each other.