NYLL
Module

FieldNormImage.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.FieldNormImage
12 declarations indexed from sourceView source ↗

Module documentation

Neu1999 field-norm value images

This file specializes the generic field-norm image lemmas to Neu1999 local fields. It keeps the arbitrary subgroup and generator forms close to the frontier where the actual ramification-image subgroup will be constructed.

Imports1
Imported by3

Declarations

theorem

fieldNormSubgroup_valueImage_eq_residueDegree

L31 ↗
TameAbhyankar.NAField.fieldNormSubgroup_valueImage_eq_residueDegree
Documentation

For a single Neu1999 local-field extension, the valuation image of the field-norm subgroup is exactly the integer subgroup generated by the Neu1999 residue degree.

Source context 6 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
Lean source · statement
theorem fieldNormSubgroup_valueImage_eq_residueDegree
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (fieldNormSubgroup K L) =
      integerMultipleSubgroup (Module.finrank 𝓀[K] 𝓀[L] : ℤ)
theorem

exists_mem_fieldNormSubgroup_val_iff_residueDegree_dvd

L65 ↗
TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_iff_residueDegree_dvd
Documentation

Elementwise form of fieldNormSubgroup_valueImage_eq_residueDegree: a base valuation value occurs on the field-norm subgroup exactly when it is divisible by the Neu1999 residue degree.

Source context 6 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
Lean source · statement
theorem exists_mem_fieldNormSubgroup_val_iff_residueDegree_dvd
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    (n : ℤ) :
    (∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧
        (multiplicativeIntegerValuation K).val x = n) ↔
      (Module.finrank 𝓀[K] 𝓀[L] : ℤ) ∣ n
theorem

exists_mem_fieldNormSubgroup_val_nat_iff_residueDegree_dvd

L110 ↗
TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_nat_iff_residueDegree_dvd
Documentation

Natural-number form of exists_mem_fieldNormSubgroup_val_iff_residueDegree_dvd.

Source context 6 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
Lean source · statement
theorem exists_mem_fieldNormSubgroup_val_nat_iff_residueDegree_dvd
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    (n : ℕ) :
    (∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧
        (multiplicativeIntegerValuation K).val x = (n : ℤ)) ↔
      Module.finrank 𝓀[K] 𝓀[L] ∣ n
theorem

exists_mem_fieldNormSubgroup_val_residueDegree

L129 ↗
TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_residueDegree
Documentation

A single Neu1999 field-norm subgroup contains an element whose base valuation is exactly the residue degree.

Source context 6 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
Lean source · statement
theorem exists_mem_fieldNormSubgroup_val_residueDegree
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    ∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧
      (multiplicativeIntegerValuation K).val x =
        (Module.finrank 𝓀[K] 𝓀[L] : ℤ)
theorem

fieldNormSubgroup_valueImage_le_lcm_towers

L170 ↗
TameAbhyankar.NAField.fieldNormSubgroup_valueImage_le_lcm_towers
Documentation

Neu1999 local-field specialization of the common-top field-norm image theorem: the base valuation image of N_{M/K}(Mˣ) is cut out by the lcm of the two lower Neu1999 residue degrees.

Source context 24 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
section TwoLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem fieldNormSubgroup_valueImage_le_lcm_towers :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (fieldNormSubgroup K M) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

subgroupValueSubgroup_le_lcm_of_le_fieldNormSubgroup_towers

L189 ↗
TameAbhyankar.NAField.subgroupValueSubgroup_le_lcm_of_le_fieldNormSubgroup_towers
Documentation

Any Neu1999 subgroup contained in the common-top field-norm subgroup inherits the lcm value-step inclusion. This is the immediate input shape for the actual ramification-image subgroup.

Source context 24 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
section TwoLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem subgroupValueSubgroup_le_lcm_of_le_fieldNormSubgroup_towers
    {S : Subgroup Kˣ} (hS : S ≤ fieldNormSubgroup K M) :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup S ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

lcm_residueDegree_dvd_of_exists_mem_val_of_le_fieldNormSubgroup_towers

L208 ↗
TameAbhyankar.NAField.lcm_residueDegree_dvd_of_exists_mem_val_of_le_fieldNormSubgroup_towers
Documentation

Generator form for the next ramification-image step: once an element of a subgroup contained in N_{M/K}(Mˣ) has valuation n, that valuation is divisible by the lcm of the two lower Neu1999 residue degrees.

Source context 24 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
section TwoLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem lcm_residueDegree_dvd_of_exists_mem_val_of_le_fieldNormSubgroup_towers
    {S : Subgroup Kˣ} {n : ℤ}
    (hn :
      ∃ x : Kˣ, x ∈ S ∧
        (multiplicativeIntegerValuation K).val x = n)
    (hS : S ≤ fieldNormSubgroup K M) :
    ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
      (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ) ∣ n)
theorem

intLcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers

L235 ↗
TameAbhyankar.NAField.intLcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers
Documentation

Nat form of lcm_residueDegree_dvd_of_exists_mem_val_of_le_fieldNormSubgroup_towers, keeping the same integer-lcm source step.

Source context 24 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
section TwoLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem intLcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers
    {S : Subgroup Kˣ} {n : ℕ}
    (hn :
      ∃ x : Kˣ, x ∈ S ∧
        (multiplicativeIntegerValuation K).val x = (n : ℤ))
    (hS : S ≤ fieldNormSubgroup K M) :
    ((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
      (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) ∣ n
theorem

nat_lcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers

L249 ↗
TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers
Documentation

Standard Nat.lcm form of the Neu1999 subgroup-generator divisibility. This is the shape expected by the ramification-index arithmetic layer.

Source context 24 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
section TwoLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem nat_lcm_residueDegree_dvd_nat_of_exists_mem_val_of_le_fieldNormSubgroup_towers
    {S : Subgroup Kˣ} {n : ℕ}
    (hn :
      ∃ x : Kˣ, x ∈ S ∧
        (multiplicativeIntegerValuation K).val x = (n : ℤ))
    (hS : S ≤ fieldNormSubgroup K M) :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣ n
theorem

fieldNormSubgroup_valueImage_le_galoisResidueDegree_lcm_towers

L288 ↗
TameAbhyankar.NAField.fieldNormSubgroup_valueImage_le_galoisResidueDegree_lcm_towers
Documentation

If both lower branches are supplied by Neu1999 Galois valuation data, the common-top field-norm value image is cut out by the lcm of the two Galois residue degrees.

Source context 24 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
section GaloisLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [IsGalois K L] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem fieldNormSubgroup_valueImage_le_galoisResidueDegree_lcm_towers :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (fieldNormSubgroup K M) ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

subgroupValueSubgroup_le_galoisResidueDegree_lcm_of_le_fieldNormSubgroup

L300 ↗
TameAbhyankar.NAField.subgroupValueSubgroup_le_galoisResidueDegree_lcm_of_le_fieldNormSubgroup
Documentation

Any subgroup already contained in the common-top norm subgroup inherits the Galois-residue-degree lcm value-step inclusion.

Source context 24 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
section GaloisLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [IsGalois K L] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem subgroupValueSubgroup_le_galoisResidueDegree_lcm_of_le_fieldNormSubgroup
    {S : Subgroup Kˣ} (hS : S ≤ fieldNormSubgroup K M) :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup S ≤
      integerMultipleSubgroup
        ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
          (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ))
theorem

nat_lcm_galoisResidueDegree_dvd_nat_of_mem_le_fieldNormSubgroup

L312 ↗
TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_nat_of_mem_le_fieldNormSubgroup
Documentation

Generator form for a subgroup of the common-top norm subgroup, with both lower residue degrees supplied by Neu1999 Galois valuation data.

Source context 24 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
section GaloisLowerTowers
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]
variable [FiniteDimensional K L] [FiniteDimensional K L']
variable [IsGalois K L] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
Lean source · statement
theorem nat_lcm_galoisResidueDegree_dvd_nat_of_mem_le_fieldNormSubgroup
    {S : Subgroup Kˣ} {n : ℕ}
    (hn :
      ∃ x : Kˣ, x ∈ S ∧
        (multiplicativeIntegerValuation K).val x = (n : ℤ))
    (hS : S ≤ fieldNormSubgroup K M) :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣ n

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