Module

FixedField.lean

Nyll.ValuedFieldTheory.Ramification.Herbrand.FixedField

9 declarations indexed from sourceView source ↗

Module documentation

Fixed-field group models for Herbrand towers

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.Ramification.Herbrand.Quotient
Mathlib.FieldTheory.Galois.Basic

Imported by2

def

fixedFieldSubextensionFiltration

L32 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldSubextensionFiltration

Documentation

The ambient subgroup filtration transported to the actual Galois group of L / L^H.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def fixedFieldSubextensionFiltration
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) :
    AntitoneNormalSubgroupFiltration Gal(L/IntermediateField.fixedField H)

theorem

fixedFieldSubextensionFiltration_lower

L41 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldSubextensionFiltration_lower

Documentation

States the theorem fixedFieldSubextensionFiltration_lower.

Source context 9 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem fixedFieldSubextensionFiltration_lower
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) (n : ℕ) :
    (fixedFieldSubextensionFiltration F H).lower n =
      ((F.lower n).comap H.subtype).comap
        (IntermediateField.subgroupEquivAlgEquiv H).symm.toMonoidHom

def

fixedFieldQuotientImageFiltration

L51 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldQuotientImageFiltration

Documentation

The quotient-image filtration transported to the actual Galois group of L^H / K.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def fixedFieldQuotientImageFiltration
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) [H.Normal] :
    AntitoneNormalSubgroupFiltration Gal(IntermediateField.fixedField H/K)

theorem

fixedFieldQuotientImageFiltration_lower

L58 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldQuotientImageFiltration_lower

Documentation

States the theorem fixedFieldQuotientImageFiltration_lower.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem fixedFieldQuotientImageFiltration_lower
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) [H.Normal] (n : ℕ) :
    (fixedFieldQuotientImageFiltration F H).lower n =
      ((F.lower n).map (QuotientGroup.mk' H)).comap
        (IsGalois.normalAutEquivQuotient H).symm.toMonoidHom

theorem

card_fixedFieldSubextension_mul_card_fixedFieldQuotientImage

L68 ↗

RamificationTheory.HilbertRamification.Higher.card_fixedFieldSubextension_mul_card_fixedFieldQuotientImage

Documentation

Exact cardinality factorization in the two actual fixed-field Galois group models.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem card_fixedFieldSubextension_mul_card_fixedFieldQuotientImage
    [Finite Gal(L/K)]
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) [H.Normal] (n : ℕ) :
    Nat.card ((fixedFieldSubextensionFiltration F H).lower n) *
        Nat.card ((fixedFieldQuotientImageFiltration F H).lower n) =
      Nat.card (F.lower n)

theorem

fixedFieldSubextension_herbrandFunction

L86 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldSubextension_herbrandFunction

Documentation

States the theorem fixedFieldSubextension_herbrandFunction.

Source context 9 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem fixedFieldSubextension_herbrandFunction
    [Finite Gal(L/K)]
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) (s : ℝ) :
    (herbrandFunction (fixedFieldSubextensionFiltration F H)) s =
      (herbrandFunction (subgroupFiltration F H)) s

theorem

fixedFieldSubextension_inverseHerbrandFunction

L100 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldSubextension_inverseHerbrandFunction

Documentation

States the theorem fixedFieldSubextension_inverseHerbrandFunction.

Source context 9 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem fixedFieldSubextension_inverseHerbrandFunction
    [Finite Gal(L/K)]
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) (t : ℝ) :
    (inverseHerbrandFunction (fixedFieldSubextensionFiltration F H)) t =
      (inverseHerbrandFunction (subgroupFiltration F H)) t

theorem

fixedFieldQuotientImage_herbrandFunction

L113 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldQuotientImage_herbrandFunction

Documentation

States the theorem fixedFieldQuotientImage_herbrandFunction.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem fixedFieldQuotientImage_herbrandFunction
    [Finite Gal(L/K)]
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) [H.Normal] (s : ℝ) :
    (herbrandFunction (fixedFieldQuotientImageFiltration F H)) s =
      (herbrandFunction (quotientImageFiltration F H)) s

theorem

fixedFieldQuotientImage_inverseHerbrandFunction

L125 ↗

RamificationTheory.HilbertRamification.Higher.fixedFieldQuotientImage_inverseHerbrandFunction

Documentation

States the theorem fixedFieldQuotientImage_inverseHerbrandFunction.

Source context 8 commands

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

noncomputable section
universe u w
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField
open RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem fixedFieldQuotientImage_inverseHerbrandFunction
    [Finite Gal(L/K)]
    (F : AntitoneNormalSubgroupFiltration Gal(L/K))
    (H : Subgroup Gal(L/K)) [H.Normal] (t : ℝ) :
    (inverseHerbrandFunction (fixedFieldQuotientImageFiltration F H)) t =
      (inverseHerbrandFunction (quotientImageFiltration F H)) t

Module documentation

Fixed-field group models for Herbrand towers

Declarations