Formal Laurent fields, Puiseux expansions and continuous differential calculus

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremNewton–Puiseux theorem#

Over an algebraically closed field K of characteristic zero, every nonconstant polynomial over the Puiseux field has a root lying in a single ramified level.

TauCeti.puiseuxField.exists_isRoot_levelEmbedding.{u_1} {K : Type u_1} [Field K] [IsAlgClosed K]
  [CharZero K] {P : Polynomial ↥(TauCeti.puiseuxField K)} (hP : P.degree ≠ 0) :
  ∃ n y, P.IsRoot ((TauCeti.puiseuxField.levelEmbedding K n) y)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.exists_isRoot_levelEmbedding.

Other forms

Newton–Puiseux theorem. Formalized in Tau Ceti as TauCeti.LaurentSeries.exists_isRoot_map_expand.

TauCeti.LaurentSeries.exists_isRoot_map_expand.{u_1} {K : Type u_1} [Field K] [IsAlgClosed K]
  [CharZero K] {P : Polynomial (LaurentSeries K)} (hP : P.degree ≠ 0) :
  ∃ n y, (Polynomial.map (↑(LaurentSeries.expand K n)) P).IsRoot y
Sources
LeanTauCeti.puiseuxField.exists_isRoot_levelEmbedding · TauCeti.LaurentSeries.exists_isRoot_map_expand
Used by 2
Used byFinite extensions of K⸨X⸩ · TauCeti.puiseuxField.instIsAlgClosure

TheoremTauCeti.puiseuxField.instIsAlgClosure#

Over an algebraically closed field K of characteristic zero, the Puiseux field is an algebraic closure of the Laurent-series field K⸨X⸩.

TauCeti.puiseuxField.instIsAlgClosure.{u_1} {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] :
  IsAlgClosure (LaurentSeries K) ↥(TauCeti.puiseuxField K)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.instIsAlgClosure.

Sources
LeanTauCeti.puiseuxField.instIsAlgClosure
Uses 1
Proof usesNewton–Puiseux theorem

DefinitionFinite extensions of K⸨X⸩#

If K is algebraically closed of characteristic zero, then every extension L of K⸨X⸩ of degree e is isomorphic over K⸨X⸩ to the ramified level K⸨u⸩, u ^ e = X. The isomorphism is a chosen one: it is built from a chosen embedding of L into the Puiseux field, whose image is the level-e subfield.

TauCeti.LaurentSeries.Level.algEquivOfFinrankEq.{u_1, u_2} {K : Type u_1} [Field K] [IsAlgClosed K]
  [CharZero K] {L : Type u_2} [Field L] [Algebra (LaurentSeries K) L] {e : ℕ+}
  (h : Module.finrank (LaurentSeries K) L = ↑e) :
  L ≃ₐ[LaurentSeries K] TauCeti.LaurentSeries.Level K e
Lean

Formalized in Tau Ceti as TauCeti.LaurentSeries.Level.algEquivOfFinrankEq.

Sources
LeanTauCeti.LaurentSeries.Level.algEquivOfFinrankEq
Uses 2
Proof usesNewton–Puiseux theorem · TauCeti.puiseuxField.levelGalEquivRootsOfUnity

TheoremTauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero#

If K contains all roots of unity, then a Puiseux series that is a root of a nonzero polynomial of degree d over K⸨X⸩ lies in level d!. Thus all roots of such a polynomial lie in a common level.

TauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero.{u_1} {K : Type u_1} [Field K]
  [∀ (n : ℕ+), HasEnoughRootsOfUnity K ↑n] {p : Polynomial (LaurentSeries K)} (hp : p ≠ 0)
  {x : ↥(TauCeti.puiseuxField K)} (hx : (Polynomial.aeval x) p = 0) :
  x ∈ TauCeti.puiseuxField.level K p.natDegree.factorial.toPNat'
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero.

Sources
LeanTauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero
Uses 1
Proof usesTauCeti.puiseuxField.levelGalEquivRootsOfUnity

DefinitionTauCeti.puiseuxField.levelGalEquivRootsOfUnity#

If the coefficient field has a primitive d-th root of unity, then the Galois group of the level-d subfield of the Puiseux field over K⸨X⸩ is the group of d-th roots of unity of K. The inverse is levelKummer (TauCeti.puiseuxField.levelGalEquivRootsOfUnity_symm_apply).

TauCeti.puiseuxField.levelGalEquivRootsOfUnity.{u_1} (K : Type u_1) [Field K] (d : ℕ+)
  [HasEnoughRootsOfUnity K ↑d] :
  Gal(↥(TauCeti.puiseuxField.level K d)/LaurentSeries K) ≃* ↥(rootsOfUnity (↑d) K)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.levelGalEquivRootsOfUnity.

Sources
LeanTauCeti.puiseuxField.levelGalEquivRootsOfUnity
Used by 2
Used byFinite extensions of K⸨X⸩ · TauCeti.puiseuxField.mem_level_factorial_of_aeval_eq_zero

TheoremFaithfulness#

Distinct points of the Tate module act by distinct automorphisms of the Puiseux field: the automorphism attached to ζ sends t ^ (1 / n) to ζₙ t ^ (1 / n).

TauCeti.puiseuxField.kummer_injective.{u_1} {K : Type u_1} [Field K] :
  Function.Injective ⇑(TauCeti.puiseuxField.kummer K)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.kummer_injective.

Sources
LeanTauCeti.puiseuxField.kummer_injective

TheoremFinite-map residue formula for Laurent series substitution#

Substituting a nonzero power series φ of zero constant coefficient multiplies the residue of f dX by φ.order.toNat, in all characteristics: Res(f(φ) Dφ dX) = φ.order.toNat • Res(f dX).

TauCeti.LaurentSeries.coeff_neg_one_substAlgHom_mul_derivative_eq_nsmul.{u_1} {K : Type u_1}
  [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0)
  (f : LaurentSeries K) :
  ((TauCeti.LaurentSeries.substAlgHom hφ hφ₀) f *
          (LaurentSeries.derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)).coeff
      (-1) =
    φ.order.toNat • f.coeff (-1)
Lean

Formalized in Tau Ceti as TauCeti.LaurentSeries.coeff_neg_one_substAlgHom_mul_derivative_eq_nsmul.

Sources
LeanTauCeti.LaurentSeries.coeff_neg_one_substAlgHom_mul_derivative_eq_nsmul

DefinitionThe continuous derivations of K⸨X⸩ form a free module of rank one with basis the formal derivative D#

the equivalence sends a to a • D, and its inverse evaluates a derivation at the parameter X.

TauCeti.continuousDerivationsEquiv.{u_1} (K : Type u_1) [Field K] :
  LaurentSeries K ≃ₗ[LaurentSeries K] ↥(TauCeti.continuousDerivations K)
Lean

Formalized in Tau Ceti as TauCeti.continuousDerivationsEquiv.

Sources
LeanTauCeti.continuousDerivationsEquiv

DefinitionFormal coordinate changes act invertibly on one-forms#

For a formal coordinate φ, substitution f dX ↦ f (φ) dφ into continuous one-forms, as an equivalence that is semilinear over the substitution automorphism TauCeti.LaurentSeries.substAlgEquiv φ of K⸨X⸩. Its inverse is substitution of the compositional inverse φ⁻¹.

TauCeti.ContinuousKaehlerDifferential.substEquiv.{u_1} {K : Type u_1} [Field K]
  (φ : TauCeti.FormalCoordinate K) :
  TauCeti.ContinuousKaehlerDifferential K ≃ₛₗ[↑(TauCeti.LaurentSeries.substAlgEquiv φ).toRingEquiv]
    TauCeti.ContinuousKaehlerDifferential K
Lean

Formalized in Tau Ceti as TauCeti.ContinuousKaehlerDifferential.substEquiv.

Sources
LeanTauCeti.ContinuousKaehlerDifferential.substEquiv
Uses 1
Statement usesTauCeti.FormalCoordinate

DefinitionTauCeti.puiseuxField.levelCoconeIsColimit#

The Puiseux field is the colimit of the ramified Laurent levels in CommAlgCat K.

Equivalently, every compatible family of K-algebra maps from the levels factors uniquely through the bounded-denominator Puiseux series field.

TauCeti.puiseuxField.levelCoconeIsColimit.{u_1} {K : Type u_1} [Field K] :
  CategoryTheory.Limits.IsColimit (TauCeti.puiseuxField.levelCocone K)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.levelCoconeIsColimit.

Sources
LeanTauCeti.puiseuxField.levelCoconeIsColimit

TheoremThe Puiseux field is not complete#

The partial sums of ∑ j, t ^ ((j + 1) + 1 / (j + 2)) form a Cauchy sequence without a limit.

TauCeti.puiseuxField.not_completeSpace.{u_1} (K : Type u_1) [Field K] :
  ¬CompleteSpace ↥(TauCeti.puiseuxField K)
Lean

Formalized in Tau Ceti as TauCeti.puiseuxField.not_completeSpace.

Sources
LeanTauCeti.puiseuxField.not_completeSpace

StructureTauCeti.FormalCoordinate#

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 ↦ φ.

TauCeti.FormalCoordinate.{u_1} (R : Type u_1) [CommRing R] : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.FormalCoordinate.

Sources
LeanTauCeti.FormalCoordinate
Used by 8
Used byCoassociativity (Δ ⊗ id) Δ = (id ⊗ Δ) Δ of the coproduct · Lazard's classification of formal group laws by height · Lazard's theorem · Strict coordinate changes of commutative formal group laws are representable · Formal coordinate changes act invertibly on one-forms · TauCeti.FormalCoordinate.jetLimitEquiv · Hazewinkel's functional equation lemma · Universality of Hazewinkel's formal group law over ℚ-algebras

DefinitionTauCeti.FormalCoordinate.jetLimitEquiv#

The formal coordinates are the inverse limit of their jet groups: passing to all jets is an isomorphism of topological groups onto the compatible families of jets.

TauCeti.FormalCoordinate.jetLimitEquiv.{u_1} (R : Type u_1) [CommRing R] :
  TauCeti.FormalCoordinate R ≃ₜ* ↥(TauCeti.FormalCoordinate.jetLimit R)
Lean

Formalized in Tau Ceti as TauCeti.FormalCoordinate.jetLimitEquiv.

Sources
LeanTauCeti.FormalCoordinate.jetLimitEquiv
Uses 1
Statement usesTauCeti.FormalCoordinate

InstanceHahnModule.instLieRing#

Hahn series with coefficients in a Lie ring form a Lie ring under the convolution bracket.

HahnModule.instLieRing.{u_1, u_2, u_3} {Γ : Type u_1} {R : Type u_2} {L : Type u_3}
  [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] :
  LieRing (HahnModule Γ R L)
Lean

Formalized in Tau Ceti as HahnModule.instLieRing.

Sources
LeanHahnModule.instLieRing
Used by 1
Used byLieAlgebra.LoopAlgebra.toHahnModule

DefinitionLieAlgebra.LoopAlgebra.toHahnModule#

The embedding of polynomial loops into L-valued Hahn series, sending t ^ a ⊗ x to the monomial x t ^ a.

LieAlgebra.LoopAlgebra.toHahnModule.{u_1, u_2, u_3} (R : Type u_1) (Γ : Type u_2) (L : Type u_3)
  [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L]
  [LieAlgebra R L] : LieAlgebra.loopAlgebra R Γ L →ₗ⁅R⁆ HahnModule Γ R L
Lean

Formalized in Tau Ceti as LieAlgebra.LoopAlgebra.toHahnModule.

Sources
LeanLieAlgebra.LoopAlgebra.toHahnModule
Uses 1
Statement usesHahnModule.instLieRing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.