Documentation

TauCeti.RingTheory.FormalGroup.CoordinateChange.Basic

Changing the coordinate of a formal group law #

A formal group law F(X, Y) over a commutative ring R is the group law of the formal group written in one particular formal parameter. Changing the parameter by a formal coordinate φ = u X + ⋯ (u a unit, TauCeti.FormalCoordinate R) transports F to the formal group law

(φ • F)(X, Y) = φ(F(φ⁻¹(X), φ⁻¹(Y))),

for which φ is a homomorphism from F: (φ • F)(φ(X), φ(Y)) = φ(F(X, Y)). As φ has the compositional inverse φ⁻¹, it is an isomorphism of formal group laws from F to φ • F, strict when u = 1. The construction is a left action of the group of formal coordinates on formal group laws, compatible with commutativity and with base change of the coefficient ring.

The universal instance of this action, a strict coordinate with indeterminate coefficients acting on the universal formal group law, is what makes strict isomorphisms of formal group laws representable by a polynomial ring over the Lazard ring.

Main definitions #

FormalGroup.changeCoordinate: the formal group law φ(F(φ⁻¹(X), φ⁻¹(Y))), written φ • F.
FormalGroup.instMulActionFormalCoordinate: the action φ • F of formal coordinates on formal group laws.
FormalGroup.smulIso: the isomorphism φ of formal group laws from F to φ • F.

Main results #

FormalGroup.subst_smul_toPowerSeries: (φ • F)(x, y) = φ(F(φ⁻¹(x), φ⁻¹(y))) for all substitutable x, y.
FormalGroup.subst_toPowerSeries_eq_subst_smul_toPowerSeries: φ is a homomorphism from F to φ • F, that is φ(F(X, Y)) = (φ • F)(φ(X), φ(Y)).
FormalGroup.isStrict_smulIso_iff: the isomorphism φ is strict exactly when its linear coefficient is 1.
TauCeti.FormalGroupHom.smul_eq: if φ is a homomorphism from F to G, then φ • F = G.
FormalGroup.instIsCommSMul: changing coordinates preserves commutativity.
FormalGroup.map_smul: changing coordinates commutes with base change.
FormalGroup.map_ofStrictCoeffs_smul_𝔾ₐ: the base change of the additive law transported along X + ∑ bᵢ X^(i + 1) is transported along X + ∑ f(bᵢ) X^(i + 1).
FormalGroup.nsmulSeries_smul_eq_zero_iff: changing coordinates preserves [n](X) = 0.
FormalGroup.nsmulSeries_smul_𝔾ₐ_eq_zero: if n = 0 in R, then [n](X) = 0 for every transport φ • 𝔾ₐ of the additive formal group law.
FormalGroup.ofStrictCoeffs_single_smul_𝔾ₐ_toPowerSeries: if e² = 0, transporting the additive law along X + e X^(n + 1) gives X + Y + e ((X + Y)^(n + 1) - X^(n + 1) - Y^(n + 1)).
FormalGroup.nsmulSeries_ofStrictCoeffs_single_smul_𝔾ₐ: if e² = 0, multiplication by k on that law is k X + e (k^(n + 1) - k) X^(n + 1).

References #

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

noncomputable def FormalGroup.changeCoordinate {R : Type u_1} [CommRing R] (F : FormalGroup R) (φ : TauCeti.FormalCoordinate R) :

The change of coordinate of a formal group law: the formal group law φ(F(φ⁻¹(X), φ⁻¹(Y))) obtained by transporting F along the formal coordinate φ. It is written φ • F (FormalGroup.instMulActionFormalCoordinate), and its API is stated for φ • F.

Instances For

@[instance_reducible]

noncomputable instance FormalGroup.instSMulFormalCoordinate {R : Type u_1} [CommRing R] :

SMul (TauCeti.FormalCoordinate R) (FormalGroup R)

Formal coordinates act on formal group laws by change of coordinate, φ • F = φ(F(φ⁻¹(X), φ⁻¹(Y))).

@[simp]

theorem FormalGroup.changeCoordinate_eq_smul {R : Type u_1} [CommRing R] (F : FormalGroup R) (φ : TauCeti.FormalCoordinate R) :

F.changeCoordinate φ = φ • F

F.changeCoordinate φ is the action φ • F.

theorem FormalGroup.smul_toPowerSeries {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

(φ • F).toPowerSeries = PowerSeries.subst (MvPowerSeries.subst ![PowerSeries.subst (MvPowerSeries.X 0) φ⁻¹.toPowerSeries, PowerSeries.subst (MvPowerSeries.X 1) φ⁻¹.toPowerSeries] F.toPowerSeries) φ.toPowerSeries

The series of φ • F is φ(F(φ⁻¹(X), φ⁻¹(Y))).

theorem FormalGroup.subst_smul_toPowerSeries {R : Type u_1} [CommRing R] {σ : Type u_3} (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) {x y : MvPowerSeries σ R} (hx : PowerSeries.HasSubst x) (hy : PowerSeries.HasSubst y) :

The formal group law φ • F at substitutable x, y is φ(F(φ⁻¹(x), φ⁻¹(y))).

theorem FormalGroup.subst_smul_toPowerSeries_subst {R : Type u_1} [CommRing R] {σ : Type u_3} (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) {x y : MvPowerSeries σ R} (hx : PowerSeries.HasSubst x) (hy : PowerSeries.HasSubst y) :

MvPowerSeries.subst ![PowerSeries.subst x φ.toPowerSeries, PowerSeries.subst y φ.toPowerSeries] (φ • F).toPowerSeries = PowerSeries.subst (MvPowerSeries.subst ![x, y] F.toPowerSeries) φ.toPowerSeries

A change of coordinate φ is additive from F to φ • F on substitutable series: (φ • F)(φ(x), φ(y)) = φ(F(x, y)).

theorem FormalGroup.subst_toPowerSeries_eq_subst_smul_toPowerSeries {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

PowerSeries.subst F.toPowerSeries φ.toPowerSeries = MvPowerSeries.subst ![PowerSeries.subst (MvPowerSeries.X 0) φ.toPowerSeries, PowerSeries.subst (MvPowerSeries.X 1) φ.toPowerSeries] (φ • F).toPowerSeries

A change of coordinate φ is a homomorphism from F to φ • F: φ(F(X, Y)) = (φ • F)(φ(X), φ(Y)).

@[instance_reducible]

noncomputable instance FormalGroup.instMulActionFormalCoordinate {R : Type u_1} [CommRing R] :

MulAction (TauCeti.FormalCoordinate R) (FormalGroup R)

Formal coordinates act on formal group laws: 1 • F = F and (φ * ψ) • F = φ • (ψ • F).

instance FormalGroup.instIsCommSMul {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) [F.IsComm] :

(φ • F).IsComm

Changing coordinates preserves commutativity.

theorem FormalGroup.map_smul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

(φ • F).map f = (TauCeti.FormalCoordinate.map f) φ • F.map f

Changing coordinates commutes with base change: for f : R →+* S, the base change of φ • F is the base change of φ acting on the base change of F.

theorem FormalGroup.map_ofStrictCoeffs_smul_𝔾ₐ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (b : ℕ+ → R) :

(TauCeti.FormalCoordinate.ofStrictCoeffs b • 𝔾ₐ).map f = TauCeti.FormalCoordinate.ofStrictCoeffs (⇑f ∘ b) • 𝔾ₐ

The base change along f : R →+* S of the additive formal group law transported along the strict coordinate X + ∑ bᵢ X^(i + 1) is the additive law transported along X + ∑ f(bᵢ) X^(i + 1).

noncomputable def FormalGroup.smulIso {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

TauCeti.FormalGroupIso F (φ • F)

Changing coordinates gives an isomorphic formal group law: the formal coordinate φ is an isomorphism of formal group laws from F to φ • F, with inverse φ⁻¹.

Instances For

@[simp]

theorem FormalGroup.smulIso_toHom_toPowerSeries {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

(smulIso φ F).toHom.toPowerSeries = φ.toPowerSeries

@[simp]

theorem FormalGroup.smulIso_invHom_toPowerSeries {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

(smulIso φ F).invHom.toPowerSeries = φ⁻¹.toPowerSeries

theorem TauCeti.FormalGroupHom.smul_eq {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {φ : FormalCoordinate R} (h : f.toPowerSeries = φ.toPowerSeries) :

φ • F = G

A coordinate that is a homomorphism changes the source into the target: if the series of the formal coordinate φ underlies a homomorphism of formal group laws from F to G, then φ • F = G. Thus every isomorphism of formal group laws is, up to equality of the target, one of the isomorphisms FormalGroup.smulIso.

theorem FormalGroup.isStrict_smulIso_iff {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) :

(smulIso φ F).IsStrict ↔ TauCeti.FormalCoordinate.linearCoeff φ = 1

The isomorphism φ from F to φ • F is strict exactly when φ has linear coefficient 1.

@[simp]

theorem FormalGroup.nsmulSeries_smul_eq_zero_iff {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) {n : ℕ} :

(φ • F).nsmulSeries n = 0 ↔ F.nsmulSeries n = 0

Changing coordinates preserves exponents: φ • F is killed by n exactly when F is.

theorem FormalGroup.nsmulSeries_smul_𝔾ₐ_eq_zero {R : Type u_1} [CommRing R] (φ : TauCeti.FormalCoordinate R) {n : ℕ} (hn : ↑n = 0) :

(φ • 𝔾ₐ).nsmulSeries n = 0

Transporting the additive formal group law kills n when n = 0: if n = 0 in R, then [n](X) = 0 for the formal group law φ • 𝔾ₐ = φ(φ⁻¹(X) + φ⁻¹(Y)). This is a converse of FormalGroup.natCast_eq_zero_of_nsmulSeries_eq_zero.

theorem FormalGroup.ofStrictCoeffs_single_smul_𝔾ₐ_toPowerSeries {R : Type u_1} [CommRing R] (n : ℕ+) {e : R} (he : e * e = 0) :

(TauCeti.FormalCoordinate.ofStrictCoeffs (Pi.single n e) • 𝔾ₐ).toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1 + MvPowerSeries.C e * ((MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ (↑n + 1) - MvPowerSeries.X 0 ^ (↑n + 1) - MvPowerSeries.X 1 ^ (↑n + 1))

If e² = 0, transporting the additive formal group law along X + e X^(n + 1) gives X + Y + e ((X + Y)^(n + 1) - X^(n + 1) - Y^(n + 1)). For instance, over the dual numbers this is the first-order deformation of X + Y in the direction of the coordinate coefficient bₙ.

theorem FormalGroup.nsmulSeries_ofStrictCoeffs_single_smul_𝔾ₐ {R : Type u_1} [CommRing R] (n : ℕ+) {e : R} (he : e * e = 0) (k : ℕ) :

(TauCeti.FormalCoordinate.ofStrictCoeffs (Pi.single n e) • 𝔾ₐ).nsmulSeries k = PowerSeries.C ↑k * PowerSeries.X + PowerSeries.C (e * (↑k ^ (↑n + 1) - ↑k)) * PowerSeries.X ^ (↑n + 1)

If e² = 0, multiplication by k on the additive formal group law transported along X + e X^(n + 1) is [k](X) = k X + e (k^(n + 1) - k) X^(n + 1).