Rescaling a formal group law

Let F(X, Y) = ∑_d a_d X^(d 0) Y^(d 1) be a one-dimensional formal group law over a commutative ring R and let s ∈ R. Multiplying the coefficient of every monomial of total degree n ≥ 1 by s ^ (n - 1) gives the series

F^s(X, Y) = X + Y + ∑_{i, j ≥ 1} s ^ (i + j - 1) aᵢⱼ Xⁱ Yʲ,

which satisfies s • F^s(X, Y) = F(s X, s Y); when s is a nonzerodivisor, this identity characterises F^s. When s is a unit, F^s(X, Y) = s⁻¹ F(s X, s Y) is the transport of F along the homothety X ↦ s⁻¹ X (FormalGroup.homothety_smul), and rescaling by s commutes with every change of coordinates up to conjugating the coordinate by that homothety (FormalGroup.rescale_smul). For every s, unit or not, F^s is again a formal group law, FormalGroup.rescale F s, and it is commutative when F is.

This is the action of the multiplicative monoid of R on formal group laws (FormalGroup.rescale_rescale). Applied with s a polynomial variable to the universal formal group law, it records the grading of the Lazard ring: the coefficient aᵢⱼ is acted on by s ^ (i + j - 1).

When s is a nonzerodivisor, associativity of F^s follows from that of F by cancelling s from s • F^s(F^s(X, Y), Z) = F(F(s X, s Y), s Z). The general case is the base change of the case of the polynomial variable s over R[s].

Main definitions

• FormalGroup.rescale F s: the formal group law F^s, with coefficients s ^ (i + j - 1) aᵢⱼ.

Main results

• FormalGroup.coeff_rescale: the coefficient of a monomial of degree n in F^s is s ^ (n - 1) times its coefficient in F.
• FormalGroup.smul_rescale: s • F^s(X, Y) = F(s X, s Y).
• FormalGroup.smul_nsmulSeries_rescale: s • [k]_(F^s)(X) = [k]_F(s X).
• FormalGroup.map_rescale: rescaling commutes with base change.
• FormalGroup.rescale_one and FormalGroup.rescale_rescale: rescaling is an action of the multiplicative monoid of R.
• FormalGroup.rescale_𝔾ₘ_toPowerSeries: rescaling X + Y + XY by s gives X + Y + s X Y.
• FormalGroup.invariantDifferential_rescale: the invariant differential of F^s is P(s T) dT when that of F is P(T) dT.
• FormalGroup.homothety_smul: transporting F along the homothety X ↦ u X by a unit u is rescaling by u⁻¹.
• FormalGroup.rescale_smul: rescaling by a unit commutes with changes of coordinates, up to conjugating the coordinate by a homothety.
• FormalGroup.rescale_ofStrictCoeffs_smul_𝔾ₐ: rescaling by a unit u the additive law transported along X + ∑ bᵢ X^(i + 1) multiplies each bᵢ by uⁱ.
• FormalGroup.isWeightedHomogeneous_coeff_ofStrictCoeffs_X_smul_𝔾ₐ: the coefficient of X^(d 0) Y^(d 1) in the additive law transported along X + ∑ bᵢ X^(i + 1), with indeterminate bᵢ of weight i, is weighted homogeneous of degree d 0 + d 1 - 1.
• FormalGroup.subst_rescale_toPowerSeries_of_smul_eq_rescale: if g is additive along F and s • gₛ = g(s X) for a nonzerodivisor s, then gₛ is additive along F^s.
• FormalGroup.map_toPolynomial_eq_rescale_iff: over a ring graded by ℕ, F has its coefficient of Xⁱ Yʲ in degree w * (i + j - 1) exactly when its base change along a ↦ ∑ₙ aₙ Tⁿ is its rescaling by T ^ w.
• FormalGroup.coeff_nsmulSeries_mem: for such a graded F, the coefficient of X^m in [k]_F has degree w * (m - 1).

References

• M. Hazewinkel, Formal Groups and Applications, Chapter I, §1.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.

def FormalGroup.rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) : FormalGroup R

The rescaling F^s of a formal group law F by s ∈ R: the formal group law whose coefficient of Xⁱ Yʲ is s ^ (i + j - 1) times that of F. It satisfies s • F^s(X, Y) = F(s X, s Y) (FormalGroup.smul_rescale), so F^s(X, Y) = s⁻¹ F(s X, s Y) when s is a unit.

@[simp]

theorem FormalGroup.coeff_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) (d : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff d) (F.rescale s).toPowerSeries = s ^ (Finsupp.degree d - 1) * (MvPowerSeries.coeff d) F.toPowerSeries

The coefficient of a monomial of total degree n in F^s is s ^ (n - 1) times its coefficient in F.

theorem FormalGroup.smul_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) : s • (F.rescale s).toPowerSeries = (MvPowerSeries.rescale fun (x : Fin 2) => s) F.toPowerSeries

The rescaling satisfies s • F^s(X, Y) = F(s X, s Y). This identity characterises F^s when s is a nonzerodivisor, but not in general: for s = 0 every series satisfies it.

theorem FormalGroup.smul_nsmulSeries_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) (k : ℕ) : s • (F.rescale s).nsmulSeries k = (PowerSeries.rescale s) (F.nsmulSeries k)

Multiplication by k on the rescaling: s • [k]_(F^s)(X) = [k]_F(s X).

instance FormalGroup.instIsCommRescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) [F.IsComm] : (F.rescale s).IsComm

The rescaling of a commutative formal group law is commutative.

@[simp]

theorem FormalGroup.map_rescale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) (s : R) (f : R →+* S) : (F.rescale s).map f = (F.map f).rescale (f s)

Rescaling commutes with base change: (F^s).map f = (F.map f)^(f s).

@[simp]

theorem FormalGroup.rescale_one {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.rescale 1 = F

Rescaling by 1 does nothing.

theorem FormalGroup.rescale_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s t : R) : (F.rescale s).rescale t = F.rescale (s * t)

Rescaling is an action of the multiplicative monoid: (F^s)^t = F^(s t).

@[simp]

theorem FormalGroup.rescale_𝔾ₐ {R : Type u_1} [CommRing R] (s : R) : 𝔾ₐ.rescale s = 𝔾ₐ

Rescaling does not change the additive formal group law.

@[simp]

theorem FormalGroup.rescale_𝔾ₘ_toPowerSeries {R : Type u_1} [CommRing R] (s : R) : (𝔾ₘ.rescale s).toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1 + s • (MvPowerSeries.X 0 * MvPowerSeries.X 1)

Rescaling the multiplicative formal group law by s gives X + Y + s X Y.

@[simp]

theorem FormalGroup.invariantDifferential_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) : (F.rescale s).invariantDifferential = (PowerSeries.rescale s) F.invariantDifferential

The invariant differential of a rescaling: if P(T) dT is the invariant differential of F, then P(s T) dT is that of F^s.

theorem FormalGroup.homothety_smul {R : Type u_1} [CommRing R] (F : FormalGroup R) (u : Rˣ) : TauCeti.FormalCoordinate.homothety u • F = F.rescale ↑u⁻¹

Changing coordinates by a homothety is rescaling: transporting F along X ↦ u X gives u F(u⁻¹ X, u⁻¹ Y), the rescaling of F by u⁻¹.

theorem FormalGroup.rescale_smul {R : Type u_1} [CommRing R] (F : FormalGroup R) (u : Rˣ) (φ : TauCeti.FormalCoordinate R) : (φ • F).rescale ↑u = (TauCeti.FormalCoordinate.homothety u⁻¹ * φ * TauCeti.FormalCoordinate.homothety u) • F.rescale ↑u

Rescaling commutes with changes of coordinates: rescaling φ • F by a unit u gives the rescaling of F by u, transported along the conjugate u⁻¹ φ(u X) of φ.

theorem FormalGroup.rescale_ofStrictCoeffs_smul_𝔾ₐ {R : Type u_1} [CommRing R] (u : Rˣ) (b : ℕ+ → R) : (TauCeti.FormalCoordinate.ofStrictCoeffs b • 𝔾ₐ).rescale ↑u = (TauCeti.FormalCoordinate.ofStrictCoeffs fun (i : ℕ+) => ↑u ^ ↑i * b i) • 𝔾ₐ

Rescaling by a unit u the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1) gives the additive law transported along X + ∑ uⁱ bᵢ X^(i + 1).

theorem FormalGroup.subst_rescale_toPowerSeries_of_smul_eq_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} {g gₛ : PowerSeries R} (hs : IsLeftRegular s) (hgₛ : s • gₛ = (PowerSeries.rescale s) g) (hg : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g) : PowerSeries.subst (F.rescale s).toPowerSeries gₛ = PowerSeries.subst (MvPowerSeries.X 0) gₛ + PowerSeries.subst (MvPowerSeries.X 1) gₛ

If g is additive along F and s • gₛ = g(s X) for a nonzerodivisor s, then gₛ is additive along the rescaling F^s. Multiplied by s, both sides of the additivity of gₛ become g(F(s X, s Y)) = g(s X) + g(s Y).

theorem FormalGroup.map_toPolynomial_eq_rescale_iff {A : Type u_3} {σ : Type u_4} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (F : FormalGroup A) (w : ℕ) : F.map (TauCeti.GradedAlgebra.toPolynomial 𝒜) = (F.map Polynomial.C).rescale (Polynomial.X ^ w) ↔ ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (w * (Finsupp.degree d - 1))

The grading as rescaling by a power of a polynomial variable. A formal group law has its coefficient of X^(d 0) Y^(d 1) in degree w * (d 0 + d 1 - 1) exactly when its base change along a ↦ ∑ₙ aₙ Tⁿ is its rescaling by T ^ w.

theorem FormalGroup.coeff_nsmulSeries_mem {A : Type u_3} {σ : Type u_4} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (F : FormalGroup A) {w : ℕ} (hF : ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (w * (Finsupp.degree d - 1))) (k m : ℕ) : (PowerSeries.coeff m) (F.nsmulSeries k) ∈ 𝒜 (w * (m - 1))

Multiplication by k on a graded formal group law is graded. If the coefficient of X^(d 0) Y^(d 1) in F has degree w * (d 0 + d 1 - 1) for every d, then the coefficient of X^m in [k]_F has degree w * (m - 1).

theorem FormalGroup.isWeightedHomogeneous_coeff_ofStrictCoeffs_X_smul_𝔾ₐ {R : Type u_1} [CommRing R] (d : Fin 2 →₀ ℕ) : MvPolynomial.IsWeightedHomogeneous (fun (i : ℕ+) => ↑i) ((MvPowerSeries.coeff d) (TauCeti.FormalCoordinate.ofStrictCoeffs MvPolynomial.X • 𝔾ₐ).toPowerSeries) (Finsupp.degree d - 1)

The transported additive law is graded. The coefficient of X^(d 0) Y^(d 1) in the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1) over R[b₁, b₂, …] is weighted homogeneous of degree d 0 + d 1 - 1, for bᵢ of weight i.