Documentation

TauCeti.RingTheory.LaurentSeries.Colimit

Puiseux series as a colimit of ramified Laurent fields #

Ramified Laurent levels are indexed by TauCeti.RamificationIndex, the positive natural numbers ordered by divisibility. The transition from level n to level m, for n ∣ m, substitutes X ^ (m / n) for X. These transitions form a filtered diagram of commutative algebras over the coefficient field.

The level embeddings into the Puiseux series field form a cocone on this diagram. This file proves its universal property: a compatible family of algebra maps out of all ramified levels factors uniquely through the Puiseux field. Thus the bounded-denominator carrier of Puiseux series is not merely the union of the levels; it is their colimit in commutative algebras.

Main definitions #

source
noncomputable def TauCeti.puiseuxField.levelDiagram (K : Type u_1) [Field K] :
CategoryTheory.Functor RamificationIndex (CommAlgCat K)

The filtered diagram of ramified Laurent fields. Its object at n is a copy of K⸨X⸩, and its map along n ≤ m substitutes X ^ (m / n) for X.

Instances For
    source
    @[simp]
    theorem TauCeti.puiseuxField.levelDiagram_obj (K : Type u_1) [Field K] (n : RamificationIndex) :
    (levelDiagram K).obj n = ↧(LaurentSeries K)

    The object at every ramification index is the Laurent-series K-algebra.

    source
    @[simp]
    theorem TauCeti.puiseuxField.levelDiagram_map_hom (K : Type u_1) [Field K] {n m : RamificationIndex} (f : n ⟶ m) :
    CommAlgCat.Hom.hom ((levelDiagram K).map f) = LaurentSeries.expand K (RamificationIndex.transitionDegree ⋯)

    The transition map along n ≤ m is the substitution X ↦ X ^ (m / n).

    source
    noncomputable def TauCeti.puiseuxField.levelCocone (K : Type u_1) [Field K] :
    CategoryTheory.Limits.Cocone (levelDiagram K)

    The level embeddings into the Puiseux field, as a cocone on the ramified-level diagram.

    Instances For
      source
      @[simp]
      theorem TauCeti.puiseuxField.levelCocone_pt (K : Type u_1) [Field K] :
      (levelCocone K).pt = ↧↥(puiseuxField K)

      The point of the level cocone is the Puiseux field.

      source
      @[simp]
      theorem TauCeti.puiseuxField.levelCocone_ι_app_hom (K : Type u_1) [Field K] (n : RamificationIndex) :
      CommAlgCat.Hom.hom ((levelCocone K).ι.app n) = levelEmbedding K n.toPNat

      The component of the level cocone at n is the level-n embedding.

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

      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.

      Instances For