Module

CyclicIndex.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Book.CyclicIndex

5 declarations indexed from sourceView source ↗

Module documentation

Coprime indices in a discrete book value group

The value group of a nontrivial discrete book exponential valuation is an infinite cyclic additive group. In an infinite cyclic group, two subgroups which generate the whole group have coprime indices. This file records that group-theoretic fact and specializes it to actual book value subgroups.

Imports4

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Book.ValueGroup
Mathlib.GroupTheory.Archimedean
Mathlib.GroupTheory.SpecificGroups.Cyclic
Mathlib.RingTheory.Int.Basic

Imported by2

theorem

int_addSubgroup_index_coprime_of_sup_eq_top

L30 ↗

TameAbhyankar.int_addSubgroup_index_coprime_of_sup_eq_top

Documentation

Two subgroups of ℤ which generate ℤ have coprime indices.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem int_addSubgroup_index_coprime_of_sup_eq_top
    (A B : AddSubgroup ℤ) (hsup : A ⊔ B = ⊤) :
    Nat.Coprime A.index B.index

theorem

addSubgroup_index_coprime_of_addEquiv_int

L54 ↗

TameAbhyankar.addSubgroup_index_coprime_of_addEquiv_int

Documentation

Coprimality of subgroup indices is invariant under identifying the ambient additive group with ℤ.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem addSubgroup_index_coprime_of_addEquiv_int
    {G : Type u} [AddCommGroup G] (e : G ≃+ ℤ)
    (A B : AddSubgroup G) (hsup : A ⊔ B = ⊤) :
    Nat.Coprime A.index B.index

theorem

bookValueSubgroup_index_coprime_of_sup_eq_top

L69 ↗

TameAbhyankar.bookValueSubgroup_index_coprime_of_sup_eq_top

Documentation

The subgroups of a discrete book value group which generate the whole value group have coprime indices.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem bookValueSubgroup_index_coprime_of_sup_eq_top
    {Top : Type u} [Field Top]
    (w : LubinTate.Valuations.ExponentialValuation Top)
    (hwdisc : LubinTate.Valuations.DiscreteExponentialValuation w)
    (A B : AddSubgroup (exponentialValueSubgroup w))
    (hsup : A ⊔ B = ⊤) :
    Nat.Coprime A.index B.index

theorem

bookValueSubgroup_relIndex_coprime_of_sup_eq

L104 ↗

TameAbhyankar.bookValueSubgroup_relIndex_coprime_of_sup_eq

Documentation

Ambient-subgroup form: if two subgroups of ℝ lie in a discrete book value group and their supremum is that value group, their relative indices in the value group are coprime.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem bookValueSubgroup_relIndex_coprime_of_sup_eq
    {Top : Type u} [Field Top]
    (w : LubinTate.Valuations.ExponentialValuation Top)
    (hwdisc : LubinTate.Valuations.DiscreteExponentialValuation w)
    (GammaA GammaB : AddSubgroup ℝ)
    (hsup : GammaA ⊔ GammaB = exponentialValueSubgroup w) :
    Nat.Coprime
      (GammaA.relIndex (exponentialValueSubgroup w))
      (GammaB.relIndex (exponentialValueSubgroup w))

theorem

bookRamificationIndex_coprime_of_valueSubgroup_sup_eq

L145 ↗

TameAbhyankar.bookRamificationIndex_coprime_of_valueSubgroup_sup_eq

Documentation

Book-valuation form of the cyclic-index calculation. Exact extensions whose two value subgroups generate the discrete target value group have coprime book ramification indices.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem bookRamificationIndex_coprime_of_valueSubgroup_sup_eq
    {A B Top : Type u} [Field A] [Field B] [Field Top]
    (vA : LubinTate.Valuations.ExponentialValuation A)
    (vB : LubinTate.Valuations.ExponentialValuation B)
    (w : LubinTate.Valuations.ExponentialValuation Top)
    (hwdisc : LubinTate.Valuations.DiscreteExponentialValuation w)
    (hsup : exponentialValueSubgroup vA ⊔
      exponentialValueSubgroup vB = exponentialValueSubgroup w) :
    Nat.Coprime (exponentialRamificationIndex vA w)
      (exponentialRamificationIndex vB w)

Module documentation

Coprime indices in a discrete book value group

Declarations

int_addSubgroup_index_coprime_of_sup_eq_top

addSubgroup_index_coprime_of_addEquiv_int

bookValueSubgroup_index_coprime_of_sup_eq_top

bookValueSubgroup_relIndex_coprime_of_sup_eq

bookRamificationIndex_coprime_of_valueSubgroup_sup_eq