NYLL
Module

LocalizationRing.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.LocalizationRing
14 declarations indexed from sourceView source ↗

Module documentation

The actual localized integral closure inside an extension field

Choose a prime above the base maximal ideal and realize its localization as the image of the injective localization map into the extension field. This subalgebra representation uses the canonical inclusion and scalar towers.

Imports6
Imported by2

Declarations

abbrev

Normalization

L31 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.Normalization
Documentation

The actual integral closure of the base valuation ring in the extension field.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
abbrev Normalization (base : DVF.{u, v} K) : Type w
theorem

normalization_faithful

L34 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.normalization_faithful
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem normalization_faithful (base : DVF.{u, v} K) :
    FaithfulSMul base.valuationSubring (Normalization (L := L) base)
theorem

exists_prime

L43 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.exists_prime
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_prime (base : DVF.{u, v} K) :
    ∃ P : PrimeSpectrum (Normalization (L := L) base),
      P.asIdeal.IsMaximal ∧ P.asIdeal.LiesOver base.maximalIdeal
def

prime

L53 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.prime
Documentation

A chosen prime of the actual integral closure above the base maximal ideal.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def prime (base : DVF.{u, v} K) : PrimeSpectrum (Normalization (L := L) base)
theorem

prime_isMaximal

L57 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.prime_isMaximal
Documentation

The chosen prime is maximal.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem prime_isMaximal (base : DVF.{u, v} K) : (prime (L := L) base).asIdeal.IsMaximal
theorem

prime_liesOver

L61 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.prime_liesOver
Documentation

The chosen prime contracts to the base maximal ideal.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem prime_liesOver (base : DVF.{u, v} K) :
    (prime (L := L) base).asIdeal.LiesOver base.maximalIdeal
theorem

prime_ne_bot

L66 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.prime_ne_bot
Documentation

A prime above the nonzero maximal ideal of the base DVR is nonzero.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem prime_ne_bot (base : DVF.{u, v} K) : (prime (L := L) base).asIdeal ≠ ⊥
theorem

primeCompl_maps_to_units

L72 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.primeCompl_maps_to_units
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem primeCompl_maps_to_units (base : DVF.{u, v} K)
    (y : (prime (L := L) base).asIdeal.primeCompl) :
    IsUnit (algebraMap (Normalization (L := L) base) L y)
def

localizationEmbedding

L82 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localizationEmbedding
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def localizationEmbedding (base : DVF.{u, v} K) :
    Localization.AtPrime (prime (L := L) base).asIdeal →ₐ[Normalization (L := L) base] L where
  toRingHom := IsLocalization.lift (primeCompl_maps_to_units (L := L) base)
  commutes' x := IsLocalization.lift_eq (primeCompl_maps_to_units (L := L) base) x
theorem

localizationEmbedding_injective

L87 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localizationEmbedding_injective
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem localizationEmbedding_injective (base : DVF.{u, v} K) :
    Function.Injective (localizationEmbedding (L := L) base)
def

localizationSubalgebra

L97 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localizationSubalgebra
Documentation

The localization as an actual subalgebra of the extension field.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def localizationSubalgebra (base : DVF.{u, v} K) : Subalgebra (Normalization (L := L) base) L
abbrev

LocalizationRing

L101 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.LocalizationRing
Documentation

The localization of the actual integral closure at the selected prime.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
abbrev LocalizationRing (base : DVF.{u, v} K) : Type w
theorem

localization_isLocalization

L105 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localization_isLocalization
Documentation

The actual subalgebra has the localization universal property.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem localization_isLocalization (base : DVF.{u, v} K) :
    IsLocalization.AtPrime (LocalizationRing (L := L) base) (prime (L := L) base).asIdeal
theorem

baseMap_isLocalHom

L113 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.baseMap_isLocalHom
Documentation

The localized integral closure has a local algebra map from the base valuation ring.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
attribute [local instance] localization_isLocalization
Lean source · statement
theorem baseMap_isLocalHom (base : DVF.{u, v} K) :
    IsLocalHom (algebraMap base.valuationSubring (LocalizationRing (L := L) base))

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