NYLL
Module

LocalTop.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.LocalTop
6 declarations indexed from sourceView source ↗

Module documentation

Local-top comparisons for powered Galois ramification images

This file records the lower local-top residue-degree consequences forced by the powered embedded-base-unit image inside a field-norm subgroup.

Imports2
Imported by2

Declarations

theorem

residueDegree_dvd_finrank_mul_val_of_mem_baseUnitsImage_tower

L51 ↗
TameAbhyankar.NAField.residueDegree_dvd_finrank_mul_val_of_mem_baseUnitsImage_tower
Documentation

Any value generated by the embedded-base-unit image in L, after multiplication by [M : L], is divisible by the Neu1999 residue degree of M/L.

Source context 20 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] in
Lean source · statement
theorem residueDegree_dvd_finrank_mul_val_of_mem_baseUnitsImage_tower
    {x : Lˣ} (hx : x ∈ baseUnitsImageSubgroup (K := K) (L := L)) :
    (Module.finrank 𝓀[L] 𝓀[M] : ℤ) ∣
      (Module.finrank L M : ℤ) *
        (multiplicativeIntegerValuation L).val x
theorem

residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_val

L75 ↗
TameAbhyankar.NAField.residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_val
Documentation

Source-valued form of the lower-branch comparison: for every base unit x, the residue degree of M/L divides [M : L] * e_gal(L/K) * v_K(x).

Source context 19 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_val
    (x : Kˣ) :
    (Module.finrank 𝓀[L] 𝓀[M] : ℤ) ∣
      (Module.finrank L M : ℤ) *
        (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ) *
        (multiplicativeIntegerValuation K).val x
theorem

residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_int

L96 ↗
TameAbhyankar.NAField.residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_int
Documentation

Integer-valued form of the lower-branch comparison. Since the Neu1999 source valuation is onto ℤ, the previous source-valued divisibility holds for every integer value.

Source context 19 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem residueDegree_dvd_finrank_mul_galoisRamificationIndex_mul_int
    (n : ℤ) :
    (Module.finrank 𝓀[L] 𝓀[M] : ℤ) ∣
      (Module.finrank L M : ℤ) *
        (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ) *
        n
theorem

poweredBaseUnitsImageSubgroup_valueImage_le_residueDegree

L115 ↗
TameAbhyankar.NAField.poweredBaseUnitsImageSubgroup_valueImage_le_residueDegree
Documentation

The value image of the powered embedded-base-unit subgroup inherits the Neu1999 residue-degree value step from the field-norm subgroup.

Source context 20 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] in
Lean source · statement
theorem poweredBaseUnitsImageSubgroup_valueImage_le_residueDegree :
    (multiplicativeIntegerValuation L).subgroupValueSubgroup
        (poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) ≤
      integerMultipleSubgroup (Module.finrank 𝓀[L] 𝓀[M] : ℤ)
theorem

integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_residueDegree

L135 ↗
TameAbhyankar.NAField.integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_residueDegree
Documentation

Integer-multiple subgroup form of the powered lower-branch comparison: the subgroup generated by [M : L] * e_gal(L/K) lies in the value-step subgroup cut out by the residue degree of M/L.

Source context 19 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem integerMultipleSubgroup_finrank_mul_galoisRamificationIndex_le_residueDegree :
    integerMultipleSubgroup
        ((Module.finrank L M : ℤ) *
          (Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K] : ℤ)) ≤
      integerMultipleSubgroup (Module.finrank 𝓀[L] 𝓀[M] : ℤ)
theorem

residueDegree_dvd_finrank_mul_galoisRamificationIndex

L150 ↗
TameAbhyankar.NAField.residueDegree_dvd_finrank_mul_galoisRamificationIndex
Documentation

The powered ramification-image norm generator forces the Neu1999 residue degree of M/L to divide [M : L] * e_gal(L/K).

Source context 19 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 M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
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)]
variable [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField M]
variable [FiniteDimensional L M] [Algebra.IsSeparable L M]
variable [Valuation.HasExtension (ValuativeRel.valuation L)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem residueDegree_dvd_finrank_mul_galoisRamificationIndex :
    Module.finrank 𝓀[L] 𝓀[M] ∣
      Module.finrank L M *
        Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]

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