NYLL
Module

RamificationNumberRestriction.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationNumberRestriction
5 declarations indexed from sourceView source ↗

Module documentation

quotient-depth identity over a general DVF

The public endpoint has no generator argument. The monogenic integral-generator theorem supplies the top integral generator internally, while the fixed-field ramification number is the intrinsic value of its displacement ideal.

Imports2
Imported by2

Declarations

def

cosetRamificationNumberSum

L37 ↗
RamificationTheory.HilbertRamification.Higher.cosetRamificationNumberSum
Documentation

Sum of ramification numbers over the right coset sigma H, for a specified top generator.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def cosetRamificationNumberSum
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    (z : target.valuationSubring) : ℕ∞
theorem

addVal_cosetGeneratorDisplacementProduct

L51 ↗
RamificationTheory.HilbertRamification.Higher.addVal_cosetGeneratorDisplacementProduct
Documentation

The valuation of the coset displacement product is the corresponding sum of ramification numbers.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem addVal_cosetGeneratorDisplacementProduct
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    (z : target.valuationSubring) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (cosetGeneratorDisplacementProductDVF
          (base := base) (target := target) huniq H sigma z) =
      cosetRamificationNumberSum
        (base := base) (target := target) huniq H sigma z
def

intrinsicCosetRamificationNumberSum

L87 ↗
RamificationTheory.HilbertRamification.Higher.intrinsicCosetRamificationNumberSum
Documentation

The canonical coset sum, with its monogenic integral generator hidden.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
def intrinsicCosetRamificationNumberSum
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : ℕ∞
theorem

cosetRamificationNumberSum_eq_intrinsic

L98 ↗
RamificationTheory.HilbertRamification.Higher.cosetRamificationNumberSum_eq_intrinsic
Documentation

States the theorem cosetRamificationNumberSum_eq_intrinsic.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem cosetRamificationNumberSum_eq_intrinsic
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    {z : target.valuationSubring}
    (hz : Algebra.adjoin base.valuationSubring
      ({z} : Set target.valuationSubring) = ⊤) :
    cosetRamificationNumberSum
        (base := base) (target := target) huniq H sigma z =
      intrinsicCosetRamificationNumberSum
        (base := base) (target := target) huniq H sigma
theorem

ramificationIndex_nsmul_fixedFieldRamificationNumber_eq_cosetSum

L129 ↗
RamificationTheory.HilbertRamification.Higher.ramificationIndex_nsmul_fixedFieldRamificationNumber_eq_cosetSum
Documentation

The quotient-depth identity (division-free normalized form).

For M = L ^ H and sigma' = sigma|_M,

e(L/M) * i_(M/K)(sigma') = sum_(tau in H) i_(L/K)(sigma tau).

The statement also covers the identity, where both sides are infinite.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem ramificationIndex_nsmul_fixedFieldRamificationNumber_eq_cosetSum
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) :
    fixedFieldRamificationIndex
          (target := target) H •
        fixedFieldRamificationNumber
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma) =
      intrinsicCosetRamificationNumberSum
        (base := base) (target := target) huniq H sigma

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.