NYLL
Module

Invariants.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Invariants
8 declarations indexed from sourceView source ↗

Module documentation

Local-field extension invariants

This file exposes the elementary divisibility consequences of the canonical ramification identity e * f = [L : K] for finite separable nonarchimedean local-field extensions.

Imports2
Imported by4

Declarations

theorem

ramificationIndex_mul_residueDegree_eq_finrank

L44 ↗
TameAbhyankar.NAField.ramificationIndex_mul_residueDegree_eq_finrank
Documentation

The canonical ramification and residue degrees multiply to the field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem ramificationIndex_mul_residueDegree_eq_finrank :
    e[K,L] * f[K,L] = Module.finrank K L
theorem

ramificationIndex_dvd_finrank

L59 ↗
TameAbhyankar.NAField.ramificationIndex_dvd_finrank
Documentation

The canonical ramification index divides the field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem ramificationIndex_dvd_finrank :
    e[K,L] ∣ Module.finrank K L
theorem

residueDegree_dvd_finrank

L65 ↗
TameAbhyankar.NAField.residueDegree_dvd_finrank
Documentation

The canonical residue degree divides the field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem residueDegree_dvd_finrank :
    f[K,L] ∣ Module.finrank K L
theorem

ramificationIndex_pos

L75 ↗
TameAbhyankar.NAField.ramificationIndex_pos
Documentation

The ramification index of a finite local-field extension is positive.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem ramificationIndex_pos :
    0 < e[K,L]
theorem

residueDegree_pos

L85 ↗
TameAbhyankar.NAField.residueDegree_pos
Documentation

The residue degree of a finite local-field extension is positive.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem residueDegree_pos :
    0 < f[K,L]
theorem

ramificationIndex_mul_dvd_finrank_of_dvd_residueDegree

L96 ↗
TameAbhyankar.NAField.ramificationIndex_mul_dvd_finrank_of_dvd_residueDegree
Documentation

Any divisor of the residue degree can be paired with the ramification index to divide the field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem ramificationIndex_mul_dvd_finrank_of_dvd_residueDegree {d : ℕ}
    (hd : d ∣ f[K,L]) :
    e[K,L] * d ∣ Module.finrank K L
theorem

ramificationIndex_eq_finrank_of_residueDegree_eq_one

L109 ↗
TameAbhyankar.NAField.ramificationIndex_eq_finrank_of_residueDegree_eq_one
Documentation

If the residue degree is one, the ramification index is the whole field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem ramificationIndex_eq_finrank_of_residueDegree_eq_one
    (hf : f[K,L] = 1) :
    e[K,L] = Module.finrank K L
theorem

residueDegree_eq_finrank_of_ramificationIndex_eq_one

L116 ↗
TameAbhyankar.NAField.residueDegree_eq_finrank_of_ramificationIndex_eq_one
Documentation

If the ramification index is one, the residue degree is the whole field degree.

Source context 15 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open scoped ValuativeRel
namespace NAField
local notation "e[" K "," L "]" =>
  Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
local notation "f[" K "," L "]" => Module.finrank 𝓀[K] 𝓀[L]
variable {K L : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
Lean source · statement
theorem residueDegree_eq_finrank_of_ramificationIndex_eq_one
    (he : e[K,L] = 1) :
    f[K,L] = Module.finrank K L

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