NYLL
Module

ResidueDegree.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.ResidueDegree
10 declarations indexed from sourceView source ↗

Module documentation

Neu1999 residue-degree lcm divisibility

This file extracts concrete residue-degree divisibility from the Neu1999 field-norm value-image comparison.

Imports3
Imported by1

Declarations

theorem

lcm_residueDegree_dvd_common_residueDegree_towers

L60 ↗
TameAbhyankar.NAField.lcm_residueDegree_dvd_common_residueDegree_towers
Documentation

Common-top residue-degree divisibility generated by the Neu1999 field-norm value images. The valuation image of N_{M/K}(Mˣ) is generated by f(K,M), while the same image lies in the lcm value-step subgroup generated by f(K,L) and f(K,L').

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem lcm_residueDegree_dvd_common_residueDegree_towers :
    ((((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
      (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) : ℤ) ∣
        (Module.finrank 𝓀[K] 𝓀[M] : ℤ))
theorem

intLcm_residueDegree_dvd_common_residueDegree_towers_nat

L84 ↗
TameAbhyankar.NAField.intLcm_residueDegree_dvd_common_residueDegree_towers_nat
Documentation

Nat divisibility form of lcm_residueDegree_dvd_common_residueDegree_towers, keeping the same integer-lcm source step on the left.

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem intLcm_residueDegree_dvd_common_residueDegree_towers_nat :
    ((Module.finrank 𝓀[K] 𝓀[L] : ℤ).lcm
      (Module.finrank 𝓀[K] 𝓀[L'] : ℤ) : ℕ) ∣
        Module.finrank 𝓀[K] 𝓀[M]
theorem

nat_lcm_residueDegree_dvd_common_residueDegree_towers

L94 ↗
TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_common_residueDegree_towers
Documentation

Standard Nat.lcm form of the common-top Neu1999 residue-degree divisibility.

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem nat_lcm_residueDegree_dvd_common_residueDegree_towers :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank 𝓀[K] 𝓀[M]
theorem

nat_lcm_residueDegree_dvd_common_residueDegree_towers_from_norm_generator

L106 ↗
TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_common_residueDegree_towers_from_norm_generator
Documentation

Element-generator proof of the common-top residue-degree divisibility: fieldNormSubgroup K M contains an element of valuation f(K,M), and the common-top norm-image theorem forces that valuation to be divisible by the lower residue-degree lcm.

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem nat_lcm_residueDegree_dvd_common_residueDegree_towers_from_norm_generator :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank 𝓀[K] 𝓀[M]
theorem

nat_lcm_residueDegree_dvd_common_finrank_towers

L119 ↗
TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_common_finrank_towers
Documentation

The common-top field degree is also divisible by the lower residue-degree lcm, because Neu1999's common residue degree divides [M : K].

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem nat_lcm_residueDegree_dvd_common_finrank_towers :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M
theorem

ramificationIndex_mul_nat_lcm_residueDegree_dvd_common_finrank_towers

L132 ↗
TameAbhyankar.NAField.ramificationIndex_mul_nat_lcm_residueDegree_dvd_common_finrank_towers
Documentation

The common-top field degree is divisible by the common-top ramification index times the lower residue-degree lcm. This is the Neu1999 e * f = [M : K] relation applied after the norm-image theorem produces lcm (f K L) (f K L') ∣ f K M.

Source context 28 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem ramificationIndex_mul_nat_lcm_residueDegree_dvd_common_finrank_towers :
    (𝓂[M] : Ideal 𝒪[M]).ramificationIdx 𝒪[K] *
        Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
          (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M
theorem

nat_lcm_residueDegree_dvd_common_finrank_towers_from_base_norm

L152 ↗
TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_common_finrank_towers_from_base_norm
Documentation

Element-generator proof of the common-top field-degree divisibility: the base uniformizer produces a concrete member of fieldNormSubgroup K M with valuation [M : K], and the common-top norm-image theorem forces the same valuation to be divisible by the lower residue-degree lcm.

Source context 29 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 CommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M]
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K L']
variable [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
omit [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M]
    [FiniteDimensional K M] [Algebra.IsSeparable K M]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation M)] in
Lean source · statement
theorem nat_lcm_residueDegree_dvd_common_finrank_towers_from_base_norm :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M
theorem

nat_lcm_galoisResidueDegree_dvd_common_residueDegree_towers

L194 ↗
TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_common_residueDegree_towers
Documentation

With both lower branches supplied by Neu1999 Galois valuation data, the common-top residue degree is divisible by the lcm of the lower Galois residue degrees.

Source context 27 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 GaloisLowerCommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M] [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem nat_lcm_galoisResidueDegree_dvd_common_residueDegree_towers :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank 𝓀[K] 𝓀[M]
theorem

nat_lcm_galoisResidueDegree_dvd_common_finrank_towers

L204 ↗
TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_common_finrank_towers
Documentation

Field-degree form of the Galois lower-branch residue-degree lcm source.

Source context 27 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 GaloisLowerCommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M] [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem nat_lcm_galoisResidueDegree_dvd_common_finrank_towers :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M
theorem

ramificationIndex_mul_nat_lcm_galoisResidueDegree_dvd_common_finrank_towers

L216 ↗
TameAbhyankar.NAField.ramificationIndex_mul_nat_lcm_galoisResidueDegree_dvd_common_finrank_towers
Documentation

The common-top ramification index times the lower Galois residue-degree lcm divides the common-top field degree.

Source context 27 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 GaloisLowerCommonTopResidueDegree
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] [ValuativeRel M] [TopologicalSpace M]
variable [IsNonarchimedeanLocalField 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 [FiniteDimensional K M] [Algebra.IsSeparable K M]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation M)]
Lean source · statement
theorem ramificationIndex_mul_nat_lcm_galoisResidueDegree_dvd_common_finrank_towers :
    (𝓂[M] : Ideal 𝒪[M]).ramificationIdx 𝒪[K] *
        Nat.lcm
          (Module.finrank 𝓀[K] 𝓀[L])
          (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M

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