Documentation

TauCeti.RingTheory.PowerSeries.Coordinate.Universal

The universal strict coordinate #

For a commutative ring A, the strict formal coordinate

X + ∑_{i ≥ 1} bᵢ X^(i + 1)

over the polynomial ring A[b₁, b₂, …] = MvPolynomial ℕ+ A, whose coefficients are the variables, is universal among strict coordinates over A-algebras: a ring homomorphism A[b₁, b₂, …] →+* R is the same as a ring homomorphism A →+* R together with a strict coordinate over R, and it specializes the universal strict coordinate to that coordinate.

Taking for A a ring classifying formal group laws of some kind, such as the Lazard ring, this makes the strict isomorphisms between such formal group laws representable by A[b₁, b₂, …].

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.FormalCoordinate.universalStrictCoordinate {A : Type u_1} [CommRing A] :
FormalCoordinate (MvPolynomial ℕ+ A)

The universal strict coordinate X + ∑_{i ≥ 1} bᵢ X^(i + 1) over A[b₁, b₂, …], whose coefficients are the variables bᵢ.

Instances For
    source
    @[simp]
    theorem TauCeti.FormalCoordinate.coeff_succ_universalStrictCoordinate {A : Type u_1} [CommRing A] (i : ℕ+) :
    (PowerSeries.coeff (↑i + 1)) universalStrictCoordinate.toPowerSeries = MvPolynomial.X i

    The strict coordinate universalStrictCoordinate has the variable bᵢ as its coefficient of X^(i + 1).

    source
    theorem TauCeti.FormalCoordinate.map_universalStrictCoordinate {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (f : MvPolynomial ℕ+ A →+* R) :
    (map f) universalStrictCoordinate = ofStrictCoeffs (⇑f ∘ MvPolynomial.X)

    The base change of the universal strict coordinate along f is the strict coordinate X + ∑ f(bᵢ) X^(i + 1).

    source
    theorem TauCeti.FormalCoordinate.map_universalStrictCoordinate_mem_ker {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (f : MvPolynomial ℕ+ A →+* R) :
    (map f) universalStrictCoordinate ∈ linearCoeff.ker

    Base change of the universal strict coordinate is strict.

    source
    @[simp]
    theorem TauCeti.FormalCoordinate.map_map_universalStrictCoordinate {A : Type u_1} [CommRing A] {B : Type u_3} [CommRing B] (f : A →+* B) :
    (map (MvPolynomial.map f)) universalStrictCoordinate = universalStrictCoordinate

    Applying f : A →+* B to the coefficients of A[b₁, b₂, …] carries the universal strict coordinate over A[b₁, b₂, …] to the universal strict coordinate over B[b₁, b₂, …].

    source
    theorem TauCeti.FormalCoordinate.ringHom_ext_universalStrictCoordinate {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] {f g : MvPolynomial ℕ+ A →+* R} (hC : f.comp MvPolynomial.C = g.comp MvPolynomial.C) (hφ : (map f) universalStrictCoordinate = (map g) universalStrictCoordinate) :
    f = g

    A ring homomorphism out of A[b₁, b₂, …] is determined by its restriction to A and by its base change of the universal strict coordinate.

    source
    noncomputable def TauCeti.FormalCoordinate.strictLift {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] :
    (A →+* R) × ↥linearCoeff.ker ≃ (MvPolynomial ℕ+ A →+* R)

    A[b₁, b₂, …] represents strict coordinates over A-algebras: pairs of a ring homomorphism f : A →+* R and a strict coordinate φ over R correspond to ring homomorphisms A[b₁, b₂, …] →+* R. The homomorphism attached to (f, φ) restricts to f and sends bᵢ to the coefficient of X^(i + 1) in φ.

    Instances For
      source
      @[simp]
      theorem TauCeti.FormalCoordinate.strictLift_symm_apply_fst {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (f : MvPolynomial ℕ+ A →+* R) :
      (strictLift.symm f).1 = f.comp MvPolynomial.C

      The ring homomorphism out of A attached to f : A[b₁, b₂, …] →+* R is its restriction.

      source
      @[simp]
      theorem TauCeti.FormalCoordinate.strictLift_symm_apply_snd {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (f : MvPolynomial ℕ+ A →+* R) :
      (strictLift.symm f).2 = strictCoeffsEquiv (⇑f ∘ MvPolynomial.X)

      The strict coordinate attached to f : A[b₁, b₂, …] →+* R has coefficients f (bᵢ).

      source
      @[simp]
      theorem TauCeti.FormalCoordinate.strictLift_comp_C {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (p : (A →+* R) × ↥linearCoeff.ker) :
      (strictLift p).comp MvPolynomial.C = p.1

      The homomorphism attached to (f, φ) restricts along C to f.

      source
      @[simp]
      theorem TauCeti.FormalCoordinate.strictLift_C {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (p : (A →+* R) × ↥linearCoeff.ker) (r : A) :
      (strictLift p) (MvPolynomial.C r) = p.1 r

      The homomorphism attached to (f, φ) agrees with f on constants.

      source
      @[simp]
      theorem TauCeti.FormalCoordinate.strictLift_X {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (p : (A →+* R) × ↥linearCoeff.ker) (i : ℕ+) :
      (strictLift p) (MvPolynomial.X i) = (PowerSeries.coeff (↑i + 1)) (↑p.2).toPowerSeries

      The homomorphism attached to (f, φ) sends bᵢ to the coefficient of X^(i + 1) in φ.

      source
      @[simp]
      theorem TauCeti.FormalCoordinate.map_strictLift_universalStrictCoordinate {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] (p : (A →+* R) × ↥linearCoeff.ker) :
      (map (strictLift p)) universalStrictCoordinate = ↑p.2

      The homomorphism attached to (f, φ) specializes the universal strict coordinate to φ.