Documentation

TauCeti.RingTheory.LaurentSeries.RamificationIndex

Ramification indices #

Ramified Laurent levels are indexed by positive natural numbers ordered by divisibility. This file introduces that index type, shows it is a directed order with bottom element 1, and records the transition degree m / n attached to n ∣ m.

Main definitions #

source
structure TauCeti.RamificationIndex :
Type

Positive ramification indices, ordered by divisibility rather than by their usual order.

  • toPNat : ℕ+

    The positive natural number underlying a ramification index.

Instances For
    source
    theorem TauCeti.RamificationIndex.ext {x y : RamificationIndex} (toPNat : x.toPNat = y.toPNat) :
    x = y
    source
    theorem TauCeti.RamificationIndex.ext_iff {x y : RamificationIndex} :
    x = y ↔ x.toPNat = y.toPNat
    source
    @[instance_reducible]
    instance TauCeti.RamificationIndex.instLE :
    LE RamificationIndex
    source
    @[simp]
    theorem TauCeti.RamificationIndex.le_iff_dvd {n m : RamificationIndex} :
    n ≤ m ↔ n.toPNat ∣ m.toPNat

    Comparison of ramification indices is divisibility of the underlying positive integers.

    source
    @[instance_reducible]
    instance TauCeti.RamificationIndex.instPartialOrder :
    PartialOrder RamificationIndex
    source
    instance TauCeti.RamificationIndex.instIsDirectedOrder :
    IsDirectedOrder RamificationIndex
    source
    @[instance_reducible]
    instance TauCeti.RamificationIndex.instOrderBot :
    OrderBot RamificationIndex
    source
    @[simp]
    theorem TauCeti.RamificationIndex.toPNat_bot :
    ⊥.toPNat = 1

    The least ramification index is 1.

    source
    def TauCeti.RamificationIndex.transitionDegree {n m : RamificationIndex} (_h : n ≤ m) :
    ℕ+

    The quotient m / n attached to a divisibility relation n ≤ m.

    Instances For
      source
      theorem TauCeti.RamificationIndex.transitionDegree_def {n m : RamificationIndex} (h : n ≤ m) :
      transitionDegree h = m.toPNat.divExact n.toPNat

      The transition degree along n ≤ m is the exact quotient m / n of positive naturals.

      source
      theorem TauCeti.RamificationIndex.mul_transitionDegree {n m : RamificationIndex} (h : n ≤ m) :
      n.toPNat * transitionDegree h = m.toPNat

      Multiplying an index by its transition degree recovers the target index.

      source
      @[simp]
      theorem TauCeti.RamificationIndex.transitionDegree_refl (n : RamificationIndex) :
      transitionDegree ⋯ = 1
      source
      theorem TauCeti.RamificationIndex.transitionDegree_trans {n m l : RamificationIndex} (hnm : n ≤ m) (hml : m ≤ l) :
      transitionDegree hnm * transitionDegree hml = transitionDegree ⋯

      Transition degrees multiply along a chain of ramification indices.