Module

RamificationIndexTower.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.RamificationIndexTower

3 declarations indexed from sourceView source ↗

Module documentation

Ramification index in valued-field towers

The generic tower and embedding-monotonicity lemmas extracted from the tame adapter.

Imports2

Imported by3

theorem

exponentialRamificationIndex_mul_in_tower

L30 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_mul_in_tower

Documentation

The actual value-group ramification index is multiplicative in exact valued-field towers.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section RamificationIndexTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L]

Lean source · statement

theorem exponentialRamificationIndex_mul_in_tower
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a) :
    exponentialRamificationIndex v u * exponentialRamificationIndex u w =
      exponentialRamificationIndex v w

theorem

exponentialRamificationIndex_le_in_tower

L75 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_le_in_tower

Documentation

In a finite relative extension, the ramification index of the lower stage is at most that of the whole exact valued-field tower.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section RamificationIndexTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L]

Lean source · statement

theorem exponentialRamificationIndex_le_in_tower
    [FiniteDimensional M L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a) :
    exponentialRamificationIndex v u ≤ exponentialRamificationIndex v w

theorem

exponentialRamificationIndex_le_of_algHom

L94 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_le_of_algHom

Documentation

Ramification index is monotone along an algebra embedding of finite extensions. The embedding supplies the relative algebra and scalar-tower structures used by exponentialRamificationIndex_le_in_tower.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section RamificationIndexTower
variable {K M L : Type u} [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L]

Lean source · statement

theorem exponentialRamificationIndex_le_of_algHom
    {K E D : Type} [Field K] [Field E] [Field D]
    [Algebra K E] [Algebra K D]
    [FiniteDimensional K E] [FiniteDimensional K D]
    (i : E →ₐ[K] D)
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation E)
    (w : LubinTate.Valuations.ExponentialValuation D)
    (hKE : ∀ x : K, u (algebraMap K E x) = v x)
    (hED : ∀ x : E, w (i x) = u x) :
    exponentialRamificationIndex v u ≤ exponentialRamificationIndex v w

Module documentation

Ramification index in valued-field towers

Declarations

exponentialRamificationIndex_mul_in_tower

exponentialRamificationIndex_le_in_tower

exponentialRamificationIndex_le_of_algHom