NYLL
Module

HerbrandTheorem.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HerbrandTheorem
40 declarations indexed from sourceView source ↗

Module documentation

Herbrand's theorem for general discrete valuation fields

This leaf contains the completion-free endpoints of the Herbrand quotient theorem and the quotient and tower filtration theorems. The private lemmas below isolate the finite-group averaging argument used in the quotient-filtration comparison.

Imports7
Imported by2

Declarations

theorem

mem_lowerRamificationGroup_iff_ramificationNumber_dvf

L42 ↗
RamificationTheory.HilbertRamification.Higher.mem_lowerRamificationGroup_iff_ramificationNumber_dvf
Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 mem_lowerRamificationGroup_iff_ramificationNumber_dvf
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (s : ℝ) (sigma : Gal(L/K)) :
    sigma ∈ lowerRamificationGroup
        (base := base) (target := target) huniq s ↔
      (realRamificationExponent s : ℕ∞) ≤
        intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq sigma
theorem

realRamificationExponent_le_iff_add_one_le_dvf

L67 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent_le_iff_add_one_le_dvf
Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 realRamificationExponent_le_iff_add_one_le_dvf
    (s : ℝ) (n : ℕ) :
    realRamificationExponent s ≤ n ↔ s + 1 ≤ n
theorem

fixedFieldRamificationIdeal_antitone

L74 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationIdeal_antitone
Documentation

States the theorem fixedFieldRamificationIdeal_antitone.

Source context 12 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldRamificationIdeal_antitone
    (H : Subgroup Gal(L/K)) {s t : ℝ} (hst : s ≤ t) :
    fixedFieldRamificationIdealDVF
        (K := K) (target := target) H t ≤
      fixedFieldRamificationIdealDVF
        (K := K) (target := target) H s
theorem

fixedFieldLowerRamificationGroup_antitone

L83 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldLowerRamificationGroup_antitone
Documentation

States the theorem fixedFieldLowerRamificationGroup_antitone.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldLowerRamificationGroup_antitone
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    Antitone (fixedFieldLowerRamificationGroup
      (base := base) (target := target) huniq H)
theorem

fixedFieldLowerRamificationGroup_normal

L95 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldLowerRamificationGroup_normal
Documentation

States the theorem fixedFieldLowerRamificationGroup_normal.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldLowerRamificationGroup_normal
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    (fixedFieldLowerRamificationGroup
      (base := base) (target := target) huniq H s).Normal
def

fixedFieldLowerRamificationFiltration

L132 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldLowerRamificationFiltration
Documentation

The integral fixed-field lower groups, packaged as a lower filtration.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 · full declaration
def fixedFieldLowerRamificationFiltration
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    AntitoneNormalSubgroupFiltration Gal((fixedFieldDVF (K := K) H)/K) where
  lower n := fixedFieldLowerRamificationGroup
    (base := base) (target := target) huniq H (n : ℝ)
  lower_normal n :=
    fixedFieldLowerRamificationGroup_normal
      (base := base) (target := target) huniq H (n : ℝ)
  antitone := by
    intro m n hmn
    apply fixedFieldLowerRamificationGroup_antitone
      (base := base) (target := target) huniq H
    exact_mod_cast hmn
theorem

fixedFieldLowerRamificationFiltration_lower

L150 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldLowerRamificationFiltration_lower
Documentation

States the theorem fixedFieldLowerRamificationFiltration_lower.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldLowerRamificationFiltration_lower
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (n : ℕ) :
    (fixedFieldLowerRamificationFiltration
      (base := base) (target := target) huniq H).lower n =
      fixedFieldLowerRamificationGroup
        (base := base) (target := target) huniq H (n : ℝ)
def

fixedFieldHerbrandFunction

L162 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldHerbrandFunction
Documentation

Herbrand's eta function for the actual fixed extension (L ^ H)/K.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldHerbrandFunction
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) : ℝ
def

fixedFieldInverseHerbrandFunction

L171 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldInverseHerbrandFunction
Documentation

The inverse Herbrand function for the actual fixed extension.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldInverseHerbrandFunction
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) : ℝ
theorem

fixedFieldHerbrandFunction_inverseHerbrandFunction

L180 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldHerbrandFunction_inverseHerbrandFunction
Documentation

States the theorem fixedFieldHerbrandFunction_inverseHerbrandFunction.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldHerbrandFunction_inverseHerbrandFunction
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) :
    fixedFieldHerbrandFunction
        (base := base) (target := target) huniq H
        (fixedFieldInverseHerbrandFunction
          (base := base) (target := target) huniq H t) = t
theorem

fixedFieldInverseHerbrandFunction_herbrandFunction

L193 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldInverseHerbrandFunction_herbrandFunction
Documentation

States the theorem fixedFieldInverseHerbrandFunction_herbrandFunction.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldInverseHerbrandFunction_herbrandFunction
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    fixedFieldInverseHerbrandFunction
        (base := base) (target := target) huniq H
        (fixedFieldHerbrandFunction
          (base := base) (target := target) huniq H s) = s
theorem

fixedFieldHerbrandFunction_strictMono

L206 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldHerbrandFunction_strictMono
Documentation

States the theorem fixedFieldHerbrandFunction_strictMono.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldHerbrandFunction_strictMono
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    StrictMono (fixedFieldHerbrandFunction
      (base := base) (target := target) huniq H)
theorem

fixedFieldInverseHerbrandFunction_strictMono

L217 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldInverseHerbrandFunction_strictMono
Documentation

States the theorem fixedFieldInverseHerbrandFunction_strictMono.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldInverseHerbrandFunction_strictMono
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    StrictMono (fixedFieldInverseHerbrandFunction
      (base := base) (target := target) huniq H)
theorem

fixedFieldInverseHerbrandFunction_ge_neg_one_iff

L228 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldInverseHerbrandFunction_ge_neg_one_iff
Documentation

States the theorem fixedFieldInverseHerbrandFunction_ge_neg_one_iff.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldInverseHerbrandFunction_ge_neg_one_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] {t : ℝ} :
    -1 ≤ fixedFieldInverseHerbrandFunction
        (base := base) (target := target) huniq H t ↔ -1 ≤ t
def

fixedFieldUpperRamificationGroup

L239 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldUpperRamificationGroup
Documentation

Upper ramification groups of the actual fixed extension.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldUpperRamificationGroup
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) :
    Subgroup Gal((fixedFieldDVF (K := K) H)/K)
theorem

fixedFieldUpperRamificationGroup_herbrandFunction

L251 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldUpperRamificationGroup_herbrandFunction
Documentation

States the theorem fixedFieldUpperRamificationGroup_herbrandFunction.

Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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 fixedFieldUpperRamificationGroup_herbrandFunction
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    fixedFieldUpperRamificationGroup
        (base := base) (target := target) huniq H
        (fixedFieldHerbrandFunction
          (base := base) (target := target) huniq H s) =
      fixedFieldLowerRamificationGroup
        (base := base) (target := target) huniq H s
instance

lowerMembershipDecidable

L264 ↗
RamificationTheory.HilbertRamification.Higher.lowerMembershipDecidable
Source context 11 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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
instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n)
instance

finiteSubgroupFintype

L269 ↗
RamificationTheory.HilbertRamification.Higher.finiteSubgroupFintype
Source context 12 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
Lean source · statement
instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H
theorem

truncate_depth_eq_intrinsic_summand_of_mem

L273 ↗
RamificationTheory.HilbertRamification.Higher.truncate_depth_eq_intrinsic_summand_of_mem
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · full declaration
theorem truncate_depth_eq_intrinsic_summand_of_mem
    {G : Type*} [Group G] [Finite G]
    (F : AntitoneNormalSubgroupFiltration G) (depth : G → ℕ∞)
    (hmem : ∀ n sigma,
      sigma ∈ F.lower n ↔ (((n + 1 : ℕ) : ℕ∞) ≤ depth sigma))
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1)
    (sigma : F.lower 0) :
    truncateENatAtDVF (depth (sigma : G)) (s + 1) =
      1 + (F.truncatedLowerDepth m sigma : ℝ) +
        (s - m) * (if (sigma : G) ∈ F.lower (m + 1) then 1 else 0) := by
  classical
  let i := depth (sigma : G)
  have hi_one : (1 : ℕ∞) ≤ i := by
    simpa [i] using (hmem 0 (sigma : G)).1 sigma.property
  by_cases hhigh : ((m + 2 : ℕ) : ℕ∞) ≤ i
  · have hsigma : (sigma : G) ∈ F.lower (m + 1) := by
      apply (hmem (m + 1) (sigma : G)).2
      simpa [i, Nat.add_assoc] using hhigh
    have hdepth : F.truncatedLowerDepth m sigma = m := by
      rw [AntitoneNormalSubgroupFiltration.truncatedLowerDepth]
      rw [Finset.filter_eq_self.2]
      · simp
      · intro j hj
        apply (hmem (j + 1) (sigma : G)).2
        have hjm : j < m := Finset.mem_range.1 hj
        have hjle : ((j + 2 : ℕ) : ℕ∞) ≤ ((m + 2 : ℕ) : ℕ∞) :=
          ENat.natCast_le_natCast.2 (by omega)
        simpa [i, Nat.add_assoc] using hjle.trans hhigh
    have htrunc : truncateENatAtDVF i (s + 1) = s + 1 := by
      exact truncateENatAtDVF_eq_right_of_natCast_le
        (m := m + 2) (by
          norm_num [Nat.cast_add, Nat.cast_ofNat] at hsm ⊢
          linarith) hhigh
    rw [htrunc, hdepth]
    simp [hsigma]
    ring
  · have hlt : i < ((m + 2 : ℕ) : ℕ∞) := lt_of_not_ge hhigh
    have hine : i ≠ ⊤ := ne_top_of_lt hlt
    obtain ⟨k, hk⟩ := ENat.ne_top_iff_exists.1 hine
    have hk_one : 1 ≤ k := by
      exact_mod_cast (hi_one.trans_eq hk.symm)
    have hk_upper : k ≤ m + 1 := by
      have : k < m + 2 := by exact_mod_cast (hk.symm ▸ hlt)
      omega
    have hsigma : (sigma : G) ∉ F.lower (m + 1) := by
      intro hsigma
      apply hhigh
      simpa [i, Nat.add_assoc] using (hmem (m + 1) (sigma : G)).1 hsigma
    have hdepth : F.truncatedLowerDepth m sigma = k - 1 := by
      rw [AntitoneNormalSubgroupFiltration.truncatedLowerDepth]
      have hfilter :
          (Finset.range m).filter
              (fun j => (sigma : G) ∈ F.lower (j + 1)) =
            Finset.range (k - 1) := by
        ext j
        simp only [Finset.mem_filter, Finset.mem_range]
        have hthreshold :
            ((sigma : G) ∈ F.lower (j + 1)) ↔ j + 2 ≤ k := by
          rw [hmem]
          change (((j + 1 + 1 : ℕ) : ℕ∞) ≤ i) ↔ j + 2 ≤ k
          rw [← hk]
          norm_cast
        rw [hthreshold]
        omega
      rw [hfilter, Finset.card_range]
    have htrunc : truncateENatAtDVF i (s + 1) = k := by
      rw [← hk, truncateENatAtDVF_coe, min_eq_left]
      have : (k : ℝ) ≤ m + 1 := by exact_mod_cast hk_upper
      linarith
    rw [htrunc, hdepth]
    rw [ite_eq_right hsigma]
    simp only [mul_zero, add_zero]
    exact_mod_cast (by omega : k = 1 + (k - 1))
theorem

truncate_depth_eq_zero_of_not_mem_lower_zero

L347 ↗
RamificationTheory.HilbertRamification.Higher.truncate_depth_eq_zero_of_not_mem_lower_zero
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
theorem truncate_depth_eq_zero_of_not_mem_lower_zero
    {G : Type*} [Group G] [Finite G]
    (F : AntitoneNormalSubgroupFiltration G) (depth : G → ℕ∞)
    (hmem : ∀ n sigma,
      sigma ∈ F.lower n ↔ (((n + 1 : ℕ) : ℕ∞) ≤ depth sigma))
    {s : ℝ} (hs : -1 ≤ s) {sigma : G}
    (hsigma : sigma ∉ F.lower 0) :
    truncateENatAtDVF (depth sigma) (s + 1) = 0
theorem

sum_truncate_depth_eq_sum_lower_zero_of_mem

L364 ↗
RamificationTheory.HilbertRamification.Higher.sum_truncate_depth_eq_sum_lower_zero_of_mem
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
theorem sum_truncate_depth_eq_sum_lower_zero_of_mem
    {G : Type*} [Group G] [Fintype G]
    (F : AntitoneNormalSubgroupFiltration G) (depth : G → ℕ∞)
    (hmem : ∀ n sigma,
      sigma ∈ F.lower n ↔ (((n + 1 : ℕ) : ℕ∞) ≤ depth sigma))
    {s : ℝ} (hs : -1 ≤ s) :
    (∑ sigma : G, truncateENatAtDVF (depth sigma) (s + 1)) =
      ∑ sigma : F.lower 0,
        truncateENatAtDVF (depth (sigma : G)) (s + 1)
theorem

sum_lower_zero_truncate_depth_eq_intrinsic_of_mem

L393 ↗
RamificationTheory.HilbertRamification.Higher.sum_lower_zero_truncate_depth_eq_intrinsic_of_mem
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
theorem sum_lower_zero_truncate_depth_eq_intrinsic_of_mem
    {G : Type*} [Group G] [Finite G]
    (F : AntitoneNormalSubgroupFiltration G) (depth : G → ℕ∞)
    (hmem : ∀ n sigma,
      sigma ∈ F.lower n ↔ (((n + 1 : ℕ) : ℕ∞) ≤ depth sigma))
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (∑ sigma : F.lower 0,
        truncateENatAtDVF (depth (sigma : G)) (s + 1)) =
      Nat.card (F.lower 0) +
        (∑ sigma : F.lower 0, (F.truncatedLowerDepth m sigma : ℝ)) +
        (s - m) * Nat.card (F.lower (m + 1))
theorem

herbrandFunction_eq_depth_sum_of_mem

L422 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunction_eq_depth_sum_of_mem
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
    (herbrandFunction herbrandFunction_of_nonpos) in
Lean source · statement
theorem herbrandFunction_eq_depth_sum_of_mem
    {G : Type*} [Group G] [Fintype G]
    (F : AntitoneNormalSubgroupFiltration G) (depth : G → ℕ∞)
    (hmem : ∀ n sigma,
      sigma ∈ F.lower n ↔ (((n + 1 : ℕ) : ℕ∞) ≤ depth sigma))
    {s : ℝ} (hs : -1 ≤ s) :
    (herbrandFunction F) s =
      (1 / Nat.card (F.lower 0) : ℝ) *
        (∑ sigma : G, truncateENatAtDVF (depth sigma) (s + 1)) - 1
theorem

fixedField_herbrandFunction_formula_dvf

L462 ↗
RamificationTheory.HilbertRamification.Higher.fixedField_herbrandFunction_formula_dvf
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
theorem fixedField_herbrandFunction_formula_dvf
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] {s : ℝ} (hs : -1 ≤ s) :
    fixedFieldHerbrandFunction
        (base := base) (target := target) huniq H s =
      (1 / Nat.card ((fixedFieldLowerRamificationFiltration
        (base := base) (target := target) huniq H).lower 0) : ℝ) *
        (∑ q : Gal((fixedFieldDVF (K := K) H)/K),
          truncateENatAtDVF
            (fixedFieldRamificationNumber
              (base := base) (target := target) huniq H q) (s + 1)) - 1
instance

finiteQuotientFiberFintype

L487 ↗
RamificationTheory.HilbertRamification.Higher.finiteQuotientFiberFintype
Source context 13 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q)
theorem

truncate_depth_eq_intrinsic_summand

L492 ↗
RamificationTheory.HilbertRamification.Higher.truncate_depth_eq_intrinsic_summand
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · full declaration
theorem truncate_depth_eq_intrinsic_summand
    {G : Type*} [Group G] [Finite G]
    (D : NonarchimedeanDepth G) (H : Subgroup G) [H.Normal]
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1)
    (tau : (D.depthLowerFiltration H).lower 0) :
    truncateENatAtDVF (D.depth ((tau : H) : G)) (s + 1) =
      1 + ((D.depthLowerFiltration H).truncatedLowerDepth m tau : ℝ) +
        (s - m) *
          (if (tau : H) ∈ (D.depthLowerFiltration H).lower (m + 1)
            then 1 else 0) := by
  classical
  let F := D.depthLowerFiltration H
  let i := D.depth ((tau : H) : G)
  have hi_one : (1 : ℕ∞) ≤ i := tau.property
  by_cases hhigh : ((m + 2 : ℕ) : ℕ∞) ≤ i
  · have hmem : (tau : H) ∈
        (D.depthLowerFiltration H).lower (m + 1) := hhigh
    have hdepth : F.truncatedLowerDepth m tau = m := by
      rw [AntitoneNormalSubgroupFiltration.truncatedLowerDepth]
      rw [Finset.filter_eq_self.2]
      · simp
      · intro j hj
        change ((j + 2 : ℕ) : ℕ∞) ≤ i
        have hjm : j < m := Finset.mem_range.1 hj
        have hjm' : ((j + 2 : ℕ) : ℕ∞) ≤ ((m + 2 : ℕ) : ℕ∞) :=
          ENat.natCast_le_natCast.2 (by omega)
        exact hjm'.trans hhigh
    have htrunc : truncateENatAtDVF i (s + 1) = s + 1 := by
      exact truncateENatAtDVF_eq_right_of_natCast_le
        (m := m + 2) (by
          norm_num [Nat.cast_add, Nat.cast_ofNat] at hsm ⊢
          linarith) hhigh
    rw [htrunc, hdepth]
    rw [ite_eq_left hmem]
    ring
  · have hlt : i < ((m + 2 : ℕ) : ℕ∞) := lt_of_not_ge hhigh
    have hine : i ≠ ⊤ := ne_top_of_lt hlt
    obtain ⟨k, hk⟩ := ENat.ne_top_iff_exists.1 hine
    have hk_one : 1 ≤ k := by
      exact_mod_cast (hi_one.trans_eq hk.symm)
    have hk_upper : k ≤ m + 1 := by
      have : k < m + 2 := ENat.natCast_lt_natCast.1 (hk.symm ▸ hlt)
      omega
    have hmem : (tau : H) ∉
        (D.depthLowerFiltration H).lower (m + 1) := hhigh
    have hdepth : F.truncatedLowerDepth m tau = k - 1 := by
      rw [AntitoneNormalSubgroupFiltration.truncatedLowerDepth]
      have hfilter :
          (Finset.range m).filter
              (fun j => (tau : H) ∈ F.lower (j + 1)) =
            Finset.range (k - 1) := by
        ext j
        simp only [Finset.mem_filter, Finset.mem_range]
        have hthreshold :
            ((tau : H) ∈ F.lower (j + 1)) ↔ j + 2 ≤ k := by
          change (((j + 2 : ℕ) : ℕ∞) ≤ i) ↔ j + 2 ≤ k
          rw [← hk]
          norm_cast
        rw [hthreshold]
        omega
      rw [hfilter, Finset.card_range]
    have htrunc : truncateENatAtDVF i (s + 1) = k := by
      rw [← hk, truncateENatAtDVF_coe, min_eq_left]
      have : (k : ℝ) ≤ m + 1 := by exact_mod_cast hk_upper
      linarith
    rw [htrunc, hdepth]
    rw [ite_eq_right hmem]
    simp only [mul_zero, add_zero]
    exact_mod_cast (by omega : k = 1 + (k - 1))
theorem

sum_truncate_depth_eq_sum_lower_zero

L562 ↗
RamificationTheory.HilbertRamification.Higher.sum_truncate_depth_eq_sum_lower_zero
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem sum_truncate_depth_eq_sum_lower_zero
    {G : Type*} [Group G] [Finite G]
    (D : NonarchimedeanDepth G) (H : Subgroup G) [H.Normal]
    {s : ℝ} (hs : -1 ≤ s) :
    (∑ tau : H, truncateENatAtDVF (D.depth (tau : G)) (s + 1)) =
      ∑ tau : (D.depthLowerFiltration H).lower 0,
        truncateENatAtDVF (D.depth ((tau : H) : G)) (s + 1)
theorem

sum_lower_zero_truncate_depth_eq_intrinsic

L595 ↗
RamificationTheory.HilbertRamification.Higher.sum_lower_zero_truncate_depth_eq_intrinsic
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem sum_lower_zero_truncate_depth_eq_intrinsic
    {G : Type*} [Group G] [Finite G]
    (D : NonarchimedeanDepth G) (H : Subgroup G) [H.Normal]
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (∑ tau : (D.depthLowerFiltration H).lower 0,
        truncateENatAtDVF (D.depth ((tau : H) : G)) (s + 1)) =
      Nat.card ((D.depthLowerFiltration H).lower 0) +
        (∑ tau : (D.depthLowerFiltration H).lower 0,
          ((D.depthLowerFiltration H).truncatedLowerDepth m tau : ℝ)) +
        (s - m) * Nat.card ((D.depthLowerFiltration H).lower (m + 1))
theorem

depth_herbrandFunction_add_one_eq_average

L631 ↗
RamificationTheory.HilbertRamification.Higher.depth_herbrandFunction_add_one_eq_average
Documentation

The Herbrand-function sum formula for an abstract nonarchimedean depth, in the form used to compare the subgroup Herbrand parameter with a normalized depth sum.

Source context 15 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_of_nonpos
) in
Lean source · statement
theorem depth_herbrandFunction_add_one_eq_average
    {G : Type*} [Group G] [Finite G]
    (D : NonarchimedeanDepth G) (H : Subgroup G) [H.Normal]
    {s : ℝ} (hs : -1 ≤ s) :
    (D.depthLowerFiltration H).herbrandFunction s + 1 =
      (1 / D.depthRamificationIndex H : ℝ) *
        ∑ tau : H, truncateENatAtDVF (D.depth (tau : G)) (s + 1)
theorem

truncate_min_coe_eq_of_le

L671 ↗
RamificationTheory.HilbertRamification.Higher.truncate_min_coe_eq_of_le
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem truncate_min_coe_eq_of_le
    {i : ℕ∞} {m : ℕ} {r : ℝ} (hr : r ≤ m) :
    truncateENatAtDVF (min i (m : ℕ∞)) r = truncateENatAtDVF i r
theorem

min_quotientFiberAverage_eq_average_truncate

L688 ↗
RamificationTheory.HilbertRamification.Higher.min_quotientFiberAverage_eq_average_truncate
Documentation

Truncating a nontrivial quotient-fibre average at the subgroup Herbrand parameter equals the normalized sum of the truncated ambient depths.

Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem min_quotientFiberAverage_eq_average_truncate
    {G : Type*} [Group G] [Fintype G]
    (D : NonarchimedeanDepth G) (H : Subgroup G) [H.Normal]
    {q : G ⧸ H} (hq : q ≠ 1) {s : ℝ} (hs : -1 ≤ s) :
    min (D.quotientFiberAverage H hq)
        ((D.depthLowerFiltration H).herbrandFunction s + 1) =
      (1 / D.depthRamificationIndex H : ℝ) *
        ∑ gamma : NonarchimedeanDepth.QuotientFiber H q,
          truncateENatAtDVF (D.depth (gamma : G)) (s + 1)
theorem

subgroupFiltration_lower_eq_depthLowerFiltration_dvf

L796 ↗
RamificationTheory.HilbertRamification.Higher.subgroupFiltration_lower_eq_depthLowerFiltration_dvf
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem subgroupFiltration_lower_eq_depthLowerFiltration_dvf
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (n : ℕ) :
    ((lowerRamificationFiltrationOfUniqueExtension
      (base := base) (target := target) huniq).subgroupFiltration H).lower n =
      ((ramificationNumberDepthOfUniqueExtension
        (base := base) (target := target) huniq).depthLowerFiltration H).lower n
theorem

fixedFieldSubextension_herbrandFunction_eq_depth_dvf

L816 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldSubextension_herbrandFunction_eq_depth_dvf
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem fixedFieldSubextension_herbrandFunction_eq_depth_dvf
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    (fixedFieldSubextensionFiltration
      (lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq) H).herbrandFunction s =
      ((ramificationNumberDepthOfUniqueExtension
        (base := base) (target := target) huniq).depthLowerFiltration H).herbrandFunction s
theorem

card_fixedFieldSubextension_lower_eq_depth_dvf

L838 ↗
RamificationTheory.HilbertRamification.Higher.card_fixedFieldSubextension_lower_eq_depth_dvf
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem card_fixedFieldSubextension_lower_eq_depth_dvf
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (n : ℕ) :
    Nat.card ((fixedFieldSubextensionFiltration
      (lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq) H).lower n) =
      Nat.card (((ramificationNumberDepthOfUniqueExtension
        (base := base) (target := target) huniq).depthLowerFiltration H).lower n)
theorem

fixedFieldRamificationNumber_untop_eq_quotientFiberAverage

L859 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationNumber_untop_eq_quotientFiberAverage
Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem fixedFieldRamificationNumber_untop_eq_quotientFiberAverage
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) (hq : QuotientGroup.mk' H sigma ≠ 1) :
    ∃ hfinite :
        fixedFieldRamificationNumber
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma) ≠ ⊤,
      ((fixedFieldRamificationNumber
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma)).untop hfinite : ℝ) =
        (ramificationNumberDepthOfUniqueExtension
          (base := base) (target := target) huniq).quotientFiberAverage H hq
theorem

lowerRamificationGroup_quotient

L946 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_quotient
Documentation

The Herbrand quotient theorem over the stated discretely valued field hypotheses hypotheses. The image of the ambient lower group is the lower group of the actual fixed extension at the subgroup Herbrand parameter.

Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem lowerRamificationGroup_quotient
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    Subgroup.map (QuotientGroup.mk' H)
        (lowerRamificationGroup
          (base := base) (target := target) huniq s) =
      Subgroup.comap (IsGalois.normalAutEquivQuotient H).toMonoidHom
        (fixedFieldLowerRamificationGroup
          (base := base) (target := target) huniq H
          ((fixedFieldSubextensionFiltration
            (lowerRamificationFiltrationOfUniqueExtension
              (base := base) (target := target) huniq) H).herbrandFunction s))
theorem

herbrandFunction_trans_of_neg_one_le

L1074 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunction_trans_of_neg_one_le
Documentation

The quotient-filtration comparison over the stated discretely valued field hypotheses hypotheses: Herbrand eta is transitive in the actual fixed-field tower.

Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem herbrandFunction_trans_of_neg_one_le
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    {s : ℝ} (hs : -1 ≤ s) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq s =
      fixedFieldHerbrandFunction
        (base := base) (target := target) huniq H
        ((fixedFieldSubextensionFiltration
          (lowerRamificationFiltrationOfUniqueExtension
            (base := base) (target := target) huniq) H).herbrandFunction s)
theorem

herbrandFunction_trans

L1263 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunction_trans
Documentation

States the theorem herbrandFunction_trans.

Source context 15 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_of_nonpos
) in
Lean source · statement
theorem herbrandFunction_trans
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq s =
      fixedFieldHerbrandFunction
        (base := base) (target := target) huniq H
        ((fixedFieldSubextensionFiltration
          (lowerRamificationFiltrationOfUniqueExtension
            (base := base) (target := target) huniq) H).herbrandFunction s)
theorem

inverseHerbrandFunction_trans

L1298 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunction_trans
Documentation

The quotient-filtration comparison over the stated discretely valued field hypotheses hypotheses: inverse Herbrand functions compose in reverse tower order.

Source context 15 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_inverseHerbrandFunction
  herbrandFunction_strictMono
  inverseHerbrandFunction
) in
Lean source · statement
theorem inverseHerbrandFunction_trans
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) :
    inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq t =
      (fixedFieldSubextensionFiltration
        (lowerRamificationFiltrationOfUniqueExtension
          (base := base) (target := target) huniq) H).inverseHerbrandFunction
        (fixedFieldInverseHerbrandFunction
          (base := base) (target := target) huniq H t)
theorem

upperRamificationGroup_quotient

L1331 ↗
RamificationTheory.HilbertRamification.Higher.upperRamificationGroup_quotient
Documentation

The tower-filtration comparison over the stated discretely valued field hypotheses hypotheses: upper numbering is invariant under a Galois quotient.

Source context 14 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.HerbrandGroupTheory
universe u v w x
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]
noncomputable local instance lowerMembershipDecidable
    {G : Type*} [Group G] (F : AntitoneNormalSubgroupFiltration G)
    (n : ℕ) (sigma : G) : Decidable (sigma ∈ F.lower n) :=
  Classical.propDecidable _
noncomputable local instance finiteSubgroupFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance finiteQuotientFiberFintype
    {G : Type*} [Group G] [Finite G] (H : Subgroup G) [H.Normal]
    (q : G ⧸ H) : Fintype (NonarchimedeanDepth.QuotientFiber H q) :=
  Fintype.ofFinite _
Lean source · statement
theorem upperRamificationGroup_quotient
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) :
    Subgroup.map (QuotientGroup.mk' H)
        (upperRamificationGroupOfUniqueExtension
          (base := base) (target := target) huniq t) =
      Subgroup.comap (IsGalois.normalAutEquivQuotient H).toMonoidHom
        (fixedFieldUpperRamificationGroup
          (base := base) (target := target) huniq H t)

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