NYLL
Module

FixedFieldRamificationIndex.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FixedFieldRamificationIndex
11 declarations indexed from sourceView source ↗

Module documentation

The ramification index of an actual fixed field over a general DVF

For M = L ^ H, this file defines e(L/M) from the literal inclusion O_M = O_L ∩ M → O_L. The definition and its comparison with the zeroth depth subgroup require no completeness or Henselian hypothesis.

Imports4
Imported by2

Declarations

def

fixedFieldRamificationIndex

L39 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationIndex
Documentation

The ramification index of L/(L ^ H), formed from the literal inclusion of the restricted fixed-field valuation ring into the top valuation ring.

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
open scoped Pointwise
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 fixedFieldRamificationIndex
    (H : Subgroup Gal(L/K)) : ℕ
theorem

map_fixedField_maximalIdeal_eq_pow_ramificationIndex

L51 ↗
RamificationTheory.HilbertRamification.Higher.map_fixedField_maximalIdeal_eq_pow_ramificationIndex
Documentation

The image of the fixed-field maximal ideal is the power of the top maximal ideal indexed by the literal ramification index.

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
open scoped Pointwise
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
theorem map_fixedField_maximalIdeal_eq_pow_ramificationIndex
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    Ideal.map
        (fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H)
        (IsLocalRing.maximalIdeal
          (fixedFieldValuationSubringDVF (K := K) (target := target) H)) =
      target.maximalIdeal ^
        fixedFieldRamificationIndex
          (target := target) H
theorem

isUnit_fixedFieldValuationSubringDVFToTarget_iff

L101 ↗
RamificationTheory.HilbertRamification.Higher.isUnit_fixedFieldValuationSubringDVFToTarget_iff
Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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 [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem isUnit_fixedFieldValuationSubringDVFToTarget_iff
    (H : Subgroup Gal(L/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    IsUnit
        (fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H a) ↔
      IsUnit a
theorem

fixedFieldRamificationIndex_ne_zero

L134 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationIndex_ne_zero
Documentation

States the theorem fixedFieldRamificationIndex_ne_zero.

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
open scoped Pointwise
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
theorem fixedFieldRamificationIndex_ne_zero
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    fixedFieldRamificationIndex
        (target := target) H ≠ 0
theorem

addVal_fixedFieldValuationSubringToTarget_eq_ramificationIndex_nsmul

L176 ↗
RamificationTheory.HilbertRamification.Higher.addVal_fixedFieldValuationSubringToTarget_eq_ramificationIndex_nsmul
Documentation

The normalized additive valuation on the top valuation ring restricts to the ramification index times the normalized additive valuation on the literal fixed-field valuation ring.

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
open scoped Pointwise
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
theorem addVal_fixedFieldValuationSubringToTarget_eq_ramificationIndex_nsmul
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H a) =
      fixedFieldRamificationIndex
          (target := target) H •
        (@IsDiscreteValuationRing.addVal
          (fixedFieldValuationSubringDVF (K := K) (target := target) H)
          inferInstance inferInstance
          (fixedFieldValuationSubringDVF_isDiscreteValuationRing
            (base := base) (target := target) huniq H)) a
def

fixedFieldTopValuationSubringActionHomDVF

L253 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldTopValuationSubringActionHomDVF
Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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 [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
def fixedFieldTopValuationSubringActionHomDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) :
    H →* (target.valuationSubring ≃+* target.valuationSubring) where
  toFun tau := valuationSubringAutOfUniqueExtension
    (base := base) (target := target) huniq (tau : Gal(L/K))
  map_one' := by
    ext a
    simp
  map_mul' sigma tau := by
    ext a
    simp
def

fixedFieldInertiaSubgroupDVF

L268 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldInertiaSubgroupDVF
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
open scoped Pointwise
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 fixedFieldInertiaSubgroupDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) : Subgroup H
theorem

depthLowerFiltration_zero_eq_fixedFieldInertiaSubgroupDVF

L287 ↗
RamificationTheory.HilbertRamification.Higher.depthLowerFiltration_zero_eq_fixedFieldInertiaSubgroupDVF
Documentation

The zeroth subgroup cut out by the canonical general-DVF depth is the inertia subgroup for the action of H on the top valuation ring.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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]
open _root_.RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth (
  depthLowerFiltration_lower
  mem_depthLowerSubgroup_iff
) in
Lean source · statement
theorem depthLowerFiltration_zero_eq_fixedFieldInertiaSubgroupDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    ((ramificationNumberDepthOfUniqueExtension
        (base := base) (target := target) huniq).depthLowerFiltration H).lower 0 =
      fixedFieldInertiaSubgroupDVF
        (base := base) (target := target) huniq H
theorem

card_stabilizer_eq_inertia_mul_inertiaDeg

L322 ↗
RamificationTheory.HilbertRamification.Higher.card_stabilizer_eq_inertia_mul_inertiaDeg
Documentation

Computes a decomposition-group stabilizer from inertia and residue degree when the induced residue extension is separable.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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 card_stabilizer_eq_inertia_mul_inertiaDeg
    {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Group G] [Finite G] [MulSemiringAction G S] [IsGaloisGroup G R S]
    (p : Ideal R) [p.IsPrime] [p.IsMaximal]
    (P : Ideal S) [P.LiesOver p] [P.IsPrime] [P.IsMaximal]
    [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    Nat.card (MulAction.stabilizer G P) =
      Nat.card (Ideal.inertia G P) * P.inertiaDeg R
theorem

card_inertia_eq_ramificationIdxIn

L388 ↗
RamificationTheory.HilbertRamification.Higher.card_inertia_eq_ramificationIdxIn
Documentation

Identifies the finite inertia cardinality with the ramification index without assuming that the base residue field is perfect.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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 card_inertia_eq_ramificationIdxIn
    {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Group G] [Finite G] [MulSemiringAction G S] [IsGaloisGroup G R S]
    [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S]
    (p : Ideal R) (P : Ideal S) [P.LiesOver p]
    [p.IsPrime] [p.IsMaximal] [P.IsPrime] [P.IsMaximal]
    [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] :
    Nat.card (Ideal.inertia G P) =
      Ideal.ramificationIdxIn p S
theorem

fixedFieldRamificationIndex_eq_card_depthLowerFiltration_zero

L434 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationIndex_eq_card_depthLowerFiltration_zero
Documentation

The literal ramification index of L/(L^H) is the cardinality of the zeroth subgroup induced on H by the canonical general-DVF depth.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Pointwise
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 fixedFieldRamificationIndex_eq_card_depthLowerFiltration_zero
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    fixedFieldRamificationIndex
        (target := target) H =
      Nat.card
        (((ramificationNumberDepthOfUniqueExtension
          (base := base) (target := target) huniq).depthLowerFiltration H).lower 0)

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