NYLL
Module

Extensions.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Extensions
54 declarations indexed from sourceView source ↗

Module documentation

Finite extensions of discretely valued fields

The extension relation is ambient data: an algebra, finite-dimensionality, and mathlib's Valuation.HasExtension property. There is deliberately no proof-irrelevant marker object. All invariants and maps are defined once for DVF values and can therefore be used unchanged for Henselian and complete discretely valued fields through their canonical toDVF projections.

Imports8
Imported by12

Declarations

def

degree

L41 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.degree
Documentation

The field degree of a finite valued extension.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def degree (_base : DVF.{u, v} K) (_target : DVF.{w, x} L) : ℕ
theorem

degree_eq_finrank

L47 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.degree_eq_finrank
Documentation

The degree of a finite extension of discrete valuation fields is its linear finrank.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L]
    [base.valuation.HasExtension target.valuation] in
Lean source · statement
theorem degree_eq_finrank :
    degree base target = Module.finrank K L
def

ramificationIndex

L53 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
Documentation

The canonical ramification index of the target maximal ideal over the base maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def ramificationIndex : ℕ
def

residueDegree

L60 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
Documentation

The canonical residue degree of the target maximal ideal over the base maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def residueDegree : ℕ
def

integerMap

L65 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap
Documentation

The induced map between valuation subrings.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def integerMap :
    base.valuationSubring →+* target.valuationSubring
theorem

integerMap_injective

L71 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_injective
Documentation

The induced map between valuation subrings is injective.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_injective :
    Function.Injective (integerMap base target)
theorem

integerMap_apply

L81 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_apply
Documentation

The valuation-subring map evaluates through the ambient algebra map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_apply (a : base.valuationSubring) :
    (((integerMap base target) a : target.valuationSubring) : L) =
      algebraMap K L (a : K)
theorem

algebraMap_mem_valuationSubring_iff

L90 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.algebraMap_mem_valuationSubring_iff
Documentation

Elementwise form of valuation-ring pullback along the field algebra map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem algebraMap_mem_valuationSubring_iff (a : K) :
    algebraMap K L a ∈ target.valuation.valuationSubring ↔
      a ∈ base.valuation.valuationSubring
theorem

integerMap_mem_maximalIdeal_iff

L99 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_mem_maximalIdeal_iff
Documentation

Maximal-ideal membership is reflected by a valued extension.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_mem_maximalIdeal_iff (a : base.valuationSubring) :
    integerMap base target a ∈ target.maximalIdeal ↔
      a ∈ base.maximalIdeal
theorem

integerMap_not_mem_maximalIdeal_iff

L109 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_not_mem_maximalIdeal_iff
Documentation

Nonmembership in the maximal ideal is reflected by a valued extension.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_not_mem_maximalIdeal_iff (a : base.valuationSubring) :
    integerMap base target a ∉ target.maximalIdeal ↔
      a ∉ base.maximalIdeal
theorem

integerMap_isUnit_iff

L116 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_isUnit_iff
Documentation

The integer map of a valued extension preserves and reflects units.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_isUnit_iff (a : base.valuationSubring) :
    IsUnit (integerMap base target a) ↔ IsUnit a
theorem

maximalIdeal_comap_integerMap_eq

L124 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_comap_integerMap_eq
Documentation

The target maximal ideal pulls back to the base maximal ideal.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem maximalIdeal_comap_integerMap_eq :
    target.maximalIdeal.comap (integerMap base target) =
      base.maximalIdeal
theorem

maximalIdeal_map_integerMap_ne_bot

L132 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_map_integerMap_ne_bot
Documentation

The image of the source maximal ideal in the target valuation ring is nonzero.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem maximalIdeal_map_integerMap_ne_bot :
    Ideal.map (integerMap base target) base.maximalIdeal ≠ ⊥
theorem

maximalIdeal_map_integerMap_le

L141 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_map_integerMap_le
Documentation

The source maximal ideal maps into the target maximal ideal.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem maximalIdeal_map_integerMap_le :
    Ideal.map (integerMap base target) base.maximalIdeal ≤
      target.maximalIdeal
theorem

residueField_ringChar_eq_of_hasExtension

L150 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueField_ringChar_eq_of_hasExtension
Documentation

Residue fields connected by a valued extension have the same ring characteristic.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueField_ringChar_eq_of_hasExtension :
    ringChar target.residueField = ringChar base.residueField
def

residueMap

L155 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap
Documentation

The induced map on residue fields.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def residueMap :
    base.residueField →+* target.residueField
theorem

residueMap_residue

L161 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue
Documentation

The residue-field map sends the residue of an integer to its target residue.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue (a : base.valuationSubring) :
    residueMap base target (base.residueMap a) =
      target.residueMap (integerMap base target a)
theorem

residueMap_injective

L176 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_injective
Documentation

The residue-field map of a valued extension is injective.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_injective :
    Function.Injective (residueMap base target)
theorem

residueMap_eq_zero_iff

L187 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_eq_zero_iff
Documentation

The residue-field map of a valued extension has trivial kernel.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_eq_zero_iff (z : base.residueField) :
    residueMap base target z = 0 ↔ z = 0
theorem

residueMap_ne_zero_iff

L197 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_ne_zero_iff
Documentation

Nonzero residue classes remain nonzero after mapping.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_ne_zero_iff (z : base.residueField) :
    residueMap base target z ≠ 0 ↔ z ≠ 0
theorem

residueMap_eq_iff

L203 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_eq_iff
Documentation

Equality of base residue classes can be checked after mapping.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_eq_iff (a b : base.residueField) :
    residueMap base target a = residueMap base target b ↔ a = b
theorem

residueMap_eq_one_iff

L213 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_eq_one_iff
Documentation

The residue-field map reflects the unit element.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_eq_one_iff (a : base.residueField) :
    residueMap base target a = 1 ↔ a = 1
theorem

residueMap_bijective_of_surjective

L221 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_bijective_of_surjective
Documentation

Surjectivity of the residue map upgrades its canonical injectivity to bijectivity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_bijective_of_surjective
    (hSurj : Function.Surjective (residueMap base target)) :
    Function.Bijective (residueMap base target)
def

residueFieldEquivOfSurjective

L228 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldEquivOfSurjective
Documentation

The residue-field isomorphism attached to a surjective residue map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
def residueFieldEquivOfSurjective
    (hSurj : Function.Surjective (residueMap base target)) :
    base.residueField ≃+* target.residueField
theorem

residueFieldEquivOfSurjective_apply

L236 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldEquivOfSurjective_apply
Documentation

The residue-field equivalence induced by surjectivity evaluates by the residue map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueFieldEquivOfSurjective_apply
    (hSurj : Function.Surjective (residueMap base target))
    (z : base.residueField) :
    residueFieldEquivOfSurjective base target hSurj z =
      residueMap base target z
theorem

residueFieldEquivOfSurjective_symm_apply_residueMap

L245 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldEquivOfSurjective_symm_apply_residueMap
Documentation

The inverse residue-field equivalence recovers a source class after applying the residue map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueFieldEquivOfSurjective_symm_apply_residueMap
    (hSurj : Function.Surjective (residueMap base target))
    (z : base.residueField) :
    (residueFieldEquivOfSurjective base target hSurj).symm
        (residueMap base target z) = z
theorem

residueMap_residueFieldEquivOfSurjective_symm_apply

L256 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residueFieldEquivOfSurjective_symm_apply
Documentation

Applying the residue map after the inverse residue-field equivalence recovers the target class.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residueFieldEquivOfSurjective_symm_apply
    (hSurj : Function.Surjective (residueMap base target))
    (z : target.residueField) :
    residueMap base target
        ((residueFieldEquivOfSurjective base target hSurj).symm z) = z
theorem

residueMap_residue_eq_zero_iff

L265 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue_eq_zero_iff
Documentation

Zero of a mapped residue class is exactly base maximal-ideal membership.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue_eq_zero_iff (a : base.valuationSubring) :
    residueMap base target (base.residueMap a) = 0 ↔
      a ∈ base.maximalIdeal
theorem

residueMap_residue_ne_zero_iff

L274 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue_ne_zero_iff
Documentation

Nonzero of a mapped residue class is exactly nonmembership in the base maximal ideal.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue_ne_zero_iff (a : base.valuationSubring) :
    residueMap base target (base.residueMap a) ≠ 0 ↔
      a ∉ base.maximalIdeal
theorem

residueMap_residue_ne_zero_iff_isUnit

L282 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue_ne_zero_iff_isUnit
Documentation

Nonzero of a mapped residue class is exactly unitness of its representative.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue_ne_zero_iff_isUnit
    (a : base.valuationSubring) :
    residueMap base target (base.residueMap a) ≠ 0 ↔ IsUnit a
theorem

residueMap_residue_eq_iff

L290 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue_eq_iff
Documentation

Equality of mapped residue classes is equality in the base residue field.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue_eq_iff (a b : base.valuationSubring) :
    residueMap base target (base.residueMap a) =
        residueMap base target (base.residueMap b) ↔
      base.residueMap a = base.residueMap b
theorem

residueMap_residue_eq_target_residue_iff_sub_mem_maximalIdeal

L299 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_residue_eq_target_residue_iff_sub_mem_maximalIdeal
Documentation

Congruence criterion comparing a mapped base residue with a target representative.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_residue_eq_target_residue_iff_sub_mem_maximalIdeal
    (a : base.valuationSubring) (b : target.valuationSubring) :
    residueMap base target (base.residueMap a) = target.residueMap b ↔
      integerMap base target a - b ∈ target.maximalIdeal
theorem

target_residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal

L310 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal
Documentation

Opposite-orientation form of the target congruence criterion.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal
    (b : target.valuationSubring) (a : base.valuationSubring) :
    target.residueMap b = residueMap base target (base.residueMap a) ↔
      b - integerMap base target a ∈ target.maximalIdeal
theorem

target_residue_integerMap_eq_zero_iff

L321 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_eq_zero_iff
Documentation

Target-residue form of zero detection for a mapped base integer.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_eq_zero_iff
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) = 0 ↔
      a ∈ base.maximalIdeal
theorem

target_residue_integerMap_ne_zero_iff

L330 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_ne_zero_iff
Documentation

Target-residue form of nonzero detection for a mapped base integer.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_ne_zero_iff
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) ≠ 0 ↔
      a ∉ base.maximalIdeal
theorem

target_residue_integerMap_ne_zero_iff_isUnit

L339 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_ne_zero_iff_isUnit
Documentation

A mapped base integer has nonzero target residue exactly when it is a unit in the base valuation ring.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_ne_zero_iff_isUnit
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) ≠ 0 ↔ IsUnit a
theorem

target_residue_integerMap_ne_zero_iff_integerMap_isUnit

L348 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_ne_zero_iff_integerMap_isUnit
Documentation

A mapped base integer has nonzero target residue exactly when its image is a unit.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_ne_zero_iff_integerMap_isUnit
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) ≠ 0 ↔
      IsUnit (integerMap base target a)
theorem

target_residue_integerMap_ne_zero_iff_base_residue_ne_zero

L356 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_ne_zero_iff_base_residue_ne_zero
Documentation

Nonzero residue is preserved and reflected by the integer map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_ne_zero_iff_base_residue_ne_zero
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) ≠ 0 ↔
      base.residueMap a ≠ 0
theorem

integerMap_isUnit_iff_target_residue_integerMap_ne_zero

L365 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_isUnit_iff_target_residue_integerMap_ne_zero
Documentation

A mapped valuation-ring element is a unit exactly when its target residue is nonzero.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_isUnit_iff_target_residue_integerMap_ne_zero
    (a : base.valuationSubring) :
    IsUnit (integerMap base target a) ↔
      target.residueMap (integerMap base target a) ≠ 0
theorem

integerMap_isUnit_iff_base_residue_ne_zero

L374 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.integerMap_isUnit_iff_base_residue_ne_zero
Documentation

A mapped valuation-ring element is a unit exactly when its source residue is nonzero.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem integerMap_isUnit_iff_base_residue_ne_zero
    (a : base.valuationSubring) :
    IsUnit (integerMap base target a) ↔ base.residueMap a ≠ 0
theorem

target_residue_integerMap_eq_iff

L383 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_eq_iff
Documentation

Equality of target residues of mapped base integers is equality of their base residues.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_eq_iff
    (a b : base.valuationSubring) :
    target.residueMap (integerMap base target a) =
        target.residueMap (integerMap base target b) ↔
      base.residueMap a = base.residueMap b
theorem

target_residue_integerMap_eq_one_iff_base_residue_eq_one

L394 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.target_residue_integerMap_eq_one_iff_base_residue_eq_one
Documentation

A mapped integer has target residue one exactly when its source residue is one.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem target_residue_integerMap_eq_one_iff_base_residue_eq_one
    (a : base.valuationSubring) :
    target.residueMap (integerMap base target a) = 1 ↔
      base.residueMap a = 1
def

unitMap

L402 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.unitMap
Documentation

The induced map on unit groups of valuation rings.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def unitMap :
    base.valuationSubringˣ →* target.valuationSubringˣ
theorem

unitMap_apply

L408 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.unitMap_apply
Documentation

The induced unit map agrees with the valuation-ring map on underlying elements.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem unitMap_apply (a : base.valuationSubringˣ) :
    ((unitMap base target a : target.valuationSubringˣ) :
        target.valuationSubring) =
      integerMap base target (a : base.valuationSubring)
theorem

residueUnitsMap_injective

L416 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueUnitsMap_injective
Documentation

The induced map on residue-field units is injective.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueUnitsMap_injective :
    Function.Injective
      (Units.map (residueMap base target).toMonoidHom)
theorem

residueUnitsMap_surjective_of_residueMap_surjective

L423 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueUnitsMap_surjective_of_residueMap_surjective
Documentation

Surjectivity of the residue map implies surjectivity on residue-field units.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueUnitsMap_surjective_of_residueMap_surjective
    (hSurj : Function.Surjective (residueMap base target)) :
    Function.Surjective
      (Units.map (residueMap base target).toMonoidHom)
theorem

residueUnitsMap_bijective_of_residueMap_surjective

L438 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueUnitsMap_bijective_of_residueMap_surjective
Documentation

A surjective residue map induces a bijection on residue-field units.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueUnitsMap_bijective_of_residueMap_surjective
    (hSurj : Function.Surjective (residueMap base target)) :
    Function.Bijective
      (Units.map (residueMap base target).toMonoidHom)
def

residueUnitsEquivOfResidueMapSurjective

L447 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueUnitsEquivOfResidueMapSurjective
Documentation

The unit-group equivalence induced by a surjective residue map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
def residueUnitsEquivOfResidueMapSurjective
    (hSurj : Function.Surjective (residueMap base target)) :
    base.residueFieldˣ ≃* target.residueFieldˣ
theorem

residueUnitsEquivOfResidueMapSurjective_apply

L456 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueUnitsEquivOfResidueMapSurjective_apply
Documentation

The residue-unit equivalence evaluates by the induced residue-unit map.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueUnitsEquivOfResidueMapSurjective_apply
    (hSurj : Function.Surjective (residueMap base target))
    (a : base.residueFieldˣ) :
    residueUnitsEquivOfResidueMapSurjective base target hSurj a =
      Units.map (residueMap base target).toMonoidHom a
theorem

residueFieldEquivOfSurjective_apply_residue

L465 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldEquivOfSurjective_apply_residue
Documentation

The residue-field equivalence sends a source residue to the corresponding target residue.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueFieldEquivOfSurjective_apply_residue
    (hSurj : Function.Surjective (residueMap base target))
    (a : base.valuationSubring) :
    residueFieldEquivOfSurjective base target hSurj (base.residueMap a) =
      target.residueMap (integerMap base target a)
theorem

residueFieldEquivOfSurjective_symm_apply_target_residue

L475 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldEquivOfSurjective_symm_apply_target_residue
Documentation

The inverse residue-field equivalence sends a target residue back to its source residue.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem residueFieldEquivOfSurjective_symm_apply_target_residue
    (hSurj : Function.Surjective (residueMap base target))
    (a : base.valuationSubring) :
    (residueFieldEquivOfSurjective base target hSurj).symm
        (target.residueMap (integerMap base target a)) =
      base.residueMap a
def

IsUnramified

L485 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsUnramified
Documentation

Unramified means that the canonical ramification index is one.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def IsUnramified : Prop
def

IsTotallyRamified

L489 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyRamified
Documentation

Totally ramified means that the canonical residue degree is one.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def IsTotallyRamified : Prop
def

IsDefectless

L493 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsDefectless
Documentation

Defectlessness is the exact fundamental equality.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def IsDefectless : Prop

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