Module

ValueImage.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.ValueImage

12 declarations indexed from sourceView source ↗

Module documentation

Galois ramification value images

This file identifies the exact value images generated by embedded base units and their [M : L]-powered lower-branch images using Neu1999 Galois valuation data.

Imports1

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.Basic

Imported by3

theorem

galois_mapBaseUnitsToExtensionUnits_valuation_formula

L41 ↗

TameAbhyankar.NAField.galois_mapBaseUnitsToExtensionUnits_valuation_formula

Documentation

Neu1999's Galois valuation data, rewritten for the packaged MultiplicativeIntegerValuation: embedding a base unit into the extension multiplies its valuation by the supplied ramification index.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem galois_mapBaseUnitsToExtensionUnits_valuation_formula
    (x : Kˣ) :
    (multiplicativeIntegerValuation L).val
        (LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits K L x) =
      (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ) *
        (multiplicativeIntegerValuation K).val x

theorem

galois_mapBaseUnitsToExtensionUnits_uniformizer_val

L61 ↗

TameAbhyankar.NAField.galois_mapBaseUnitsToExtensionUnits_uniformizer_val

Documentation

A base uniformizer maps to an extension unit whose valuation is exactly the Galois ramification index supplied by Neu1999.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem galois_mapBaseUnitsToExtensionUnits_uniformizer_val
    {ϖ : Kˣ} (hϖ : (multiplicativeIntegerValuation K).IsUniformizer ϖ) :
    (multiplicativeIntegerValuation L).val
        (LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits K L ϖ) =
      (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

exists_baseUnitsImageSubgroup_val_galoisRamificationIndex

L71 ↗

TameAbhyankar.NAField.exists_baseUnitsImageSubgroup_val_galoisRamificationIndex

Documentation

A concrete embedded base unit generates the Neu1999 Galois ramification index in the extension valuation group.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_baseUnitsImageSubgroup_val_galoisRamificationIndex :
    ∃ x : Lˣ,
      x ∈ baseUnitsImageSubgroup (K := K) (L := L) ∧
        (multiplicativeIntegerValuation L).val x =
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

integerMultipleSubgroup_galoisRamificationIndex_le_baseUnitsImage

L86 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_galoisRamificationIndex_le_baseUnitsImage

Documentation

Subgroup-image form of the Galois ramification generator: the integer subgroup generated by the Neu1999 Galois ramification index lies in the value image of embedded base units.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem integerMultipleSubgroup_galoisRamificationIndex_le_baseUnitsImage :
    integerMultipleSubgroup
        (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ) ≤
      (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (baseUnitsImageSubgroup (K := K) (L := L))

theorem

baseUnitsImageSubgroup_valueImage_le_galoisRamificationIndex

L98 ↗

TameAbhyankar.NAField.baseUnitsImageSubgroup_valueImage_le_galoisRamificationIndex

Documentation

Every valuation value appearing on the embedded-base-unit subgroup is a multiple of the Neu1999 Galois ramification index.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem baseUnitsImageSubgroup_valueImage_le_galoisRamificationIndex :
    (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (baseUnitsImageSubgroup (K := K) (L := L)) ≤
      integerMultipleSubgroup
        (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

baseUnitsImageSubgroup_valueImage_eq_galoisRamificationIndex

L118 ↗

TameAbhyankar.NAField.baseUnitsImageSubgroup_valueImage_eq_galoisRamificationIndex

Documentation

Exact value image of the embedded-base-unit subgroup in a finite Galois Neu1999 local-field extension.

Source context 14 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem baseUnitsImageSubgroup_valueImage_eq_galoisRamificationIndex :
    (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (baseUnitsImageSubgroup (K := K) (L := L)) =
      integerMultipleSubgroup
        (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

exists_mem_fieldNormSubgroup_val_finrank_mul_galoisRamificationIndex

L136 ↗

TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_finrank_mul_galoisRamificationIndex

Documentation

A base uniformizer, embedded in L and then powered by [M : L], produces a concrete element of fieldNormSubgroup L M whose L-valuation is [M : L] times the Neu1999 Galois ramification index of L/K.

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem exists_mem_fieldNormSubgroup_val_finrank_mul_galoisRamificationIndex :
    ∃ x : Lˣ,
      x ∈ fieldNormSubgroup L M ∧
        (multiplicativeIntegerValuation L).val x =
          (Module.finrank L M : ℤ) *
            (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_fieldNormSubgroup

L157 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_fieldNormSubgroup

Documentation

Subgroup-image form of the powered norm generator. The integer subgroup generated by [M : L] * e_gal(L/K) lies in the value image of fieldNormSubgroup L M.

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_fieldNormSubgroup :
    integerMultipleSubgroup
        ((Module.finrank L M : ℤ) *
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)) ≤
      (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (fieldNormSubgroup L M)

theorem

exists_mem_poweredBaseUnitsImageSubgroup_val_finrank_mul_galoisRamificationIndex

L170 ↗

TameAbhyankar.NAField.exists_mem_poweredBaseUnitsImageSubgroup_val_finrank_mul_galoisRamificationIndex

Documentation

A concrete powered embedded base unit generates the value step [M : L] * e_gal(L/K).

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem exists_mem_poweredBaseUnitsImageSubgroup_val_finrank_mul_galoisRamificationIndex :
    ∃ x : Lˣ,
      x ∈ poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M) ∧
        (multiplicativeIntegerValuation L).val x =
          (Module.finrank L M : ℤ) *
            (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)

theorem

integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_poweredBaseUnitsImage

L191 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_poweredBaseUnitsImage

Documentation

The integer subgroup generated by [M : L] * e_gal(L/K) lies in the value image of the powered embedded-base-unit subgroup.

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_poweredBaseUnitsImage :
    integerMultipleSubgroup
        ((Module.finrank L M : ℤ) *
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)) ≤
      (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M))

theorem

poweredBaseUnitsImageSubgroup_valueImage_le_finrank_mul_galoisRamificationIndex

L204 ↗

TameAbhyankar.NAField.poweredBaseUnitsImageSubgroup_valueImage_le_finrank_mul_galoisRamificationIndex

Documentation

Every value appearing on the powered embedded-base-unit subgroup is a multiple of [M : L] * e_gal(L/K).

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem poweredBaseUnitsImageSubgroup_valueImage_le_finrank_mul_galoisRamificationIndex :
    (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) ≤
      integerMultipleSubgroup
        ((Module.finrank L M : ℤ) *
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ))

theorem

poweredBaseUnitsImageSubgroup_valueImage_eq_finrank_mul_galoisRamificationIndex

L237 ↗

TameAbhyankar.NAField.poweredBaseUnitsImageSubgroup_valueImage_eq_finrank_mul_galoisRamificationIndex

Documentation

Exact value image of the powered embedded-base-unit subgroup.

Source context 16 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
section NormTower
variable {M : Type u} [Field M] [Algebra L M]

Lean source · statement

theorem poweredBaseUnitsImageSubgroup_valueImage_eq_finrank_mul_galoisRamificationIndex :
    (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) =
      integerMultipleSubgroup
        ((Module.finrank L M : ℤ) *
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ))

Module documentation

Galois ramification value images

Declarations