Homomorphisms and isomorphisms of formal group laws

A homomorphism is a power series with zero constant term carrying one formal group law to another. Composition is substitution. An isomorphism carries a specified inverse homomorphism; it is strict when its linear coefficient is one. These maps act on the native power-series points, including points with nilpotent, not necessarily zero, constant coefficient.

The homomorphism defect f(F(X, Y)) - G(f(X), f(Y)) (FormalGroup.homDefect) of a power series f measures how far f is from a homomorphism: it vanishes exactly for homomorphisms (TauCeti.FormalGroupHom.homDefect_toPowerSeries, TauCeti.FormalGroupHom.ofHomDefectEqZero). At substitutable x, y the defect is f(F(x, y)) - G(f(x), f(y)) (FormalGroup.subst_homDefect); in particular it is f(F(X, Y)) - G(f(X), f(Y)) (FormalGroup.homDefect_eq_sub_subst_pair). The defect of X is the difference F - G (FormalGroup.homDefect_X). Towards the additive formal group law the defect is additive in f (FormalGroup.homDefect_𝔾ₐ_sub) and vanishes to the order of f (FormalGroup.le_order_homDefect_𝔾ₐ). Towards an arbitrary formal group law, the defects of two series with zero constant term that agree below degree n agree below degree n (FormalGroup.le_order_homDefect_sub), and replacing f by f + c Xⁿ changes the defect in degree n by c ((X + Y)ⁿ - Xⁿ - Yⁿ) (FormalGroup.homogeneousComponent_homDefect_add_sub).

Base change along a ring homomorphism φ : R →+* S applies φ to the coefficients of the series: TauCeti.FormalGroupHom.map and TauCeti.FormalGroupIso.map carry homomorphisms and isomorphisms between F and G to ones between F.map φ and G.map φ, compatibly with identities, composition, inverses and strictness. Base change along the identity ring homomorphism does nothing, and successive base changes agree with base change along the composite.

The bundles TauCeti.FormalGroupHom, TauCeti.FormalGroupIso, and TauCeti.FormalGroupIso.IsStrict are adapted from Wenrong Zou's Mathlib PR #38213 (https://github.com/leanprover-community/mathlib4/pull/38213). The action on points here uses Mathlib's native FormalGroup.Point carrier and formal substitution, not evaluation in an arbitrary topological algebra.

noncomputable def FormalGroup.homDefect {R : Type u_1} [CommRing R] (F G : FormalGroup R) (f : PowerSeries R) : MvPowerSeries (Fin 2) R

The homomorphism defect f(F(X, Y)) - G(f(X), f(Y)) of a power series f with respect to formal group laws F and G. It vanishes exactly when f satisfies the homomorphism equation (FormalGroup.homDefect_eq_zero_iff), and its order measures to which degree f is a homomorphism from F to G.

theorem FormalGroup.homDefect_def {R : Type u_1} [CommRing R] (F G : FormalGroup R) (f : PowerSeries R) : F.homDefect G f = PowerSeries.subst F.toPowerSeries f - MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) f) G.toPowerSeries

Unfold the homomorphism defect.

theorem FormalGroup.homDefect_eq_zero_iff {R : Type u_1} [CommRing R] (F G : FormalGroup R) {f : PowerSeries R} : F.homDefect G f = 0 ↔ PowerSeries.subst F.toPowerSeries f = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) f) G.toPowerSeries

The homomorphism defect vanishes exactly when f satisfies the homomorphism equation.

theorem FormalGroup.subst_homDefect {R : Type u_1} [CommRing R] (F G : FormalGroup R) {σ : Type u_2} {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) {x y : MvPowerSeries σ R} (hx : PowerSeries.HasSubst x) (hy : PowerSeries.HasSubst y) : MvPowerSeries.subst ![x, y] (F.homDefect G g) = PowerSeries.subst (MvPowerSeries.subst ![x, y] F.toPowerSeries) g - MvPowerSeries.subst ![PowerSeries.subst x g, PowerSeries.subst y g] G.toPowerSeries

The homomorphism defect at substitutable x, y is g(F(x, y)) - G(g(x), g(y)).

@[simp]

theorem FormalGroup.homDefect_X {R : Type u_1} [CommRing R] (F G : FormalGroup R) : F.homDefect G PowerSeries.X = F.toPowerSeries - G.toPowerSeries

The homomorphism defect of X is the difference F - G of the formal group laws.

theorem FormalGroup.homDefect_𝔾ₐ {R : Type u_1} [CommRing R] (F : FormalGroup R) {f : PowerSeries R} : F.homDefect 𝔾ₐ f = PowerSeries.subst F.toPowerSeries f - PowerSeries.subst (MvPowerSeries.X 0) f - PowerSeries.subst (MvPowerSeries.X 1) f

The homomorphism defect towards the additive formal group law is the additivity defect f(F(X, Y)) - f(X) - f(Y).

theorem FormalGroup.homDefect_𝔾ₐ_sub {R : Type u_1} [CommRing R] (F : FormalGroup R) {g h : PowerSeries R} : F.homDefect 𝔾ₐ (g - h) = F.homDefect 𝔾ₐ g - F.homDefect 𝔾ₐ h

The homomorphism defect towards the additive formal group law is additive in the series.

theorem FormalGroup.le_order_homDefect_𝔾ₐ {R : Type u_1} [CommRing R] (F : FormalGroup R) {g : PowerSeries R} {n : ℕ} (hg : ↑n ≤ g.order) : ↑n ≤ (F.homDefect 𝔾ₐ g).order

The homomorphism defect of g towards the additive formal group law vanishes to the order of g.

theorem FormalGroup.homDefect_eq_sub_subst_pair {R : Type u_1} [CommRing R] (F G : FormalGroup R) (f : PowerSeries R) : F.homDefect G f = PowerSeries.subst F.toPowerSeries f - MvPowerSeries.subst ![PowerSeries.subst (MvPowerSeries.X 0) f, PowerSeries.subst (MvPowerSeries.X 1) f] G.toPowerSeries

The homomorphism defect of f, with G evaluated at the pair (f(X), f(Y)).

@[simp]

theorem FormalGroup.homDefect_zero {R : Type u_1} [CommRing R] {F G : FormalGroup R} : F.homDefect G 0 = 0

The homomorphism defect of zero vanishes.

theorem FormalGroup.coeff_subst_sub_subst_of_degree_le {R : Type u_1} [CommRing R] (G : FormalGroup R) {τ : Type u_2} {x y z w : MvPowerSeries τ R} (hx : MvPowerSeries.constantCoeff x = 0) (hy : MvPowerSeries.constantCoeff y = 0) (hz : MvPowerSeries.constantCoeff z = 0) (hw : MvPowerSeries.constantCoeff w = 0) {n : ℕ} (hxy : ↑n ≤ (x - y).order) (hzw : ↑n ≤ (z - w).order) {e : τ →₀ ℕ} (he : Finsupp.degree e ≤ n) : (MvPowerSeries.coeff e) (MvPowerSeries.subst ![x, z] G.toPowerSeries - MvPowerSeries.subst ![y, w] G.toPowerSeries) = (MvPowerSeries.coeff e) (x - y) + (MvPowerSeries.coeff e) (z - w)

The coefficients of G(x, z) - G(y, w) in degrees at most n are those of (x - y) + (z - w), when x - y and z - w have order at least n.

theorem FormalGroup.homogeneousComponent_subst_sub_subst {R : Type u_1} [CommRing R] (G : FormalGroup R) {τ : Type u_2} {x y z w : MvPowerSeries τ R} (hx : MvPowerSeries.constantCoeff x = 0) (hy : MvPowerSeries.constantCoeff y = 0) (hz : MvPowerSeries.constantCoeff z = 0) (hw : MvPowerSeries.constantCoeff w = 0) {n : ℕ} (hxy : ↑n ≤ (x - y).order) (hzw : ↑n ≤ (z - w).order) : (MvPowerSeries.homogeneousComponent n) (MvPowerSeries.subst ![x, z] G.toPowerSeries - MvPowerSeries.subst ![y, w] G.toPowerSeries) = (MvPowerSeries.homogeneousComponent n) (x - y) + (MvPowerSeries.homogeneousComponent n) (z - w)

The degree-n part of G(x, z) - G(y, w) is that of (x - y) + (z - w), when x - y and z - w have order at least n.

theorem FormalGroup.le_order_homDefect_sub {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) {n : ℕ} (hfg : ↑n ≤ (f - g).order) : ↑n ≤ (F.homDefect G f - F.homDefect G g).order

The homomorphism defects of two series agreeing below degree n agree below degree n.

theorem FormalGroup.homogeneousComponent_homDefect_add_sub {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f : PowerSeries R} (hf : PowerSeries.constantCoeff f = 0) {n : ℕ} (hn : n ≠ 0) (c : R) : (MvPowerSeries.homogeneousComponent n) (F.homDefect G (f + c • PowerSeries.X ^ n) - F.homDefect G f) = ↑(c • ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n - MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n))

The lowest-degree part of the change of the homomorphism defect under f ↦ f + c Xⁿ is c ((X + Y)ⁿ - Xⁿ - Yⁿ).

structure TauCeti.FormalGroupHom {R : Type u_1} [CommRing R] (F G : FormalGroup R) : Type u_1

A homomorphism of formal group laws is a series f with zero constant term such that f(F(X,Y)) = G(f(X),f(Y)).

• toPowerSeries : PowerSeries R

  The underlying one-variable series.

• zero_constantCoeff : PowerSeries.constantCoeff self.toPowerSeries = 0

  The homomorphism sends the origin to the origin.

• hom : PowerSeries.subst F.toPowerSeries self.toPowerSeries = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) self.toPowerSeries) G.toPowerSeries

  Compatibility with the formal group laws.

theorem TauCeti.FormalGroupHom.ext {R : Type u_1} {inst✝ : CommRing R} {F G : FormalGroup R} {x y : FormalGroupHom F G} (toPowerSeries : x.toPowerSeries = y.toPowerSeries) : x = y

theorem TauCeti.FormalGroupHom.ext_iff {R : Type u_1} {inst✝ : CommRing R} {F G : FormalGroup R} {x y : FormalGroupHom F G} : x = y ↔ x.toPowerSeries = y.toPowerSeries

def TauCeti.FormalGroupHom.ofSourceEq {R : Type u_1} [CommRing R] {F G F' : FormalGroup R} (e : F = F') (f : FormalGroupHom F G) : FormalGroupHom F' G

Transport a homomorphism along an equality of source formal groups.

@[simp]

theorem TauCeti.FormalGroupHom.ofSourceEq_toPowerSeries {R : Type u_1} [CommRing R] {F G F' : FormalGroup R} (e : F = F') (f : FormalGroupHom F G) : (ofSourceEq e f).toPowerSeries = f.toPowerSeries

theorem TauCeti.FormalGroupHom.hasSubst {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : PowerSeries.HasSubst f.toPowerSeries

The series of a formal group homomorphism can be substituted.

theorem TauCeti.FormalGroupHom.hom_subst {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} {a : Fin 2 → MvPowerSeries σ R} (ha : MvPowerSeries.HasSubst a) : PowerSeries.subst (MvPowerSeries.subst a F.toPowerSeries) f.toPowerSeries = MvPowerSeries.subst (fun (i : Fin 2) => PowerSeries.subst (a i) f.toPowerSeries) G.toPowerSeries

The homomorphism equation after substituting any admissible coordinate family.

theorem TauCeti.FormalGroupHom.hom_additive_iff {R : Type u_1} [CommRing R] {F : FormalGroup R} {g : PowerSeries R} : PowerSeries.subst F.toPowerSeries g = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) g) FormalGroup.𝔾ₐ.toPowerSeries ↔ PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g

The homomorphism equation into the additive formal group is the additivity equation.

@[simp]

theorem TauCeti.FormalGroupHom.homDefect_toPowerSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : F.homDefect G f.toPowerSeries = 0

A homomorphism of formal group laws has zero homomorphism defect.

def TauCeti.FormalGroupHom.ofHomDefectEqZero {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f : PowerSeries R} (hf : PowerSeries.constantCoeff f = 0) (h : F.homDefect G f = 0) : FormalGroupHom F G

A power series without constant term whose homomorphism defect vanishes, as a homomorphism of formal group laws.

@[simp]

theorem TauCeti.FormalGroupHom.ofHomDefectEqZero_toPowerSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f : PowerSeries R} (hf : PowerSeries.constantCoeff f = 0) (h : F.homDefect G f = 0) : (ofHomDefectEqZero hf h).toPowerSeries = f

noncomputable def TauCeti.FormalGroupHom.ofInverse {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g : PowerSeries R) (hg : PowerSeries.constantCoeff g = 0) (hfg : PowerSeries.subst g f.toPowerSeries = PowerSeries.X) (hgf : PowerSeries.subst f.toPowerSeries g = PowerSeries.X) : FormalGroupHom G F

A substitution inverse of a formal group homomorphism is a homomorphism.

@[simp]

theorem TauCeti.FormalGroupHom.ofInverse_toPowerSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g : PowerSeries R) (hg : PowerSeries.constantCoeff g = 0) (hfg : PowerSeries.subst g f.toPowerSeries = PowerSeries.X) (hgf : PowerSeries.subst f.toPowerSeries g = PowerSeries.X) : (f.ofInverse g hg hfg hgf).toPowerSeries = g

noncomputable def TauCeti.FormalGroupHom.id {R : Type u_1} [CommRing R] (F : FormalGroup R) : FormalGroupHom F F

The identity homomorphism has underlying series X.

@[simp]

theorem TauCeti.FormalGroupHom.id_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) : (id F).toPowerSeries = PowerSeries.X

noncomputable def TauCeti.FormalGroupHom.comp {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (g : FormalGroupHom G H) (f : FormalGroupHom F G) : FormalGroupHom F H

Composition of formal group homomorphisms, with the outer map first.

@[simp]

theorem TauCeti.FormalGroupHom.comp_toPowerSeries {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (g : FormalGroupHom G H) (f : FormalGroupHom F G) : (g.comp f).toPowerSeries = PowerSeries.subst f.toPowerSeries g.toPowerSeries

@[simp]

theorem TauCeti.FormalGroupHom.id_comp {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : (id G).comp f = f

@[simp]

theorem TauCeti.FormalGroupHom.comp_id {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : f.comp (id F) = f

theorem TauCeti.FormalGroupHom.comp_assoc {R : Type u_1} [CommRing R] {F G H K : FormalGroup R} (h : FormalGroupHom H K) (g : FormalGroupHom G H) (f : FormalGroupHom F G) : (h.comp g).comp f = h.comp (g.comp f)

Composition of formal group homomorphisms is associative.

theorem TauCeti.FormalGroupHom.eq_of_subst_eq_X {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g g' : FormalGroupHom G F) (hgf : PowerSeries.subst f.toPowerSeries g.toPowerSeries = PowerSeries.X) (hfg' : PowerSeries.subst g'.toPowerSeries f.toPowerSeries = PowerSeries.X) : g = g'

A left substitution inverse and a right substitution inverse of the same homomorphism agree.

theorem TauCeti.FormalGroupHom.coeff_one_comp {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (g : FormalGroupHom G H) (f : FormalGroupHom F G) : (PowerSeries.coeff 1) (g.comp f).toPowerSeries = (PowerSeries.coeff 1) g.toPowerSeries * (PowerSeries.coeff 1) f.toPowerSeries

Linear coefficients multiply under composition.

noncomputable def TauCeti.FormalGroupHom.applyPoint {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} (x : F.Point σ) : G.Point σ

Apply a homomorphism to a native formal power-series point by substitution.

@[simp]

theorem TauCeti.FormalGroupHom.applyPoint_val {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} (x : F.Point σ) : ↑(f.applyPoint x) = PowerSeries.subst (↑x) f.toPowerSeries

@[simp]

theorem TauCeti.FormalGroupHom.applyPoint_zero {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} : f.applyPoint 0 = 0

@[simp]

theorem TauCeti.FormalGroupHom.applyPoint_add {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} (x y : F.Point σ) : f.applyPoint (x + y) = f.applyPoint x + f.applyPoint y

noncomputable def TauCeti.FormalGroupHom.toAddMonoidHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (σ : Type u_2) : F.Point σ →+ G.Point σ

The induced additive map on native power-series points.

@[simp]

theorem TauCeti.FormalGroupHom.toAddMonoidHom_apply {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) {σ : Type u_2} (x : F.Point σ) : (f.toAddMonoidHom σ) x = f.applyPoint x

@[simp]

theorem TauCeti.FormalGroupHom.id_applyPoint {R : Type u_1} [CommRing R] {F : FormalGroup R} {σ : Type u_2} (x : F.Point σ) : (id F).applyPoint x = x

@[simp]

theorem TauCeti.FormalGroupHom.comp_applyPoint {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (g : FormalGroupHom G H) (f : FormalGroupHom F G) {σ : Type u_2} (x : F.Point σ) : (g.comp f).applyPoint x = g.applyPoint (f.applyPoint x)

structure TauCeti.FormalGroupIso {R : Type u_1} [CommRing R] (F G : FormalGroup R) : Type u_1

An isomorphism of formal group laws with specified mutually inverse homomorphisms. The inverse laws are equations of substitution operators on one-variable power series.

• toHom : FormalGroupHom F G

  The forward homomorphism.

• invHom : FormalGroupHom G F

  The inverse homomorphism.

• left_inv : PowerSeries.subst self.invHom.toPowerSeries ∘ PowerSeries.subst self.toHom.toPowerSeries = id

  Substitution by the forward series followed by the inverse is the identity.

• right_inv : PowerSeries.subst self.toHom.toPowerSeries ∘ PowerSeries.subst self.invHom.toPowerSeries = id

  Substitution by the inverse series followed by the forward is the identity.

noncomputable def TauCeti.FormalGroupIso.ofSubstEqX {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g : FormalGroupHom G F) (hfg : PowerSeries.subst g.toPowerSeries f.toPowerSeries = PowerSeries.X) (hgf : PowerSeries.subst f.toPowerSeries g.toPowerSeries = PowerSeries.X) : FormalGroupIso F G

Construct an isomorphism from the two series substitution identities.

@[simp]

theorem TauCeti.FormalGroupIso.ofSubstEqX_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g : FormalGroupHom G F) (hfg : PowerSeries.subst g.toPowerSeries f.toPowerSeries = PowerSeries.X) (hgf : PowerSeries.subst f.toPowerSeries g.toPowerSeries = PowerSeries.X) : (ofSubstEqX f g hfg hgf).toHom = f

@[simp]

theorem TauCeti.FormalGroupIso.ofSubstEqX_invHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (g : FormalGroupHom G F) (hfg : PowerSeries.subst g.toPowerSeries f.toPowerSeries = PowerSeries.X) (hgf : PowerSeries.subst f.toPowerSeries g.toPowerSeries = PowerSeries.X) : (ofSubstEqX f g hfg hgf).invHom = g

@[simp]

theorem TauCeti.FormalGroupIso.subst_invHom_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : PowerSeries.subst f.invHom.toPowerSeries f.toHom.toPowerSeries = PowerSeries.X

The forward series evaluated at the inverse series is X.

@[simp]

theorem TauCeti.FormalGroupIso.subst_toHom_invHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : PowerSeries.subst f.toHom.toPowerSeries f.invHom.toPowerSeries = PowerSeries.X

The inverse series evaluated at the forward series is X.

theorem TauCeti.FormalGroupIso.isUnit_coeff_one {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : IsUnit ((PowerSeries.coeff 1) f.toHom.toPowerSeries)

The linear coefficient of a formal group isomorphism is a unit.

theorem TauCeti.FormalGroupIso.toHom_toPowerSeries_ne_zero {R : Type u_1} [CommRing R] {F G : FormalGroup R} [Nontrivial R] (f : FormalGroupIso F G) : f.toHom.toPowerSeries ≠ 0

Over a nontrivial ring, the forward series of an isomorphism is nonzero: its linear coefficient is invertible.

theorem TauCeti.FormalGroupIso.ext {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f g : FormalGroupIso F G} (h : f.toHom = g.toHom) : f = g

A formal group isomorphism is determined by its forward homomorphism.

theorem TauCeti.FormalGroupIso.ext_iff {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f g : FormalGroupIso F G} : f = g ↔ f.toHom = g.toHom

class TauCeti.FormalGroupIso.IsStrict {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : Prop

A strict isomorphism has linear coefficient one.

• coeff_one : (PowerSeries.coeff 1) f.toHom.toPowerSeries = 1

  The forward coordinate is tangent to the identity.

def TauCeti.FormalGroupIso.symm {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : FormalGroupIso G F

Reverse a formal group isomorphism.

@[simp]

theorem TauCeti.FormalGroupIso.symm_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.symm.toHom = f.invHom

@[simp]

theorem TauCeti.FormalGroupIso.symm_invHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.symm.invHom = f.toHom

@[simp]

theorem TauCeti.FormalGroupIso.symm_symm {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.symm.symm = f

noncomputable def TauCeti.FormalGroupIso.refl {R : Type u_1} [CommRing R] (F : FormalGroup R) : FormalGroupIso F F

The identity formal group isomorphism.

@[simp]

theorem TauCeti.FormalGroupIso.refl_toHom {R : Type u_1} [CommRing R] (F : FormalGroup R) : (refl F).toHom = FormalGroupHom.id F

@[simp]

theorem TauCeti.FormalGroupIso.refl_invHom {R : Type u_1} [CommRing R] (F : FormalGroup R) : (refl F).invHom = FormalGroupHom.id F

@[simp]

theorem TauCeti.FormalGroupIso.toHom_comp_invHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.toHom.comp f.invHom = FormalGroupHom.id G

The inverse followed by the forward map is the identity homomorphism.

@[simp]

theorem TauCeti.FormalGroupIso.invHom_comp_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.invHom.comp f.toHom = FormalGroupHom.id F

The forward map followed by the inverse is the identity homomorphism.

noncomputable def TauCeti.FormalGroupIso.trans {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) : FormalGroupIso F H

Compose formal group isomorphisms, applying the first argument first.

@[simp]

theorem TauCeti.FormalGroupIso.trans_toHom {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) : (f.trans g).toHom = g.toHom.comp f.toHom

@[simp]

theorem TauCeti.FormalGroupIso.trans_invHom {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) : (f.trans g).invHom = f.invHom.comp g.invHom

@[simp]

theorem TauCeti.FormalGroupIso.refl_trans {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : (refl F).trans f = f

@[simp]

theorem TauCeti.FormalGroupIso.trans_refl {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.trans (refl G) = f

@[simp]

theorem TauCeti.FormalGroupIso.self_trans_symm {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.trans f.symm = refl F

@[simp]

theorem TauCeti.FormalGroupIso.symm_trans_self {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) : f.symm.trans f = refl G

theorem TauCeti.FormalGroupIso.trans_assoc {R : Type u_1} [CommRing R] {F G H K : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) (h : FormalGroupIso H K) : (f.trans g).trans h = f.trans (g.trans h)

Composition of formal group isomorphisms is associative.

instance TauCeti.FormalGroupIso.instIsStrictRefl {R : Type u_1} [CommRing R] (F : FormalGroup R) : (refl F).IsStrict

instance TauCeti.FormalGroupIso.instIsStrictSymm {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) [f.IsStrict] : f.symm.IsStrict

instance TauCeti.FormalGroupIso.instIsStrictTrans {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) [f.IsStrict] [g.IsStrict] : (f.trans g).IsStrict

noncomputable def TauCeti.FormalGroupIso.toAddEquiv {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) (σ : Type u_2) : F.Point σ ≃+ G.Point σ

The additive equivalence induced on native power-series points.

@[simp]

theorem TauCeti.FormalGroupIso.toAddEquiv_apply {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) {σ : Type u_2} (x : F.Point σ) : (f.toAddEquiv σ) x = f.toHom.applyPoint x

@[simp]

theorem TauCeti.FormalGroupIso.toAddEquiv_symm_apply {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) {σ : Type u_2} (x : G.Point σ) : (f.toAddEquiv σ).symm x = f.invHom.applyPoint x

@[simp]

theorem TauCeti.FormalGroupIso.toAddEquiv_refl {R : Type u_1} [CommRing R] (F : FormalGroup R) (σ : Type u_2) : (refl F).toAddEquiv σ = AddEquiv.refl (F.Point σ)

@[simp]

theorem TauCeti.FormalGroupIso.toAddEquiv_trans {R : Type u_1} [CommRing R] {F G H : FormalGroup R} (f : FormalGroupIso F G) (g : FormalGroupIso G H) (σ : Type u_2) : (f.trans g).toAddEquiv σ = (f.toAddEquiv σ).trans (g.toAddEquiv σ)

@[simp]

theorem TauCeti.FormalGroupIso.toAddEquiv_symm {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) (σ : Type u_2) : f.symm.toAddEquiv σ = (f.toAddEquiv σ).symm

noncomputable def TauCeti.FormalGroupHom.toIso {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : IsUnit ((PowerSeries.coeff 1) f.toPowerSeries)) : FormalGroupIso F G

A homomorphism with invertible linear coefficient is a formal group isomorphism.

@[simp]

theorem TauCeti.FormalGroupHom.toIso_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : IsUnit ((PowerSeries.coeff 1) f.toPowerSeries)) : (f.toIso hf).toHom = f

@[simp]

theorem TauCeti.FormalGroupHom.toIso_invHom_toPowerSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : IsUnit ((PowerSeries.coeff 1) f.toPowerSeries)) : (f.toIso hf).invHom.toPowerSeries = f.toPowerSeries.substInvOfIsUnit hf

Base change

noncomputable def TauCeti.FormalGroupHom.map {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (f : FormalGroupHom F G) (φ : R →+* S) : FormalGroupHom (F.map φ) (G.map φ)

The base change of a formal group homomorphism along a ring homomorphism φ: its series is obtained by applying φ to every coefficient, and it maps F.map φ to G.map φ.

@[simp]

theorem TauCeti.FormalGroupHom.map_toPowerSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (f : FormalGroupHom F G) (φ : R →+* S) : (f.map φ).toPowerSeries = (PowerSeries.map φ) f.toPowerSeries

@[simp]

theorem TauCeti.FormalGroupHom.map_id {R : Type u_1} [CommRing R] {F : FormalGroup R} {S : Type u_2} [CommRing S] (φ : R →+* S) : (id F).map φ = id (F.map φ)

Base change sends the identity homomorphism to the identity homomorphism.

@[simp]

theorem TauCeti.FormalGroupHom.map_comp {R : Type u_1} [CommRing R] {F G H : FormalGroup R} {S : Type u_2} [CommRing S] (g : FormalGroupHom G H) (f : FormalGroupHom F G) (φ : R →+* S) : (g.comp f).map φ = (g.map φ).comp (f.map φ)

Base change commutes with composition of homomorphisms.

@[simp]

theorem TauCeti.FormalGroupHom.map_ringHomId {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : f.map (RingHom.id R) = f

Base change along the identity ring homomorphism does nothing. The formal groups F.map (RingHom.id R) and F are definitionally equal, so no transport is needed.

@[simp]

theorem TauCeti.FormalGroupHom.map_map {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] (f : FormalGroupHom F G) (φ : R →+* S) (ψ : S →+* T) : (f.map φ).map ψ = f.map (ψ.comp φ)

Successive base changes agree with base change along the composite. The formal groups (F.map φ).map ψ and F.map (ψ.comp φ) are definitionally equal, so no transport is needed.

noncomputable def TauCeti.FormalGroupIso.map {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) (φ : R →+* S) : FormalGroupIso (F.map φ) (G.map φ)

The base change of a formal group isomorphism along a ring homomorphism φ, with forward and inverse homomorphisms the base changes of those of e.

@[simp]

theorem TauCeti.FormalGroupIso.map_toHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) (φ : R →+* S) : (e.map φ).toHom = e.toHom.map φ

@[simp]

theorem TauCeti.FormalGroupIso.map_invHom {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) (φ : R →+* S) : (e.map φ).invHom = e.invHom.map φ

@[simp]

theorem TauCeti.FormalGroupIso.map_refl {R : Type u_1} [CommRing R] {F : FormalGroup R} {S : Type u_2} [CommRing S] (φ : R →+* S) : (refl F).map φ = refl (F.map φ)

Base change sends the identity isomorphism to the identity isomorphism.

@[simp]

theorem TauCeti.FormalGroupIso.map_symm {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) (φ : R →+* S) : e.symm.map φ = (e.map φ).symm

Base change commutes with reversing an isomorphism.

@[simp]

theorem TauCeti.FormalGroupIso.map_trans {R : Type u_1} [CommRing R] {F G H : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) (e' : FormalGroupIso G H) (φ : R →+* S) : (e.trans e').map φ = (e.map φ).trans (e'.map φ)

Base change commutes with composition of isomorphisms.

@[simp]

theorem TauCeti.FormalGroupIso.map_ringHomId {R : Type u_1} [CommRing R] {F G : FormalGroup R} (e : FormalGroupIso F G) : e.map (RingHom.id R) = e

Base change along the identity ring homomorphism does nothing. The formal groups F.map (RingHom.id R) and F are definitionally equal, so no transport is needed.

@[simp]

theorem TauCeti.FormalGroupIso.map_map {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] (e : FormalGroupIso F G) (φ : R →+* S) (ψ : S →+* T) : (e.map φ).map ψ = e.map (ψ.comp φ)

Successive base changes agree with base change along the composite. The formal groups (F.map φ).map ψ and F.map (ψ.comp φ) are definitionally equal, so no transport is needed.

instance TauCeti.FormalGroupIso.instIsStrictMap {R : Type u_1} [CommRing R] {F G : FormalGroup R} {S : Type u_2} [CommRing S] (e : FormalGroupIso F G) [e.IsStrict] (φ : R →+* S) : (e.map φ).IsStrict

The base change of a strict isomorphism is strict.