The Hopf algebroid (L, L[b₁, b₂, …]) of strict coordinate changes

Write Γ = L[b₁, b₂, …] = MvPolynomial ℕ+ LazardRing. Ring homomorphisms Γ →+* R classify pairs (F, φ) of a commutative formal group law F over R and a strict coordinate φ = X + ∑ bᵢ X^(i + 1), that is, strict isomorphisms φ : F → φ • F (TauCeti.LazardRing.coordinateChangeLift). The source and target of φ are classified by the left unit η_L = C and the right unit η_R = TauCeti.LazardRing.rightUnit, and the identity isomorphisms by the counit ε. This file constructs the remaining structure maps, which classify composition and inversion of strict isomorphisms, and proves the Hopf algebroid equations: the pair (L, Γ) is a cogroupoid object in commutative rings, corepresenting the groupoid of commutative formal group laws and their strict isomorphisms.

Composable pairs F → φ • F → ψ • (φ • F) are classified by the pushout Γ ⊗_L Γ of η_R on the left factor and η_L on the right factor. As Γ is a polynomial ring over L through η_L, this pushout is the polynomial ring Γ[b₁', b₂', …] = MvPolynomial ℕ+ Γ, with left factor C and right factor MvPolynomial.map η_R; TauCeti.LazardRing.tensorLift is its universal property. The coproduct Δ : Γ → Γ ⊗_L Γ classifies the composite ψ * φ = ψ ∘ φ, and the conjugation c : Γ → Γ classifies the inverse φ⁻¹ : φ • F → F.

The equations are proved by comparing classified data: a ring homomorphism out of Γ is determined by its restriction to L and by its base change of the universal strict coordinate (TauCeti.FormalCoordinate.ringHom_ext_universalStrictCoordinate), and then each equation is a groupoid law in the group of strict coordinates. In the tensor model, the composite μ ∘ (f ⊗ g) : Γ ⊗_L Γ → R of a tensor product of maps with multiplication is tensorLift (f, g).

Main definitions

• TauCeti.LazardRing.tensorLift: the universal property of Γ ⊗_L Γ = MvPolynomial ℕ+ Γ as the pushout of η_R and η_L.
• TauCeti.LazardRing.coproduct: the coproduct Δ : Γ →+* Γ ⊗_L Γ.
• TauCeti.LazardRing.conjugation: the conjugation c : Γ →+* Γ.

Main results

• TauCeti.LazardRing.map_comp_coproduct_universalStrictCoordinate, TauCeti.LazardRing.comp_coproduct_comp_C: the coproduct classifies the composite of a composable pair of strict isomorphisms.
• TauCeti.LazardRing.coproduct_comp_C, TauCeti.LazardRing.coproduct_comp_rightUnit: Δ η_L = (η_L ⊗ 1) η_L and Δ η_R = (1 ⊗ η_R) η_R.
• TauCeti.LazardRing.tensorLift_counit_id_comp_coproduct, TauCeti.LazardRing.tensorLift_id_counit_comp_coproduct: (ε ⊗ id) Δ = id = (id ⊗ ε) Δ.
• TauCeti.LazardRing.coproduct_coassoc: coassociativity, (Δ ⊗ id) Δ = (id ⊗ Δ) Δ.
• TauCeti.LazardRing.conjugation_comp_C, TauCeti.LazardRing.conjugation_comp_rightUnit, TauCeti.LazardRing.conjugation_comp_conjugation: c η_L = η_R, c η_R = η_L and c c = id.
• TauCeti.LazardRing.counit_comp_conjugation: ε c = ε.
• TauCeti.LazardRing.tensorLift_conjugation_id_comp_coproduct, TauCeti.LazardRing.tensorLift_id_conjugation_comp_coproduct: the antipode equations μ (c ⊗ id) Δ = η_R ε and μ (id ⊗ c) Δ = η_L ε.
• TauCeti.LazardRing.map_rightUnit_heightIdeal: the height ideals I_n of the Lazard ring (FormalGroup.heightIdeal) are invariant ideals: η_R(I_n) Γ = η_L(I_n) Γ.

References

• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A1.1 (Hopf algebroids) and A2.1 (the Hopf algebroid (L, LB)).
• J. Lurie, Chromatic Homotopy Theory (Harvard lecture notes, 2010), Lecture 3.

The tensor square Γ ⊗_L Γ

noncomputable def TauCeti.LazardRing.tensorLift {R : Type u_1} [CommRing R] : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C } ≃ (MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R)

The universal property of Γ ⊗_L Γ, for Γ = L[b₁, b₂, …]: ring homomorphisms out of Γ[b₁', b₂', …] = MvPolynomial ℕ+ Γ correspond to pairs (f, g) of ring homomorphisms out of Γ with f ∘ η_R = g ∘ η_L, by restriction along the left factor C and the right factor MvPolynomial.map η_R. Thus MvPolynomial ℕ+ Γ is the pushout Γ ⊗_L Γ of the right unit on the left factor and the left unit on the right factor, and its homomorphisms to R classify composable pairs F → φ • F → ψ • (φ • F) of strict isomorphisms.

@[simp]

theorem TauCeti.LazardRing.tensorLift_symm_apply_fst {R : Type u_1} [CommRing R] (k : MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R) : (↑(tensorLift.symm k)).1 = k.comp MvPolynomial.C

The left component of the pair classified by k : Γ ⊗_L Γ →+* R is its restriction along the left factor C.

@[simp]

theorem TauCeti.LazardRing.tensorLift_symm_apply_snd {R : Type u_1} [CommRing R] (k : MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R) : (↑(tensorLift.symm k)).2 = k.comp (MvPolynomial.map rightUnit)

The right component of the pair classified by k : Γ ⊗_L Γ →+* R is its restriction along the right factor MvPolynomial.map η_R.

@[simp]

theorem TauCeti.LazardRing.tensorLift_comp_C {R : Type u_1} [CommRing R] (p : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C }) : (tensorLift p).comp MvPolynomial.C = (↑p).1

tensorLift (f, g) restricts to f on the left factor.

@[simp]

theorem TauCeti.LazardRing.tensorLift_comp_map_rightUnit {R : Type u_1} [CommRing R] (p : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C }) : (tensorLift p).comp (MvPolynomial.map rightUnit) = (↑p).2

tensorLift (f, g) restricts to g on the right factor.

@[simp]

theorem TauCeti.LazardRing.tensorLift_C {R : Type u_1} [CommRing R] (p : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C }) (x : MvPolynomial ℕ+ LazardRing) : (tensorLift p) (MvPolynomial.C x) = (↑p).1 x

tensorLift (f, g) agrees with f on the left factor.

@[simp]

theorem TauCeti.LazardRing.tensorLift_map_rightUnit {R : Type u_1} [CommRing R] (p : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C }) (x : MvPolynomial ℕ+ LazardRing) : (tensorLift p) ((MvPolynomial.map rightUnit) x) = (↑p).2 x

tensorLift (f, g) agrees with g on the right factor.

@[simp]

theorem TauCeti.LazardRing.tensorLift_X {R : Type u_1} [CommRing R] (p : { p : (MvPolynomial ℕ+ LazardRing →+* R) × (MvPolynomial ℕ+ LazardRing →+* R) // p.1.comp rightUnit = p.2.comp MvPolynomial.C }) (i : ℕ+) : (tensorLift p) (MvPolynomial.X i) = (↑p).2 (MvPolynomial.X i)

tensorLift (f, g) agrees with g on the generators of the right factor.

theorem TauCeti.LazardRing.tensor_ringHom_ext {R : Type u_1} [CommRing R] {k k' : MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R} (h₁ : k.comp MvPolynomial.C = k'.comp MvPolynomial.C) (h₂ : k.comp (MvPolynomial.map rightUnit) = k'.comp (MvPolynomial.map rightUnit)) : k = k'

A ring homomorphism out of Γ ⊗_L Γ is determined by its restrictions to both factors.

The coproduct

noncomputable def TauCeti.LazardRing.coproduct : MvPolynomial ℕ+ LazardRing →+* MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing)

The coproduct Δ : Γ →+* Γ ⊗_L Γ, classifying the composite ψ * φ = ψ ∘ φ of the universal composable pair F → φ • F → ψ • (φ • F) of strict isomorphisms: F and φ come from the left factor and ψ from the right factor.

@[simp]

theorem TauCeti.LazardRing.coproduct_comp_C : coproduct.comp MvPolynomial.C = MvPolynomial.C.comp MvPolynomial.C

Δ η_L = (η_L ⊗ 1) η_L: the source of a composite is the source of its first factor.

@[simp]

theorem TauCeti.LazardRing.coproduct_C (r : LazardRing) : coproduct (MvPolynomial.C r) = MvPolynomial.C (MvPolynomial.C r)

The coproduct agrees with the left factor on L.

@[simp]

theorem TauCeti.LazardRing.map_coproduct_universalStrictCoordinate : (FormalCoordinate.map coproduct) FormalCoordinate.universalStrictCoordinate = (FormalCoordinate.map (MvPolynomial.map rightUnit)) FormalCoordinate.universalStrictCoordinate * (FormalCoordinate.map MvPolynomial.C) FormalCoordinate.universalStrictCoordinate

The coproduct sends the universal strict coordinate to the composite ψ * φ of the universal strict coordinates φ of the left factor and ψ of the right factor.

theorem TauCeti.LazardRing.map_comp_coproduct_universalStrictCoordinate {R : Type u_1} [CommRing R] (k : MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R) : (FormalCoordinate.map (k.comp coproduct)) FormalCoordinate.universalStrictCoordinate = (FormalCoordinate.map (k.comp (MvPolynomial.map rightUnit))) FormalCoordinate.universalStrictCoordinate * (FormalCoordinate.map (k.comp MvPolynomial.C)) FormalCoordinate.universalStrictCoordinate

The coproduct classifies composition: if k : Γ ⊗_L Γ →+* R classifies the composable pair F → φ • F → ψ • (φ • F), then k ∘ Δ classifies the composite ψ * φ. This is its coordinate; TauCeti.LazardRing.comp_coproduct_comp_C is its source.

theorem TauCeti.LazardRing.comp_coproduct_comp_C {R : Type u_1} [CommRing R] (k : MvPolynomial ℕ+ (MvPolynomial ℕ+ LazardRing) →+* R) : (k.comp coproduct).comp MvPolynomial.C = (k.comp MvPolynomial.C).comp MvPolynomial.C

The source of the composite classified by k ∘ Δ is the source classified by the left factor of k.

@[simp]

theorem TauCeti.LazardRing.coproduct_comp_rightUnit : coproduct.comp rightUnit = (MvPolynomial.map rightUnit).comp rightUnit

Δ η_R = (1 ⊗ η_R) η_R: the target of a composite is the target of its second factor.

@[simp]

theorem TauCeti.LazardRing.coproduct_rightUnit (r : LazardRing) : coproduct (rightUnit r) = (MvPolynomial.map rightUnit) (rightUnit r)

The coproduct agrees with the right factor on the image of the right unit.

theorem TauCeti.LazardRing.tensorLift_counit_id_comp_coproduct : (tensorLift ⟨(MvPolynomial.C.comp counit, RingHom.id (MvPolynomial ℕ+ LazardRing)), tensorLift_counit_id_comp_coproduct._proof_1⟩).comp coproduct = RingHom.id (MvPolynomial ℕ+ LazardRing)

The left counit law (ε ⊗ id) Δ = id: composing with an identity on the left does nothing. Here ε ⊗ id is tensorLift (η_L ε, id).

theorem TauCeti.LazardRing.tensorLift_id_counit_comp_coproduct : (tensorLift ⟨(RingHom.id (MvPolynomial ℕ+ LazardRing), rightUnit.comp counit), tensorLift_id_counit_comp_coproduct._proof_1⟩).comp coproduct = RingHom.id (MvPolynomial ℕ+ LazardRing)

The right counit law (id ⊗ ε) Δ = id: composing with an identity on the right does nothing. Here id ⊗ ε is tensorLift (id, η_R ε).

theorem TauCeti.LazardRing.coproduct_coassoc : (tensorLift ⟨(MvPolynomial.C.comp coproduct, MvPolynomial.map ((MvPolynomial.map rightUnit).comp rightUnit)), ⋯⟩).comp coproduct = (tensorLift ⟨(MvPolynomial.C.comp MvPolynomial.C, (MvPolynomial.map (MvPolynomial.map rightUnit)).comp coproduct), ⋯⟩).comp coproduct

Coassociativity (Δ ⊗ id) Δ = (id ⊗ Δ) Δ of the coproduct: composition of strict isomorphisms is associative. Both sides take values in the triple tensor product Γ ⊗_L Γ ⊗_L Γ = MvPolynomial ℕ+ (Γ ⊗_L Γ), the pushout of Γ ⊗_L Γ along the target of its right factor and of Γ along η_L, whose three factors are C ∘ C, C ∘ MvPolynomial.map η_R and MvPolynomial.map (MvPolynomial.map η_R ∘ η_R). In it, Δ ⊗ id is tensorLift (C ∘ Δ, ι₃) with ι₃ the third factor, and id ⊗ Δ is tensorLift (C ∘ C, ι₂₃ ∘ Δ) with ι₂₃ = MvPolynomial.map (MvPolynomial.map η_R) the inclusion of the last two factors.

The conjugation

noncomputable def TauCeti.LazardRing.conjugation : MvPolynomial ℕ+ LazardRing →+* MvPolynomial ℕ+ LazardRing

The conjugation c : Γ →+* Γ, classifying the inverse φ⁻¹ : φ • F → F of the universal strict isomorphism φ : F → φ • F.

@[simp]

theorem TauCeti.LazardRing.conjugation_comp_C : conjugation.comp MvPolynomial.C = rightUnit

c η_L = η_R: the source of the inverse is the target.

@[simp]

theorem TauCeti.LazardRing.conjugation_C (r : LazardRing) : conjugation (MvPolynomial.C r) = rightUnit r

The conjugation agrees with the right unit on L.

@[simp]

theorem TauCeti.LazardRing.map_conjugation_universalStrictCoordinate : (FormalCoordinate.map conjugation) FormalCoordinate.universalStrictCoordinate = FormalCoordinate.universalStrictCoordinate⁻¹

The conjugation sends the universal strict coordinate to its inverse.

@[simp]

theorem TauCeti.LazardRing.conjugation_comp_rightUnit : conjugation.comp rightUnit = MvPolynomial.C

c η_R = η_L: the target of the inverse is the source.

@[simp]

theorem TauCeti.LazardRing.conjugation_rightUnit (r : LazardRing) : conjugation (rightUnit r) = MvPolynomial.C r

The conjugation agrees with the left unit on the image of the right unit.

@[simp]

theorem TauCeti.LazardRing.conjugation_comp_conjugation : conjugation.comp conjugation = RingHom.id (MvPolynomial ℕ+ LazardRing)

c c = id: the inverse of the inverse is the original strict isomorphism.

@[simp]

theorem TauCeti.LazardRing.conjugation_conjugation (x : MvPolynomial ℕ+ LazardRing) : conjugation (conjugation x) = x

The conjugation is an involution.

@[simp]

theorem TauCeti.LazardRing.counit_comp_conjugation : counit.comp conjugation = counit

ε c = ε: the inverse of an identity is an identity.

@[simp]

theorem TauCeti.LazardRing.counit_conjugation (x : MvPolynomial ℕ+ LazardRing) : counit (conjugation x) = counit x

The counit is invariant under the conjugation.

theorem TauCeti.LazardRing.tensorLift_conjugation_id_comp_coproduct : (tensorLift ⟨(conjugation, RingHom.id (MvPolynomial ℕ+ LazardRing)), tensorLift_conjugation_id_comp_coproduct._proof_1⟩).comp coproduct = rightUnit.comp counit

The left antipode equation μ (c ⊗ id) Δ = η_R ε: composing the inverse of a strict isomorphism with it gives the identity of its target. Here μ (c ⊗ id) is tensorLift (c, id).

theorem TauCeti.LazardRing.tensorLift_id_conjugation_comp_coproduct : (tensorLift ⟨(RingHom.id (MvPolynomial ℕ+ LazardRing), conjugation), tensorLift_id_conjugation_comp_coproduct._proof_1⟩).comp coproduct = MvPolynomial.C.comp counit

The right antipode equation μ (id ⊗ c) Δ = η_L ε: composing a strict isomorphism with its inverse gives the identity of its source. Here μ (id ⊗ c) is tensorLift (id, c).

Invariant ideals

theorem TauCeti.LazardRing.map_rightUnit_heightIdeal (p n : ℕ) : Ideal.map rightUnit (formalGroup.heightIdeal p n) = Ideal.map MvPolynomial.C (formalGroup.heightIdeal p n)

The height ideals of the Lazard ring are invariant. Their extensions to the ring L[b₁, b₂, …] of strict coordinate changes along the left unit η_L = C and the right unit η_R agree.