Documentation

TauCeti.RingTheory.FormalGroup.AddInv

The formal inverse of a formal group law #

Let F(X, Y) be a one-dimensional formal group law over a commutative ring R. Its formal inverse is the power series i(X) with zero constant coefficient such that

F(i(X), X) = 0 = F(X, i(X)).

It exists over every commutative ring and is unique. Writing F(X, Y) = X + Y + โ‹ฏ, the coefficient of Xโฟ in F(f(X), X) for a series f without constant term depends only on the coefficients of f up to degree n, and the coefficient of Xโฟ in f enters it with the linear coefficient 1 of F in its first variable (PowerSeries.coeff_subst_update_add_X_pow_mul). So the coefficients of i are determined one degree at a time, each killing the next coefficient of F(i(X), X).

Substituting into the formal inverse negates the power-series points of F: for x in Mathlib's monoid F.Point ฯƒ of series with nilpotent constant coefficient, -x = i(x). This makes F.Point ฯƒ a group, commutative when F is, and from the group laws the formal inverse is also a right inverse, is unique on either side, and is an involution, i(i(X)) = X.

Main definitions #

Main results #

Implementation notes #

The name addInvX and the group structure on F.Point ฯƒ follow the design proposed by Wenrong Zou in Mathlib PR #36167, which defines the inverse there through a recursion on its coefficients. Here i is instead the limit of the polynomial approximations of each degree, and the degree-by-degree step is the general perturbation lemma PowerSeries.coeff_subst_update_add_X_pow_mul.

References #

source
noncomputable def FormalGroup.tautologicalPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) :
F.Point Unit

The tautological point X of F, with values in the power series ring RโŸฆXโŸง.

Instances For
    source
    @[simp]
    theorem FormalGroup.val_tautologicalPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) :
    โ†‘F.tautologicalPoint = PowerSeries.X
    source
    theorem FormalGroup.coeff_subst_add_X_pow_mul_X {R : Type u_1} [CommRing R] (F : FormalGroup R) {f : PowerSeries R} (hf : PowerSeries.constantCoeff f = 0) (r : PowerSeries R) {m n : โ„•} (hm : m โ‰  0) (hn : n โ‰ค m) :
    (PowerSeries.coeff n) (MvPowerSeries.subst ![f + PowerSeries.X ^ m * r, PowerSeries.X] F.toPowerSeries) = (PowerSeries.coeff n) (MvPowerSeries.subst ![f, PowerSeries.X] F.toPowerSeries) + if n = m then PowerSeries.constantCoeff r else 0

    Perturbing f by X ^ m * r in F(f(X), X) changes the coefficient of degree m by r(0), and no coefficient of lower degree.

    source
    noncomputable def FormalGroup.addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) :
    PowerSeries R

    The formal inverse of a formal group law F: the power series i(X) with F(i(X), X) = 0 (FormalGroup.subst_addInvX_X_eq_zero). It is the negation of the tautological point X in the group F.Point Unit of power-series points of F.

    Instances For
      source
      @[simp]
      theorem FormalGroup.constantCoeff_addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      PowerSeries.constantCoeff F.addInvX = 0
      source
      @[simp]
      theorem FormalGroup.coeff_one_addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      (PowerSeries.coeff 1) F.addInvX = -1

      The formal inverse has linear coefficient -1: i(X) = -X + โ‹ฏ.

      source
      theorem FormalGroup.hasSubst_addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      PowerSeries.HasSubst F.addInvX

      The formal inverse can be substituted into power series.

      source
      @[simp]
      theorem FormalGroup.subst_addInvX_X_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      MvPowerSeries.subst ![F.addInvX, PowerSeries.X] F.toPowerSeries = 0

      The formal inverse is a left inverse: F(i(X), X) = 0.

      source
      theorem FormalGroup.coeff_succ_addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : โ„•) :
      (PowerSeries.coeff (n + 1)) F.addInvX = -(PowerSeries.coeff (n + 1)) (MvPowerSeries.subst ![โˆ‘ i โˆˆ Finset.range (n + 1), PowerSeries.C ((PowerSeries.coeff i) F.addInvX) * PowerSeries.X ^ i, PowerSeries.X] F.toPowerSeries)

      Each coefficient of the inverse coordinate cancels the error left by the preceding coefficients, so its construction requires no division in the coefficient ring.

      source
      theorem FormalGroup.hasSubst_subst_pair {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {x y : MvPowerSeries ฯƒ R} (hx : PowerSeries.HasSubst x) (hy : PowerSeries.HasSubst y) :
      PowerSeries.HasSubst (MvPowerSeries.subst ![x, y] F.toPowerSeries)

      The value F(x, y) of a formal group law at substitutable x, y is substitutable: it is the sum of the power-series points x and y of F.

      source
      @[instance_reducible]
      noncomputable instance FormalGroup.instNegPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} :
      Neg (F.Point ฯƒ)

      Negation of power-series points of F: -x = i(x), substituting x into the formal inverse.

      source
      @[simp]
      theorem FormalGroup.neg_apply {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {x : F.Point ฯƒ} :
      โ†‘(-x) = PowerSeries.subst (โ†‘x) F.addInvX
      source
      @[instance_reducible]
      noncomputable instance FormalGroup.instAddGroupPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} :
      AddGroup (F.Point ฯƒ)

      The power-series points of a formal group law form a group under x + y = F(x, y).

      source
      @[instance_reducible]
      noncomputable instance FormalGroup.instAddCommGroupPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} [F.IsComm] :
      AddCommGroup (F.Point ฯƒ)
      source
      theorem FormalGroup.val_neg_tautologicalPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      โ†‘(-F.tautologicalPoint) = F.addInvX

      The formal inverse is the negation of the tautological point: -X = i(X).

      source
      @[simp]
      theorem FormalGroup.subst_addInvX_self_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {f : MvPowerSeries ฯƒ R} (hf : PowerSeries.HasSubst f) :
      MvPowerSeries.subst ![PowerSeries.subst f F.addInvX, f] F.toPowerSeries = 0

      Substituting any native point into the inverse coordinate gives its left inverse.

      source
      theorem FormalGroup.eq_subst_addInvX_iff_subst_left_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {f g : MvPowerSeries ฯƒ R} (hf : PowerSeries.HasSubst f) (hg : PowerSeries.HasSubst g) :
      g = PowerSeries.subst f F.addInvX โ†” MvPowerSeries.subst ![g, f] F.toPowerSeries = 0

      A left inverse of a native point is obtained by substituting it into addInvX.

      source
      @[simp]
      theorem FormalGroup.subst_self_addInvX_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {f : MvPowerSeries ฯƒ R} (hf : PowerSeries.HasSubst f) :
      MvPowerSeries.subst ![f, PowerSeries.subst f F.addInvX] F.toPowerSeries = 0

      The inverse coordinate gives right inverses too, without assuming commutativity of F.

      source
      theorem FormalGroup.eq_subst_addInvX_iff_subst_right_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {ฯƒ : Type u_3} {f g : MvPowerSeries ฯƒ R} (hf : PowerSeries.HasSubst f) (hg : PowerSeries.HasSubst g) :
      g = PowerSeries.subst f F.addInvX โ†” MvPowerSeries.subst ![f, g] F.toPowerSeries = 0

      A right inverse of a native point is obtained by substituting it into addInvX.

      source
      @[simp]
      theorem FormalGroup.subst_X_addInvX_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      MvPowerSeries.subst ![PowerSeries.X, F.addInvX] F.toPowerSeries = 0

      The formal inverse is a right inverse: F(X, i(X)) = 0.

      source
      theorem FormalGroup.eq_addInvX_iff_subst_left_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {f : PowerSeries R} (hf : PowerSeries.HasSubst f) :
      f = F.addInvX โ†” MvPowerSeries.subst ![f, PowerSeries.X] F.toPowerSeries = 0

      The formal inverse is the only left inverse of X: a substitutable f satisfies F(f(X), X) = 0 exactly when f = i.

      source
      theorem FormalGroup.eq_addInvX_iff_subst_right_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {f : PowerSeries R} (hf : PowerSeries.HasSubst f) :
      f = F.addInvX โ†” MvPowerSeries.subst ![PowerSeries.X, f] F.toPowerSeries = 0

      The formal inverse is the only right inverse of X: a substitutable f satisfies F(X, f(X)) = 0 exactly when f = i.

      source
      @[simp]
      theorem FormalGroup.subst_addInvX_addInvX {R : Type u_1} [CommRing R] (F : FormalGroup R) :
      PowerSeries.subst F.addInvX F.addInvX = PowerSeries.X

      The formal inverse is an involution: i(i(X)) = X.

      source
      @[simp]
      theorem FormalGroup.map_addInvX {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) (ฯ† : R โ†’+* S) :
      (PowerSeries.map ฯ†) F.addInvX = (F.map ฯ†).addInvX

      The formal inverse commutes with base change of the coefficient ring.

      source
      @[simp]
      theorem FormalGroup.addInvX_๐”พโ‚ {R : Type u_1} [CommRing R] :
      ๐”พโ‚.addInvX = -PowerSeries.X

      The formal inverse of the additive formal group law X + Y is -X.

      source
      @[simp]
      theorem FormalGroup.addInvX_๐”พโ‚˜ {R : Type u_1} [CommRing R] :
      ๐”พโ‚˜.addInvX = PowerSeries.X * PowerSeries.invUnitsSub (-1)

      The formal inverse of the multiplicative formal group law X + Y + XY is -X / (1 + X) = X * (-1 - X)โปยน.