NYLL
Module

RamificationIdeal.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.RamificationIdeal
13 declarations indexed from sourceView source ↗

Module documentation

Ramification ideals in finite complete-DVF extensions

This file records the ideal-theoretic source behind the local-field structure theory. The base maximal ideal maps to the e-th power of the target maximal ideal, where e is the canonical ramification index. Every statement is expressed directly in the ambient valued-extension context; no extension marker is involved.

Imports1
Imported by8

Declarations

theorem

target_maximalIdeal_pow_not_le_pow_succ

L37 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.target_maximalIdeal_pow_not_le_pow_succ
Documentation

No power of the target maximal ideal is contained in the next power.

This is the ideal-level form of the uniformizer-power separation lemma.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem target_maximalIdeal_pow_not_le_pow_succ
    {π : target.valuationSubring}
    (hπ : target.valuation.IsUniformizer (π : L)) (n : ℕ) :
    ¬ target.maximalIdeal ^ n ≤ target.maximalIdeal ^ (n + 1)
theorem

maximalIdeal_map_eq_target_maximalIdeal_pow_ramificationIndex

L50 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_map_eq_target_maximalIdeal_pow_ramificationIndex
Documentation

The image of the base maximal ideal is the e-th power of the target maximal ideal.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem maximalIdeal_map_eq_target_maximalIdeal_pow_ramificationIndex :
    Ideal.map (integerMap base.toDVF target.toDVF) base.maximalIdeal =
      target.maximalIdeal ^ ramificationIndex base.toDVF target.toDVF
theorem

maximalIdeal_pow_map_eq_target_maximalIdeal_pow_mul_ramificationIndex

L77 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_pow_map_eq_target_maximalIdeal_pow_mul_ramificationIndex
Documentation

The image of the n-th power of the base maximal ideal is the (e*n)-th power of the target maximal ideal.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem maximalIdeal_pow_map_eq_target_maximalIdeal_pow_mul_ramificationIndex
    (n : ℕ) :
    Ideal.map (integerMap base.toDVF target.toDVF) (base.maximalIdeal ^ n) =
      target.maximalIdeal ^ (ramificationIndex base.toDVF target.toDVF * n)
theorem

integerMap_mem_target_maximalIdeal_pow_mul_ramificationIndex

L91 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.integerMap_mem_target_maximalIdeal_pow_mul_ramificationIndex
Documentation

Elements in m_K^n map into m_L^(e*n).

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem integerMap_mem_target_maximalIdeal_pow_mul_ramificationIndex
    {n : ℕ} {x : base.valuationSubring}
    (hx : x ∈ base.maximalIdeal ^ n) :
    integerMap base.toDVF target.toDVF x ∈
      target.maximalIdeal ^ (ramificationIndex base.toDVF target.toDVF * n)
theorem

maximalIdeal_pow_map_not_le_target_next_pow_mul_ramificationIndex

L102 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_pow_map_not_le_target_next_pow_mul_ramificationIndex
Documentation

The image of m_K^n is not contained in the next target maximal-ideal power after m_L^(e*n).

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem maximalIdeal_pow_map_not_le_target_next_pow_mul_ramificationIndex
    (n : ℕ) :
    ¬ Ideal.map (integerMap base.toDVF target.toDVF) (base.maximalIdeal ^ n) ≤
      target.maximalIdeal ^
        (ramificationIndex base.toDVF target.toDVF * n + 1)
theorem

span_base_uniformizer_image_eq_target_maximalIdeal_pow_ramificationIndex

L115 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.span_base_uniformizer_image_eq_target_maximalIdeal_pow_ramificationIndex
Documentation

The image of a base uniformizer generates the e-th target maximal-ideal power.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem span_base_uniformizer_image_eq_target_maximalIdeal_pow_ramificationIndex
    {ϖ : base.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K)) :
    Ideal.span ({integerMap base.toDVF target.toDVF ϖ} :
        Set target.valuationSubring) =
      target.maximalIdeal ^ ramificationIndex base.toDVF target.toDVF
theorem

span_base_uniformizer_pow_image_eq_target_maximalIdeal_pow_mul_ramificationIndex

L134 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.span_base_uniformizer_pow_image_eq_target_maximalIdeal_pow_mul_ramificationIndex
Documentation

The image of the n-th power of a base uniformizer generates m_L^(e*n).

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem span_base_uniformizer_pow_image_eq_target_maximalIdeal_pow_mul_ramificationIndex
    {ϖ : base.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K)) (n : ℕ) :
    Ideal.span ({integerMap base.toDVF target.toDVF (ϖ ^ n)} :
        Set target.valuationSubring) =
      target.maximalIdeal ^
        (ramificationIndex base.toDVF target.toDVF * n)
theorem

base_uniformizer_image_mem_target_maximalIdeal_pow_ramificationIndex

L157 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.base_uniformizer_image_mem_target_maximalIdeal_pow_ramificationIndex
Documentation

The image of a base uniformizer lies in the e-th target maximal-ideal power.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem base_uniformizer_image_mem_target_maximalIdeal_pow_ramificationIndex
    {ϖ : base.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K)) :
    integerMap base.toDVF target.toDVF ϖ ∈
      target.maximalIdeal ^ ramificationIndex base.toDVF target.toDVF
theorem

base_uniformizer_image_not_mem_target_maximalIdeal_pow_succ_ramificationIndex

L168 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.base_uniformizer_image_not_mem_target_maximalIdeal_pow_succ_ramificationIndex
Documentation

The image of a base uniformizer has exact target maximal-ideal order e: it is not in the next power.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem base_uniformizer_image_not_mem_target_maximalIdeal_pow_succ_ramificationIndex
    {ϖ : base.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K)) :
    integerMap base.toDVF target.toDVF ϖ ∉
      target.maximalIdeal ^
        (ramificationIndex base.toDVF target.toDVF + 1)
theorem

exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image

L198 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image
Documentation

The image of a base uniformizer is a unit multiple of the e-th power of any target uniformizer.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L)) :
    ∃ u : target.valuationSubringˣ,
      integerMap base.toDVF target.toDVF ϖ =
        (u : target.valuationSubring) *
          π ^ ramificationIndex base.toDVF target.toDVF
theorem

exists_unit_mul_target_uniformizer_pow_mul_eq_base_uniformizer_pow_image

L263 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.exists_unit_mul_target_uniformizer_pow_mul_eq_base_uniformizer_pow_image
Documentation

Powers of a base uniformizer map to unit multiples of the corresponding target uniformizer power.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem exists_unit_mul_target_uniformizer_pow_mul_eq_base_uniformizer_pow_image
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L)) (n : ℕ) :
    ∃ u : target.valuationSubringˣ,
      integerMap base.toDVF target.toDVF (ϖ ^ n) =
        (u : target.valuationSubring) *
          π ^ (ramificationIndex base.toDVF target.toDVF * n)
theorem

base_uniformizer_pow_image_mem_target_maximalIdeal_pow_mul_ramificationIndex

L291 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.base_uniformizer_pow_image_mem_target_maximalIdeal_pow_mul_ramificationIndex
Documentation

The image of a power of a base uniformizer lies in the corresponding target maximal-ideal power.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem base_uniformizer_pow_image_mem_target_maximalIdeal_pow_mul_ramificationIndex
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L)) (n : ℕ) :
    integerMap base.toDVF target.toDVF (ϖ ^ n) ∈
      target.maximalIdeal ^
        (ramificationIndex base.toDVF target.toDVF * n)
theorem

base_uniformizer_pow_image_not_mem_target_next_pow_mul_ramificationIndex

L309 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.base_uniformizer_pow_image_not_mem_target_next_pow_mul_ramificationIndex
Documentation

The image of a power of a base uniformizer has exact target maximal-ideal order e*n.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem base_uniformizer_pow_image_not_mem_target_next_pow_mul_ramificationIndex
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L)) (n : ℕ) :
    integerMap base.toDVF target.toDVF (ϖ ^ n) ∉
      target.maximalIdeal ^
        (ramificationIndex base.toDVF target.toDVF * n + 1)

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