Formal coordinates and automorphisms of power series rings

A formal coordinate over a commutative ring R is a power series φ = u X + ⋯ with zero constant coefficient and unit linear coefficient u. Under composition, (φ * ψ) (X) = φ (ψ (X)), formal coordinates form a group TauCeti.FormalCoordinate R: the identity is X, and the inverse of φ is Mathlib's compositional inverse PowerSeries.substInvOfIsUnit, whose coefficients are determined recursively from the linear coefficient (PowerSeries.substInvFun) and which is the unique compositional inverse (PowerSeries.eq_substInvOfIsUnit_of_subst_eq_X). The linear coefficient is a group homomorphism to Rˣ; its kernel consists of the strict coordinates X + ∑_{i ≥ 1} bᵢ X^(i + 1), which correspond to arbitrary families (bᵢ) of coefficients. The homotheties X ↦ u X split the linear coefficient, and conjugating a strict coordinate by the homothety by u multiplies bᵢ by uⁱ. Applying a ring homomorphism to the coefficients is a group homomorphism of formal coordinates.

Each formal coordinate φ gives the substitution automorphism σ_φ : f ↦ f (φ) of the R-algebra R⟦X⟧. Since f (ψ) (φ) = f (ψ (φ)), the automorphisms compose as σ_φ ∘ σ_ψ = σ_(ψ ∘ φ), so φ ↦ σ_φ reverses products: it is an injective group homomorphism from formal coordinates to the opposite of the automorphism group R⟦X⟧ ≃ₐ[R] R⟦X⟧, whose multiplication is composition. Every substitution automorphism preserves constant coefficients, so it fixes the ideal (X) and induces the identity on R⟦X⟧ / (X) = R.

Over a field K the dictionary is complete. Every K-algebra endomorphism σ of K⟦X⟧ sends X to a series of zero constant coefficient, since σ maps the units X - c, c ≠ 0, to units; hence σ is the substitution of σ X, without any continuity hypothesis (PowerSeries.algHom_eq_substAlgHom). For an automorphism, σ X has a compositional inverse, so its linear coefficient is nonzero. Thus φ ↦ σ_φ is an isomorphism between the formal coordinates over K and the opposite of K⟦X⟧ ≃ₐ[K] K⟦X⟧, with inverse σ ↦ σ X.

Main definitions

• TauCeti.FormalCoordinate R: the group of formal coordinates under composition.
• TauCeti.FormalCoordinate.linearCoeff: the linear coefficient, as a homomorphism to Rˣ.
• TauCeti.FormalCoordinate.map f: base change of formal coordinates along f : R →+* S.
• TauCeti.FormalCoordinate.ofStrictCoeffs b: the strict coordinate X + ∑ bᵢ X^(i + 1).
• TauCeti.FormalCoordinate.strictCoeffsEquiv: strict coordinates correspond to their coefficient families ℕ+ → R.
• TauCeti.FormalCoordinate.homothety u: the homothety X ↦ u X by a unit u.
• TauCeti.FormalCoordinate.substAlgEquiv φ: the substitution automorphism f ↦ f (φ).
• TauCeti.FormalCoordinate.substAlgEquivHom: the antihomomorphism φ ↦ σ_φ.
• TauCeti.FormalCoordinate.ofAlgEquiv σ: over a field, the formal coordinate σ X.
• TauCeti.FormalCoordinate.substAlgEquivMulEquiv K: over a field, the isomorphism between formal coordinates and the opposite of the automorphism group of K⟦X⟧.

Main results

• TauCeti.FormalCoordinate.subst_subst_inv, TauCeti.FormalCoordinate.subst_inv_subst: φ (φ⁻¹ (x)) = x = φ⁻¹ (φ (x)) for every substitutable multivariate series x.
• TauCeti.FormalCoordinate.substAlgEquiv_mul: σ_(φ ∘ ψ) = σ_ψ ∘ σ_φ.
• TauCeti.FormalCoordinate.inv_ofStrictCoeffs_single_of_mul_self_eq_zero: if e² = 0, the inverse of X + e X^(n + 1) is X - e X^(n + 1).
• TauCeti.FormalCoordinate.homothety_inv_mul_ofStrictCoeffs_mul_homothety: conjugating X + ∑ bᵢ X^(i + 1) by the homothety by u gives X + ∑ uⁱ bᵢ X^(i + 1).
• TauCeti.FormalCoordinate.map_substAlgEquiv: substitution commutes with base change of the coefficients.
• TauCeti.FormalCoordinate.constantCoeff_substAlgEquiv: substitution automorphisms preserve constant coefficients.
• TauCeti.FormalCoordinate.substAlgEquiv_ofAlgEquiv: over a field, every automorphism of K⟦X⟧ is the substitution of its value at X.

structure TauCeti.FormalCoordinate (R : Type u_1) [CommRing R] : Type u_1

A formal coordinate over R: a power series φ = u X + ⋯ with zero constant coefficient and unit linear coefficient u. These are the changes of formal parameter X ↦ φ.

• toPowerSeries : PowerSeries R

  The power series φ of the coordinate change X ↦ φ.

• constantCoeff_toPowerSeries : PowerSeries.constantCoeff self.toPowerSeries = 0
• isUnit_coeff_one : IsUnit ((PowerSeries.coeff 1) self.toPowerSeries)

theorem TauCeti.FormalCoordinate.ext {R : Type u_1} {inst✝ : CommRing R} {x y : FormalCoordinate R} (toPowerSeries : x.toPowerSeries = y.toPowerSeries) : x = y

theorem TauCeti.FormalCoordinate.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : FormalCoordinate R} : x = y ↔ x.toPowerSeries = y.toPowerSeries

theorem TauCeti.FormalCoordinate.hasSubst {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : PowerSeries.HasSubst φ.toPowerSeries

A formal coordinate can be substituted into any power series.

@[simp]

theorem TauCeti.FormalCoordinate.X_subst_toPowerSeries {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : PowerSeries.subst φ.toPowerSeries PowerSeries.X = φ.toPowerSeries

@[simp]

theorem TauCeti.FormalCoordinate.order_toPowerSeries {R : Type u_1} [CommRing R] [Nontrivial R] (φ : FormalCoordinate R) : φ.toPowerSeries.order = 1

Over a nontrivial ring a formal coordinate has order one.

theorem TauCeti.FormalCoordinate.toPowerSeries_ne_zero {R : Type u_1} [CommRing R] [Nontrivial R] (φ : FormalCoordinate R) : φ.toPowerSeries ≠ 0

Over a nontrivial ring a formal coordinate is a nonzero power series.

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.instMul {R : Type u_1} [CommRing R] : Mul (FormalCoordinate R)

The product φ * ψ of formal coordinates is the composite φ ∘ ψ, the series φ (ψ).

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.instOne {R : Type u_1} [CommRing R] : One (FormalCoordinate R)

The identity coordinate X.

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.instInv {R : Type u_1} [CommRing R] : Inv (FormalCoordinate R)

The inverse of a formal coordinate is its compositional inverse.

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_mul {R : Type u_1} [CommRing R] (φ ψ : FormalCoordinate R) : (φ * ψ).toPowerSeries = PowerSeries.subst ψ.toPowerSeries φ.toPowerSeries

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_one {R : Type u_1} [CommRing R] : toPowerSeries 1 = PowerSeries.X

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_inv {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : φ⁻¹.toPowerSeries = φ.toPowerSeries.substInvOfIsUnit ⋯

theorem TauCeti.FormalCoordinate.subst_subst {R : Type u_1} [CommRing R] (φ ψ : FormalCoordinate R) (f : PowerSeries R) : PowerSeries.subst ψ.toPowerSeries (PowerSeries.subst φ.toPowerSeries f) = PowerSeries.subst (φ * ψ).toPowerSeries f

Substituting φ and then ψ is substituting the composite φ ∘ ψ = φ * ψ.

@[instance_reducible]

noncomputable instance TauCeti.FormalCoordinate.instGroup {R : Type u_1} [CommRing R] : Group (FormalCoordinate R)

Formal coordinates form a group under composition.

theorem TauCeti.FormalCoordinate.toPowerSeries_mul_inv {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : (φ * φ⁻¹).toPowerSeries = PowerSeries.X

A formal coordinate composed with its inverse is X.

theorem TauCeti.FormalCoordinate.toPowerSeries_inv_mul {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : (φ⁻¹ * φ).toPowerSeries = PowerSeries.X

The inverse of a formal coordinate composed with it is X.

theorem TauCeti.FormalCoordinate.hasSubst_subst {R : Type u_1} [CommRing R] {σ : Type u_2} {x : MvPowerSeries σ R} (φ : FormalCoordinate R) (hx : PowerSeries.HasSubst x) : PowerSeries.HasSubst (PowerSeries.subst x φ.toPowerSeries)

A formal coordinate evaluated at a substitutable series x is again substitutable.

theorem TauCeti.FormalCoordinate.subst_toPowerSeries_mul {R : Type u_1} [CommRing R] {σ : Type u_2} {x : MvPowerSeries σ R} (φ ψ : FormalCoordinate R) (hx : PowerSeries.HasSubst x) : PowerSeries.subst x (φ * ψ).toPowerSeries = PowerSeries.subst (PowerSeries.subst x ψ.toPowerSeries) φ.toPowerSeries

Evaluating the composite φ ∘ ψ at x is evaluating φ at ψ (x).

theorem TauCeti.FormalCoordinate.subst_subst_inv {R : Type u_1} [CommRing R] {σ : Type u_2} {x : MvPowerSeries σ R} (φ : FormalCoordinate R) (hx : PowerSeries.HasSubst x) : PowerSeries.subst (PowerSeries.subst x φ⁻¹.toPowerSeries) φ.toPowerSeries = x

φ (φ⁻¹ (x)) = x.

theorem TauCeti.FormalCoordinate.subst_inv_subst {R : Type u_1} [CommRing R] {σ : Type u_2} {x : MvPowerSeries σ R} (φ : FormalCoordinate R) (hx : PowerSeries.HasSubst x) : PowerSeries.subst (PowerSeries.subst x φ.toPowerSeries) φ⁻¹.toPowerSeries = x

φ⁻¹ (φ (x)) = x.

noncomputable def TauCeti.FormalCoordinate.linearCoeff {R : Type u_1} [CommRing R] : FormalCoordinate R →* Rˣ

The linear coefficient of a formal coordinate, as a homomorphism to the units of R.

@[simp]

theorem TauCeti.FormalCoordinate.val_linearCoeff {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : ↑(linearCoeff φ) = (PowerSeries.coeff 1) φ.toPowerSeries

noncomputable def TauCeti.FormalCoordinate.substAlgEquiv {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : PowerSeries R ≃ₐ[R] PowerSeries R

The substitution automorphism σ_φ : f ↦ f (φ) of R⟦X⟧, with inverse the substitution of the compositional inverse of φ.

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquiv_apply {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) (f : PowerSeries R) : φ.substAlgEquiv f = PowerSeries.subst φ.toPowerSeries f

theorem TauCeti.FormalCoordinate.substAlgEquiv_X {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : φ.substAlgEquiv PowerSeries.X = φ.toPowerSeries

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquiv_symm {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : φ.substAlgEquiv.symm = φ⁻¹.substAlgEquiv

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquiv_mul {R : Type u_1} [CommRing R] (φ ψ : FormalCoordinate R) : (φ * ψ).substAlgEquiv = ψ.substAlgEquiv * φ.substAlgEquiv

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

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquiv_one {R : Type u_1} [CommRing R] : substAlgEquiv 1 = 1

theorem TauCeti.FormalCoordinate.substAlgEquiv_injective {R : Type u_1} [CommRing R] : Function.Injective substAlgEquiv

A formal coordinate is determined by its substitution automorphism.

@[simp]

theorem TauCeti.FormalCoordinate.constantCoeff_subst_toPowerSeries {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) (f : PowerSeries R) : PowerSeries.constantCoeff (PowerSeries.subst φ.toPowerSeries f) = PowerSeries.constantCoeff f

Substitution by a formal coordinate preserves constant coefficients.

theorem TauCeti.FormalCoordinate.constantCoeff_substAlgEquiv {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) (f : PowerSeries R) : PowerSeries.constantCoeff (φ.substAlgEquiv f) = PowerSeries.constantCoeff f

Substitution automorphisms preserve constant coefficients: they fix the ideal (X) and induce the identity on R⟦X⟧ / (X) = R.

noncomputable def TauCeti.FormalCoordinate.substAlgEquivHom {R : Type u_1} [CommRing R] : FormalCoordinate R →* (PowerSeries R ≃ₐ[R] PowerSeries R)ᵐᵒᵖ

The map φ ↦ σ_φ from formal coordinates to the opposite of the automorphism group of R⟦X⟧. It is a homomorphism because σ_(φ ∘ ψ) = σ_ψ ∘ σ_φ.

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquivHom_apply {R : Type u_1} [CommRing R] (φ : FormalCoordinate R) : substAlgEquivHom φ = MulOpposite.op φ.substAlgEquiv

theorem TauCeti.FormalCoordinate.substAlgEquivHom_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑substAlgEquivHom

noncomputable def TauCeti.FormalCoordinate.map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : FormalCoordinate R →* FormalCoordinate S

Base change of formal coordinates along a ring homomorphism f : R →+* S, applying f to every coefficient. It is a group homomorphism since base change commutes with composition.

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (φ : FormalCoordinate R) : ((map f) φ).toPowerSeries = (PowerSeries.map f) φ.toPowerSeries

@[simp]

theorem TauCeti.FormalCoordinate.map_id {R : Type u_1} [CommRing R] : map (RingHom.id R) = MonoidHom.id (FormalCoordinate R)

Base change of formal coordinates along the identity changes nothing.

theorem TauCeti.FormalCoordinate.map_comp {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] (f : R →+* S) (g : S →+* T) (φ : FormalCoordinate R) : (map (g.comp f)) φ = (map g) ((map f) φ)

Successive base changes of a formal coordinate agree with base change along the composite.

theorem TauCeti.FormalCoordinate.map_substAlgEquiv {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (φ : FormalCoordinate R) (p : PowerSeries R) : (PowerSeries.map f) (φ.substAlgEquiv p) = ((map f) φ).substAlgEquiv ((PowerSeries.map f) p)

Substitution is natural in the coefficients: base change along f carries p (φ) to the substitution of the base-changed coordinate into the base-changed series.

noncomputable def TauCeti.FormalCoordinate.ofStrictCoeffs {R : Type u_1} [CommRing R] (b : ℕ+ → R) : FormalCoordinate R

The strict formal coordinate X + ∑_{i ≥ 1} bᵢ X^(i + 1) with coefficients b.

@[simp]

theorem TauCeti.FormalCoordinate.coeff_succ_ofStrictCoeffs {R : Type u_1} [CommRing R] (b : ℕ+ → R) (i : ℕ+) : (PowerSeries.coeff (↑i + 1)) (ofStrictCoeffs b).toPowerSeries = b i

@[simp]

theorem TauCeti.FormalCoordinate.coeff_one_ofStrictCoeffs {R : Type u_1} [CommRing R] (b : ℕ+ → R) : (PowerSeries.coeff 1) (ofStrictCoeffs b).toPowerSeries = 1

@[simp]

theorem TauCeti.FormalCoordinate.ofStrictCoeffs_zero {R : Type u_1} [CommRing R] : ofStrictCoeffs 0 = 1

The strict coordinate with all coefficients bᵢ = 0 is the identity coordinate X.

theorem TauCeti.FormalCoordinate.toPowerSeries_ofStrictCoeffs_single {R : Type u_1} [CommRing R] (n : ℕ+) (e : R) : (ofStrictCoeffs (Pi.single n e)).toPowerSeries = PowerSeries.X + PowerSeries.C e * PowerSeries.X ^ (↑n + 1)

The strict coordinate whose only nonzero coefficient is bₙ = e is X + e X^(n + 1).

theorem TauCeti.FormalCoordinate.inv_ofStrictCoeffs_single_of_mul_self_eq_zero {R : Type u_1} [CommRing R] (n : ℕ+) {e : R} (he : e * e = 0) : (ofStrictCoeffs (Pi.single n e))⁻¹ = ofStrictCoeffs (Pi.single n (-e))

If e² = 0, the inverse of X + e X^(n + 1) is X - e X^(n + 1).

theorem TauCeti.FormalCoordinate.ofStrictCoeffs_mem_ker_linearCoeff {R : Type u_1} [CommRing R] (b : ℕ+ → R) : ofStrictCoeffs b ∈ linearCoeff.ker

The coordinates X + ∑ bᵢ X^(i + 1) are strict: their linear coefficient is 1.

noncomputable def TauCeti.FormalCoordinate.strictCoeffsEquiv {R : Type u_1} [CommRing R] : (ℕ+ → R) ≃ ↥linearCoeff.ker

A strict formal coordinate, one with linear coefficient 1, is determined by the coefficients bᵢ of X^(i + 1), i ≥ 1, and every family of them occurs: strict coordinates are the series X + ∑ bᵢ X^(i + 1).

@[simp]

theorem TauCeti.FormalCoordinate.coe_strictCoeffsEquiv_apply {R : Type u_1} [CommRing R] (b : ℕ+ → R) : ↑(strictCoeffsEquiv b) = ofStrictCoeffs b

@[simp]

theorem TauCeti.FormalCoordinate.strictCoeffsEquiv_symm_apply {R : Type u_1} [CommRing R] (φ : ↥linearCoeff.ker) (i : ℕ+) : strictCoeffsEquiv.symm φ i = (PowerSeries.coeff (↑i + 1)) (↑φ).toPowerSeries

@[simp]

theorem TauCeti.FormalCoordinate.map_ofStrictCoeffs {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (b : ℕ+ → R) : (map f) (ofStrictCoeffs b) = ofStrictCoeffs (⇑f ∘ b)

Base change of X + ∑ bᵢ X^(i + 1) along f is X + ∑ f(bᵢ) X^(i + 1).

noncomputable def TauCeti.FormalCoordinate.homothety {R : Type u_1} [CommRing R] : Rˣ →* FormalCoordinate R

The homothety X ↦ u X by a unit u, as a formal coordinate. The homotheties split the linear coefficient (TauCeti.FormalCoordinate.linearCoeff_homothety).

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_homothety {R : Type u_1} [CommRing R] (u : Rˣ) : (homothety u).toPowerSeries = ↑u • PowerSeries.X

The homothety by u is the series u X.

@[simp]

theorem TauCeti.FormalCoordinate.linearCoeff_homothety {R : Type u_1} [CommRing R] (u : Rˣ) : linearCoeff (homothety u) = u

The linear coefficient of the homothety by u is u.

theorem TauCeti.FormalCoordinate.coeff_homothety_inv_mul_mul_homothety {R : Type u_1} [CommRing R] (u : Rˣ) (φ : FormalCoordinate R) (n : ℕ) : (PowerSeries.coeff n) (homothety u⁻¹ * φ * homothety u).toPowerSeries = ↑u⁻¹ * ↑u ^ n * (PowerSeries.coeff n) φ.toPowerSeries

Conjugating a formal coordinate φ by the homothety by u gives the coordinate u⁻¹ φ(u X), whose coefficient of Xⁿ is uⁿ⁻¹ times that of φ.

theorem TauCeti.FormalCoordinate.homothety_inv_mul_ofStrictCoeffs_mul_homothety {R : Type u_1} [CommRing R] (u : Rˣ) (b : ℕ+ → R) : homothety u⁻¹ * ofStrictCoeffs b * homothety u = ofStrictCoeffs fun (i : ℕ+) => ↑u ^ ↑i * b i

Conjugating the strict coordinate X + ∑ bᵢ X^(i + 1) by the homothety by u gives u⁻¹ φ(u X) = X + ∑ uⁱ bᵢ X^(i + 1).

noncomputable def TauCeti.FormalCoordinate.ofAlgEquiv {K : Type u_2} [Field K] (σ : PowerSeries K ≃ₐ[K] PowerSeries K) : FormalCoordinate K

Over a field, the formal coordinate σ X defined by an automorphism σ of K⟦X⟧.

@[simp]

theorem TauCeti.FormalCoordinate.toPowerSeries_ofAlgEquiv {K : Type u_2} [Field K] (σ : PowerSeries K ≃ₐ[K] PowerSeries K) : (ofAlgEquiv σ).toPowerSeries = σ PowerSeries.X

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquiv_ofAlgEquiv {K : Type u_2} [Field K] (σ : PowerSeries K ≃ₐ[K] PowerSeries K) : (ofAlgEquiv σ).substAlgEquiv = σ

Over a field, every automorphism of K⟦X⟧ is the substitution of its value at X.

@[simp]

theorem TauCeti.FormalCoordinate.ofAlgEquiv_substAlgEquiv {K : Type u_2} [Field K] (φ : FormalCoordinate K) : ofAlgEquiv φ.substAlgEquiv = φ

noncomputable def TauCeti.FormalCoordinate.substAlgEquivMulEquiv (K : Type u_2) [Field K] : FormalCoordinate K ≃* (PowerSeries K ≃ₐ[K] PowerSeries K)ᵐᵒᵖ

Over a field, φ ↦ σ_φ is an isomorphism between the group of formal coordinates and the opposite of the automorphism group of K⟦X⟧, with inverse σ ↦ σ X.

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquivMulEquiv_apply {K : Type u_2} [Field K] (φ : FormalCoordinate K) : (substAlgEquivMulEquiv K) φ = MulOpposite.op φ.substAlgEquiv

@[simp]

theorem TauCeti.FormalCoordinate.substAlgEquivMulEquiv_symm_apply {K : Type u_2} [Field K] (σ : (PowerSeries K ≃ₐ[K] PowerSeries K)ᵐᵒᵖ) : (substAlgEquivMulEquiv K).symm σ = ofAlgEquiv (MulOpposite.unop σ)