Module

IntegralClosure.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.IntegralClosure

94 declarations indexed from sourceView source ↗

Module documentation

Integral closures of valuation rings

This module uses the actual mathlib integral closure integralClosure base.toDVF.valuationSubring L. It does not introduce a replacement structure.

Imports10

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Extensions
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianFinite
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.QuasiFinite.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.Valuation.Integral
Mathlib.LinearAlgebra.TensorProduct.RightExactness

Imported by3

theorem

primeSpectrum_subsingleton_of_isArtinianRing_of_idempotents_trivial

L40 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.primeSpectrum_subsingleton_of_isArtinianRing_of_idempotents_trivial

Documentation

An Artinian ring whose idempotents are all trivial has at most one prime.

This is the topological/idempotent bridge used in the Henselian frontier: in an Artinian ring, Spec is discrete, so a hypothetical singleton clopen separating two primes is represented by an idempotent.

Source context 5 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension

Lean source · statement

theorem primeSpectrum_subsingleton_of_isArtinianRing_of_idempotents_trivial
    {A : Type u} [CommRing A] [IsArtinianRing A]
    (hidempotent : ∀ e : A, IsIdempotentElem e → e = 0 ∨ e = 1) :
    Subsingleton (PrimeSpectrum A)

theorem

maximalIdeal_fiber_includeRight_surjective

L64 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_fiber_includeRight_surjective

Documentation

Over a local base ring, the canonical map from an algebra to the fiber over the maximal ideal is surjective.

Source context 5 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension

Lean source · statement

theorem maximalIdeal_fiber_includeRight_surjective
    {R S : Type*} [CommRing R] [IsLocalRing R] [CommRing S]
    [Algebra R S] :
    Function.Surjective
      (Algebra.TensorProduct.includeRight :
        S →ₐ[R] (IsLocalRing.maximalIdeal R).Fiber S)

theorem

maximalIdeal_fiber_includeRight_ker_eq_maximalIdeal_map

L90 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_fiber_includeRight_ker_eq_maximalIdeal_map

Documentation

Over a local base ring, the kernel of the canonical map from an algebra to the fiber over the maximal ideal is the ideal generated by the maximal ideal of the base.

This is the Ideal.Fiber form of the residue-field tensor kernel calculation: S -> (maximalIdeal R).Fiber S has kernel maximalIdeal R * S.

Source context 5 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension

Lean source · statement

theorem maximalIdeal_fiber_includeRight_ker_eq_maximalIdeal_map
    {R S : Type*} [CommRing R] [IsLocalRing R] [CommRing S]
    [Algebra R S] :
    RingHom.ker ((Algebra.TensorProduct.includeRight :
      S →ₐ[R] (IsLocalRing.maximalIdeal R).Fiber S) :
        S →+* (IsLocalRing.maximalIdeal R).Fiber S) =
      (IsLocalRing.maximalIdeal R).map (algebraMap R S)

theorem

residueField_tensor_includeRight_ker_eq_maximalIdeal_map

L133 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.residueField_tensor_includeRight_ker_eq_maximalIdeal_map

Documentation

For a local ring R, the kernel of S → κ(R) ⊗[R] S is the ideal of S generated by the maximal ideal of R.

This is the local-residue-field tensor form of the kernel computation needed for the Henselian finite-extension frontier.

Source context 5 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x
namespace DiscreteValuationField
namespace ValuedExtension

Lean source · statement

theorem residueField_tensor_includeRight_ker_eq_maximalIdeal_map
    {R S : Type*} [CommRing R] [IsLocalRing R] [CommRing S]
    [Algebra R S] :
    RingHom.ker ((Algebra.TensorProduct.includeRight :
      S →ₐ[R] TensorProduct R (IsLocalRing.ResidueField R) S) :
        S →+* TensorProduct R (IsLocalRing.ResidueField R) S) =
      (IsLocalRing.maximalIdeal R).map (algebraMap R S)

theorem

integralClosure_mem_target_valuationSubring_of_hasExtension

L235 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_mem_target_valuationSubring_of_hasExtension

Documentation

Every element integral over the base valuation ring lies in any valuation ring extending the base valuation. This is the construction-level inclusion from the actual integral closure into an extension 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosure_mem_target_valuationSubring_of_hasExtension
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : integralClosure base.toDVF.valuationSubring L) :
    (z : L) ∈ target.valuation.valuationSubring

def

integralClosureToTargetValuationSubringOfHasExtension

L250 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureToTargetValuationSubringOfHasExtension

Documentation

The canonical map from the actual integral closure of the base valuation ring in L to any valuation ring extending the base valuation.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · full declaration

def integralClosureToTargetValuationSubringOfHasExtension
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    integralClosure base.toDVF.valuationSubring L →+* target.toDVF.valuationSubring where
  toFun z :=
    ⟨(z : L),
      integralClosure_mem_target_valuationSubring_of_hasExtension
        (K := K) (L := L) base target z⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' z₁ z₂ := by ext; simp
  map_mul' z₁ z₂ := by ext; simp

theorem

integralClosureToTargetValuationSubringOfHasExtension_apply

L266 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureToTargetValuationSubringOfHasExtension_apply

Documentation

The map from the integral closure to the target valuation ring uses the ambient inclusion.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureToTargetValuationSubringOfHasExtension_apply
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : integralClosure base.toDVF.valuationSubring L) :
    ((integralClosureToTargetValuationSubringOfHasExtension
      (K := K) (L := L) base target z : target.toDVF.valuationSubring) : L) = z

theorem

integralClosureToTargetValuationSubringOfHasExtension_injective

L278 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureToTargetValuationSubringOfHasExtension_injective

Documentation

The canonical map from the integral closure to an extension valuation ring 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureToTargetValuationSubringOfHasExtension_injective
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    Function.Injective
      (integralClosureToTargetValuationSubringOfHasExtension
        (K := K) (L := L) base target)

theorem

target_valuationSubring_mem_integralClosure_of_moduleFinite

L293 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_mem_integralClosure_of_moduleFinite

Documentation

Under module-finiteness of the extension valuation ring over the base valuation ring, every target valuation-ring element is integral over 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_valuationSubring_mem_integralClosure_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : target.toDVF.valuationSubring) :
    (z : L) ∈ integralClosure base.toDVF.valuationSubring L

def

targetValuationSubringToIntegralClosureOfModuleFinite

L311 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.targetValuationSubringToIntegralClosureOfModuleFinite

Documentation

The canonical map from a finite extension valuation ring into the actual integral closure of the base valuation ring.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · full declaration

def targetValuationSubringToIntegralClosureOfModuleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    target.toDVF.valuationSubring →+* integralClosure base.toDVF.valuationSubring L where
  toFun z :=
    ⟨(z : L),
      target_valuationSubring_mem_integralClosure_of_moduleFinite
        (K := K) (L := L) base target z⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' z₁ z₂ := by ext; simp
  map_mul' z₁ z₂ := by ext; simp

theorem

targetValuationSubringToIntegralClosureOfModuleFinite_apply

L328 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.targetValuationSubringToIntegralClosureOfModuleFinite_apply

Documentation

The inverse map sends a target integer to its integral-closure 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem targetValuationSubringToIntegralClosureOfModuleFinite_apply
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : target.toDVF.valuationSubring) :
    ((targetValuationSubringToIntegralClosureOfModuleFinite
      (K := K) (L := L) base target z :
        integralClosure base.toDVF.valuationSubring L) : L) = z

theorem

integralClosureToTargetValuationSubringOfHasExtension_surjective_of_moduleFinite

L342 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureToTargetValuationSubringOfHasExtension_surjective_of_moduleFinite

Documentation

Under module-finiteness, the canonical map from the integral closure to the extension valuation ring is surjective.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureToTargetValuationSubringOfHasExtension_surjective_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    Function.Surjective
      (integralClosureToTargetValuationSubringOfHasExtension
        (K := K) (L := L) base target)

theorem

integralClosureToTargetValuationSubringOfHasExtension_bijective_of_moduleFinite

L359 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureToTargetValuationSubringOfHasExtension_bijective_of_moduleFinite

Documentation

Under module-finiteness, the canonical map from the integral closure to the extension valuation ring is bijective.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureToTargetValuationSubringOfHasExtension_bijective_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    Function.Bijective
      (integralClosureToTargetValuationSubringOfHasExtension
        (K := K) (L := L) base target)

def

integralClosureRingEquivTargetValuationSubringOfModuleFinite

L375 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureRingEquivTargetValuationSubringOfModuleFinite

Documentation

If the extension valuation ring is finite over the base valuation ring, then it is canonically ring-equivalent to the actual integral closure of the base valuation ring in the extension field.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

def integralClosureRingEquivTargetValuationSubringOfModuleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    integralClosure base.toDVF.valuationSubring L ≃+* target.toDVF.valuationSubring

theorem

integralClosureRingEquivTargetValuationSubringOfModuleFinite_apply

L389 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureRingEquivTargetValuationSubringOfModuleFinite_apply

Documentation

The finite integral-closure ring equivalence evaluates by the canonical inclusion.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureRingEquivTargetValuationSubringOfModuleFinite_apply
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : integralClosure base.toDVF.valuationSubring L) :
    (integralClosureRingEquivTargetValuationSubringOfModuleFinite
      (K := K) (L := L) base target z :
        target.toDVF.valuationSubring) =
      integralClosureToTargetValuationSubringOfHasExtension
        (K := K) (L := L) base target z

def

integralClosureAlgEquivTargetValuationSubringOfModuleFinite

L404 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureAlgEquivTargetValuationSubringOfModuleFinite

Documentation

Algebra-equivalence form of integralClosureRingEquivTargetValuationSubringOfModuleFinite.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

def integralClosureAlgEquivTargetValuationSubringOfModuleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    integralClosure base.toDVF.valuationSubring L ≃ₐ[base.toDVF.valuationSubring]
      target.toDVF.valuationSubring

theorem

integralClosureAlgEquivTargetValuationSubringOfModuleFinite_apply

L422 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureAlgEquivTargetValuationSubringOfModuleFinite_apply

Documentation

The finite integral-closure algebra equivalence evaluates by the canonical inclusion.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureAlgEquivTargetValuationSubringOfModuleFinite_apply
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    (z : integralClosure base.toDVF.valuationSubring L) :
    (integralClosureAlgEquivTargetValuationSubringOfModuleFinite
      (K := K) (L := L) base target z :
        target.toDVF.valuationSubring) =
      integralClosureToTargetValuationSubringOfHasExtension
        (K := K) (L := L) base target z

theorem

target_valuationSubring_isIntegralClosure_of_moduleFinite

L440 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_moduleFinite

Documentation

If the extension valuation ring is finite over the base valuation ring, then it is the integral closure of the base valuation ring in the extension 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_valuationSubring_isIntegralClosure_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L

theorem

target_valuationSubring_isIntegralClosure_of_moduleFinite'

L462 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_moduleFinite'

Documentation

Ambient-context version of target_valuationSubring_isIntegralClosure_of_moduleFinite.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_valuationSubring_isIntegralClosure_of_moduleFinite'
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L

theorem

base_valuationSubring_isFractionRing

L470 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.base_valuationSubring_isFractionRing

Documentation

The valuation ring of a complete DVF is a fraction ring inside the field.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem base_valuationSubring_isFractionRing (base : CompleteDVF.{u, v} K) :
    IsFractionRing base.toDVF.valuationSubring K

theorem

base_valuationSubring_isIntegrallyClosed

L475 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.base_valuationSubring_isIntegrallyClosed

Documentation

The valuation ring of a complete DVF is integrally closed.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem base_valuationSubring_isIntegrallyClosed
    (base : CompleteDVF.{u, v} K) :
    IsIntegrallyClosed base.toDVF.valuationSubring

theorem

base_valuationSubring_isNoetherianRing

L481 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.base_valuationSubring_isNoetherianRing

Documentation

The valuation ring of a complete DVF is Noetherian.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem base_valuationSubring_isNoetherianRing
    (base : CompleteDVF.{u, v} K) :
    IsNoetherianRing base.toDVF.valuationSubring

theorem

moduleFinite_target_valuationSubring_of_isIntegralClosure

L491 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_isIntegralClosure

Documentation

If a chosen extension valuation ring is already proved to be the integral closure of the base valuation ring in a finite separable field extension, then it is finite over the base valuation ring.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem moduleFinite_target_valuationSubring_of_isIntegralClosure
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    [IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L] :
    Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring

theorem

moduleFinite_target_valuationSubring_of_isIntegralClosure'

L508 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_isIntegralClosure'

Documentation

Ambient-context version of moduleFinite_target_valuationSubring_of_isIntegralClosure.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem moduleFinite_target_valuationSubring_of_isIntegralClosure'
    [Algebra.IsSeparable K L]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    [IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L] :
    Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring

theorem

target_valuationSubring_isIntegralClosure_iff_moduleFinite

L519 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_iff_moduleFinite

Documentation

For finite separable field extensions with a chosen valuation extension, being the integral closure is equivalent to being finite as a module over the base valuation ring.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem target_valuationSubring_isIntegralClosure_iff_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L ↔
      Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring

theorem

target_valuationSubring_isIntegralClosure_iff_moduleFinite'

L541 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_iff_moduleFinite'

Documentation

Ambient-context version of target_valuationSubring_isIntegralClosure_iff_moduleFinite.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem target_valuationSubring_isIntegralClosure_iff_moduleFinite'
    [Algebra.IsSeparable K L]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L] :
    IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L ↔
      Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring

theorem

target_maximalIdeal_liesOver_base_maximal_of_hasExtension

L553 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_maximalIdeal_liesOver_base_maximal_of_hasExtension

Documentation

The target maximal ideal lies over the base maximal ideal for an actual extension of valuations. This is the prime-theoretic input for replacing certificate-style choices of a prime above 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_maximalIdeal_liesOver_base_maximal_of_hasExtension
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation] :
    target.maximalIdeal.LiesOver base.maximalIdeal

theorem

target_primeOver_eq_maximalIdeal_of_isIntegral

L564 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_primeOver_eq_maximalIdeal_of_isIntegral

Documentation

In an integral local valued extension, every prime of the target valuation ring lying over the base maximal ideal is 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_primeOver_eq_maximalIdeal_of_isIntegral
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsIntegral base.toDVF.valuationSubring target.toDVF.valuationSubring]
    {P : Ideal target.toDVF.valuationSubring}
    (hP : P ∈ Ideal.primesOver base.maximalIdeal target.toDVF.valuationSubring) :
    P = target.maximalIdeal

theorem

target_primesOver_base_maximal_eq_singleton_of_isIntegral

L576 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_primesOver_base_maximal_eq_singleton_of_isIntegral

Documentation

Integral local valued extensions have a unique prime above the base maximal ideal: 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_primesOver_base_maximal_eq_singleton_of_isIntegral
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsIntegral base.toDVF.valuationSubring target.toDVF.valuationSubring] :
    Ideal.primesOver base.maximalIdeal target.toDVF.valuationSubring =
      {target.maximalIdeal}

theorem

target_primesOver_base_maximal_eq_singleton_of_moduleFinite

L594 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_primesOver_base_maximal_eq_singleton_of_moduleFinite

Documentation

Module-finite local valued extensions have a unique prime above 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_primesOver_base_maximal_eq_singleton_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.toDVF.valuationSubring target.toDVF.valuationSubring] :
    Ideal.primesOver base.maximalIdeal target.toDVF.valuationSubring =
      {target.maximalIdeal}

theorem

target_primesOver_base_maximal_eq_singleton_of_isIntegralClosure

L609 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_primesOver_base_maximal_eq_singleton_of_isIntegralClosure

Documentation

If the target valuation ring has already been identified as the integral closure of the base valuation ring in the field extension, then the prime over the base maximal ideal is unique.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem target_primesOver_base_maximal_eq_singleton_of_isIntegralClosure
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    [IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L] :
    Ideal.primesOver base.maximalIdeal target.toDVF.valuationSubring =
      {target.maximalIdeal}

theorem

integralClosure_mem_or_inv_of_target_valuationSubring_isIntegralClosure

L626 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_mem_or_inv_of_target_valuationSubring_isIntegralClosure

Documentation

If the chosen extension valuation ring is the actual integral closure of the base valuation ring in L, then the actual integral closure satisfies the valuation-ring dichotomy. This is the bridge from an integral-closure identification to the hval input used by the finite-separable uniqueness API.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosure_mem_or_inv_of_target_valuationSubring_isIntegralClosure
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.toDVF.valuationSubring target.toDVF.valuationSubring L]
    [IsIntegralClosure target.toDVF.valuationSubring base.toDVF.valuationSubring L] :
    ∀ z : L,
      z ∈ (integralClosure base.toDVF.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.toDVF.valuationSubring L).toSubring

abbrev

integralClosureIntegers

L651 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureIntegers

Documentation

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

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

abbrev integralClosureIntegers (base : CompleteDVF.{u, v} K)
    (_target : CompleteDVF.{w, x} L) : Type _

theorem

integralClosure_isIntegralClosure

L657 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isIntegralClosure

Documentation

The actual integral closure is an IsIntegralClosure.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isIntegralClosure :
    IsIntegralClosure (integralClosureIntegers base target) base.toDVF.valuationSubring L

theorem

integralClosure_isIntegral

L665 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isIntegral

Documentation

The actual integral closure is integral over 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isIntegral :
    Algebra.IsIntegral base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_algebraMap_injective

L674 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_algebraMap_injective

Documentation

The algebra map from the base valuation ring into the actual integral closure 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_algebraMap_injective :
    Function.Injective
      (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target))

theorem

integralClosure_faithfulSMul

L684 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_faithfulSMul

Documentation

The actual integral closure is faithful over 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_faithfulSMul :
    FaithfulSMul base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

moduleFinite_integralClosureIntegers

L693 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_integralClosureIntegers

Documentation

In a finite separable field extension, the actual integral closure is module-finite over 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem moduleFinite_integralClosureIntegers
    [Algebra.IsSeparable K L] :
    Module.Finite base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_quasiFinite

L711 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_quasiFinite

Documentation

In a finite separable field extension, the actual integral closure is quasi-finite over 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_quasiFinite
    [Algebra.IsSeparable K L] :
    Algebra.QuasiFinite base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_base_maximal_fiber_isArtinianRing

L721 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_isArtinianRing

Documentation

The residue fiber of the finite actual integral closure over the base maximal ideal is Artinian.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_isArtinianRing
    [Algebra.IsSeparable K L] :
    IsArtinianRing (base.maximalIdeal.Fiber (integralClosureIntegers base target))

theorem

integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map

L731 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map

Documentation

For the actual integral closure, the kernel of the residue-fiber includeRight map is the ideal generated by 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map
     :
    RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) =
      base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target))

theorem

integralClosure_idempotent_eq_zero_or_one

L752 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_idempotent_eq_zero_or_one

Documentation

Idempotents in the actual integral closure in the extension field are trivial.

This keeps the Henselian frontier focused on lifting idempotents out of the finite residue fiber: once an idempotent has lifted to the actual integral closure, domainhood inside the field forces it to be 0 or 1.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_idempotent_eq_zero_or_one
    (e : (integralClosureIntegers base target))
    (he : IsIdempotentElem e) :
    e = 0 ∨ e = 1

theorem

integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift

L768 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift

Documentation

If every idempotent of the residue fiber over the base maximal ideal lifts to an idempotent of the actual integral closure, then that fiber has at most one prime.

This packages the topological Artinian-fiber/idempotent argument in the form needed by the Henselian finite-extension proof.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift
    [Algebra.IsSeparable K L]
    (hlift :
      ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
        IsIdempotentElem e →
          ∃ b : (integralClosureIntegers base target),
            IsIdempotentElem b ∧
              Algebra.TensorProduct.includeRight b = e) :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker

L802 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker

Documentation

Henselian-kernel form of idempotent lifting for the residue fiber of the actual integral closure.

The remaining Henselian finite-extension work can now focus on proving that the includeRight map to the finite residue fiber is surjective and has Henselian kernel; the idempotent lifting itself is supplied by Hensel's lemma for X^2 - X.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem
integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker
    (hsurj :
      Function.Surjective
        (Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker

L837 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker

Documentation

If the residue-fiber includeRight map has Henselian kernel and is surjective, then the fiber has at most one prime.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker
    [Algebra.IsSeparable K L]
    (hsurj :
      Function.Surjective
        (Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker

L865 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker

Documentation

Henselian-kernel idempotent lifting for the residue fiber of the actual integral closure.

The includeRight map is automatically surjective because the base valuation ring is local.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker

L888 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker

Documentation

If the includeRight map to the residue fiber has Henselian kernel, then the fiber has at most one prime.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map

L911 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map

Documentation

Idempotent lifting from the natural Henselian-pair ideal base.maximalIdeal.map in the actual integral closure.

The generic kernel computation identifies this ideal with the kernel of the residue-fiber includeRight 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map
    [HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map

L936 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map

Documentation

If the ideal generated by the base maximal ideal is Henselian in the actual integral closure, then the residue fiber has at most one prime.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_map_henselianRing

L963 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_map_henselianRing

Documentation

In a finite separable extension of complete DVFs, the natural ideal generated by the base maximal ideal is Henselian in the actual integral closure.

This packages the finite-module completeness theorem together with the comparison between I-adic and I.map-adic completeness.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_henselianRing
    [Algebra.IsSeparable K L] :
    HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)))

theorem

integralClosure_primesOver_base_maximal_finite

L990 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_primesOver_base_maximal_finite

Documentation

In a finite separable field extension, there are only finitely many primes of the actual integral closure above 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_finite
    [Algebra.IsSeparable K L] :
    (Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target)).Finite

theorem

integralClosure_primesOver_base_maximal_nonempty

L1001 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_primesOver_base_maximal_nonempty

Documentation

The actual integral closure has at least one prime above 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_nonempty
     :
    Nonempty (Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target))

theorem

integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton

L1016 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then so does the actual set of primes above 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target))

theorem

integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton

L1031 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then the primes of the actual integral closure over the base maximal ideal form a singleton.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∃ P : Ideal (integralClosureIntegers base target),
      Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target) = {P}

theorem

integralClosure_isFractionRing

L1050 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isFractionRing

Documentation

The actual integral closure is a fraction ring for the finite field 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isFractionRing :
    IsFractionRing (integralClosureIntegers base target) L

theorem

integralClosure_mem_or_inv_of_integralClosure_valuationRing

L1065 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_mem_or_inv_of_integralClosure_valuationRing

Documentation

If the actual integral closure is a valuation ring, then it satisfies the valuative dichotomy inside the extension field.

This is the local/DVR-oriented bridge for the Henselian frontier: after proving that the finite integral closure is local, one can obtain a valuation-ring instance and feed this theorem into the finite-separable uniqueness API.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_mem_or_inv_of_integralClosure_valuationRing
    [ValuationRing (integralClosureIntegers base target)] :
    ∀ z : L,
      z ∈ (integralClosure base.toDVF.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.toDVF.valuationSubring L).toSubring

theorem

integralClosure_isDedekindDomain

L1087 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isDedekindDomain

Documentation

If the base valuation ring is used as a fraction ring for K and the field extension is separable, the integral closure is Dedekind.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isDedekindDomain
    [IsFractionRing base.toDVF.valuationSubring K] [Algebra.IsSeparable K L] :
    IsDedekindDomain (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton

L1102 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton

Documentation

If the primes of the actual integral closure over the base maximal ideal form a singleton, then the actual integral closure is local.

For integral extensions, every maximal ideal upstairs lies over a maximal ideal downstairs. Since the base valuation ring is local, all maximal ideals upstairs therefore lie over base.maximalIdeal; the singleton hypothesis makes the maximal spectrum upstairs a singleton.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton
    (P : Ideal (integralClosureIntegers base target))
    (hP :
      Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target) = {P}) :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton

L1157 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then the actual integral closure is local.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift

L1170 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift

Documentation

Henselian-facing localness criterion via idempotent lifting in the finite residue fiber.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift
    [Algebra.IsSeparable K L]
    (hlift :
      ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
        IsIdempotentElem e →
          ∃ b : (integralClosureIntegers base target),
            IsIdempotentElem b ∧
              Algebra.TensorProduct.includeRight b = e) :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_valuationRing_of_isLocalRing

L1192 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_valuationRing_of_isLocalRing

Documentation

A local actual integral closure in a finite separable extension of a complete DVF is a valuation ring.

The Henselian frontier can therefore aim only at localness of the finite integral closure. Dedekind theory and mathlib's local Noetherian-domain TFAE then turn that local integral closure into a valuation ring, giving the valuative dichotomy needed by the finite-extension uniqueness bridge.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_valuationRing_of_isLocalRing
    [Algebra.IsSeparable K L]
    [IsLocalRing (integralClosureIntegers base target)] :
    ValuationRing (integralClosureIntegers base target)

theorem

integralClosure_mem_or_inv_of_isLocalRing

L1215 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_mem_or_inv_of_isLocalRing

Documentation

If the actual integral closure is local, then it satisfies the valuative dichotomy inside the extension 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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in

Lean source · statement

theorem integralClosure_mem_or_inv_of_isLocalRing
    [Algebra.IsSeparable K L]
    [IsLocalRing (integralClosureIntegers base target)] :
    ∀ z : L,
      z ∈ (integralClosure base.toDVF.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.toDVF.valuationSubring L).toSubring

theorem

target_valuationSubring_isDiscreteValuationRing

L1226 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isDiscreteValuationRing

Documentation

The chosen target valuation ring remains a DVR.

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 : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem target_valuationSubring_isDiscreteValuationRing
     :
    IsDiscreteValuationRing target.toDVF.valuationSubring

abbrev

integralClosureIntegers

L1242 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosureIntegers

Documentation

The actual integral closure of the base valuation ring in the extension field, for a Henselian 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

abbrev integralClosureIntegers (base : HenselianDVF.{u, v} K)
    (_target : HenselianDVF.{w, x} L) : Type _

theorem

integralClosure_isIntegralClosure

L1249 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isIntegralClosure

Documentation

The actual integral closure is an IsIntegralClosure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isIntegralClosure :
    IsIntegralClosure (integralClosureIntegers base target) base.toDVF.valuationSubring L

theorem

integralClosure_isIntegral

L1258 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isIntegral

Documentation

The actual integral closure is integral over 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isIntegral :
    Algebra.IsIntegral base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_algebraMap_injective

L1267 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_algebraMap_injective

Documentation

The algebra map from the base valuation ring into the actual integral closure 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_algebraMap_injective
     :
    Function.Injective
      (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target))

theorem

integralClosure_faithfulSMul

L1278 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_faithfulSMul

Documentation

The actual integral closure is faithful over 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_faithfulSMul :
    FaithfulSMul base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

moduleFinite_integralClosureIntegers

L1287 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.moduleFinite_integralClosureIntegers

Documentation

In a finite separable field extension, the actual integral closure is module-finite over the base Henselian 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem moduleFinite_integralClosureIntegers
    [Algebra.IsSeparable K L] :
    Module.Finite base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_quasiFinite

L1305 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_quasiFinite

Documentation

In a finite separable field extension, the actual integral closure is quasi-finite over the base Henselian 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_quasiFinite
    [Algebra.IsSeparable K L] :
    Algebra.QuasiFinite base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_base_maximal_fiber_isArtinianRing

L1315 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_isArtinianRing

Documentation

The residue fiber of the finite actual integral closure over the base maximal ideal is Artinian.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_isArtinianRing
    [Algebra.IsSeparable K L] :
    IsArtinianRing (base.maximalIdeal.Fiber (integralClosureIntegers base target))

theorem

integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map

L1326 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map

Documentation

For the actual integral closure, the kernel of the residue-fiber includeRight map is the ideal generated by 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_includeRight_ker_eq_maximalIdeal_map
     :
    RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) =
      base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target))

theorem

integralClosure_base_maximal_map_restrictScalars_le_module_jacobson

L1347 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_map_restrictScalars_le_module_jacobson

Documentation

The ideal generated by the base maximal ideal lies in the module Jacobson radical of the actual integral closure after restricting scalars to the base.

This is the Nakayama/Jacobson component of the desired finite-algebra Henselian-pair transfer, specialized to the Henselian-DVF integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_restrictScalars_le_module_jacobson
     :
    (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring
          (integralClosureIntegers base target))).restrictScalars
      base.toDVF.valuationSubring ≤
        Module.jacobson base.toDVF.valuationSubring (integralClosureIntegers base target)

theorem

integralClosure_base_maximal_map_le_jacobson_bot

L1359 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_map_le_jacobson_bot

Documentation

In a finite separable Henselian extension, the ideal generated by the base maximal ideal lies in the Jacobson radical of the actual integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_le_jacobson_bot
    [Algebra.IsSeparable K L] :
    base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)) ≤
      Ideal.jacobson (⊥ : Ideal (integralClosureIntegers base target))

theorem

integralClosure_idempotent_eq_zero_or_one

L1372 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_idempotent_eq_zero_or_one

Documentation

Idempotents in the actual integral closure in the extension field are trivial.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_idempotent_eq_zero_or_one
    (e : (integralClosureIntegers base target))
    (he : IsIdempotentElem e) :
    e = 0 ∨ e = 1

theorem

integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift

L1385 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift

Documentation

If every idempotent of the residue fiber over the base maximal ideal lifts to an idempotent of the actual integral closure, then that fiber has at most one prime.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_idempotents_lift
    [Algebra.IsSeparable K L]
    (hlift :
      ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
        IsIdempotentElem e →
          ∃ b : (integralClosureIntegers base target),
            IsIdempotentElem b ∧
              Algebra.TensorProduct.includeRight b = e) :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker

L1415 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker

Documentation

Henselian-kernel form of idempotent lifting for the residue fiber of the actual integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem
integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_surjective_henselianRing_ker
    (hsurj :
      Function.Surjective
        (Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker

L1450 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker

Documentation

If the residue-fiber includeRight map has Henselian kernel and is surjective, then the fiber has at most one prime.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_includeRight_surjective_henselianRing_ker
    [Algebra.IsSeparable K L]
    (hsurj :
      Function.Surjective
        (Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker

L1477 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker

Documentation

Henselian-kernel idempotent lifting for the residue fiber of the actual integral closure. The includeRight map is automatically surjective because the base valuation ring is local.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_idempotents_lift_of_includeRight_henselianRing_ker
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker

L1500 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker

Documentation

If the includeRight map to the residue fiber has Henselian kernel, then the fiber has at most one prime.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_includeRight_henselianRing_ker
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.toDVF.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map

L1521 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map

Documentation

Idempotent lifting from the natural Henselian-pair ideal base.maximalIdeal.map in the actual integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_idempotents_lift_of_henselianRing_maximalIdeal_map
    [HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)))] :
    ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
      IsIdempotentElem e →
        ∃ b : (integralClosureIntegers base target),
          IsIdempotentElem b ∧
            Algebra.TensorProduct.includeRight b = e

theorem

integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map

L1546 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map

Documentation

If the ideal generated by the base maximal ideal is Henselian in the actual integral closure, then the residue fiber has at most one prime.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_henselianRing_maximalIdeal_map
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.toDVF.valuationSubring (integralClosureIntegers base target)))] :
    Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))

theorem

integralClosure_primesOver_base_maximal_nonempty

L1568 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_primesOver_base_maximal_nonempty

Documentation

The actual integral closure has at least one prime above 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_nonempty
     :
    Nonempty (Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target))

theorem

integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton

L1584 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then so does the actual set of primes above 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_subsingleton_of_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    Subsingleton
      (Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target))

theorem

integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton

L1599 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then the primes of the actual integral closure over the base maximal ideal form a singleton.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_primesOver_base_maximal_eq_singleton_of_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    ∃ P : Ideal (integralClosureIntegers base target),
      Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target) = {P}

theorem

integralClosure_isFractionRing

L1618 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isFractionRing

Documentation

The actual integral closure is a fraction ring for the finite field 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isFractionRing :
    IsFractionRing (integralClosureIntegers base target) L

theorem

integralClosure_mem_or_inv_of_integralClosure_valuationRing

L1628 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_mem_or_inv_of_integralClosure_valuationRing

Documentation

If the actual integral closure is a valuation ring, then it satisfies the valuative dichotomy inside the extension 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_mem_or_inv_of_integralClosure_valuationRing
    [ValuationRing (integralClosureIntegers base target)] :
    ∀ z : L,
      z ∈ (integralClosure base.toDVF.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.toDVF.valuationSubring L).toSubring

theorem

integralClosure_isDedekindDomain

L1650 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isDedekindDomain

Documentation

If the base valuation ring is used as a fraction ring for K and the field extension is separable, the integral closure is Dedekind.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isDedekindDomain
    [IsFractionRing base.toDVF.valuationSubring K] [Algebra.IsSeparable K L] :
    IsDedekindDomain (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton

L1660 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton

Documentation

If the primes of the actual integral closure over the base maximal ideal form a singleton, then the actual integral closure is local.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L]
    [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_primesOver_base_maximal_eq_singleton
    (P : Ideal (integralClosureIntegers base target))
    (hP :
      Ideal.primesOver base.maximalIdeal (integralClosureIntegers base target) = {P}) :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton

L1715 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton

Documentation

If the residue fiber over the base maximal ideal has at most one prime, then the actual integral closure is local.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_base_maximal_fiber_subsingleton
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift

L1728 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift

Documentation

Henselian-facing localness criterion via idempotent lifting in the finite residue fiber.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_isLocalRing_of_base_maximal_fiber_idempotents_lift
    [Algebra.IsSeparable K L]
    (hlift :
      ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
        IsIdempotentElem e →
          ∃ b : (integralClosureIntegers base target),
            IsIdempotentElem b ∧
              Algebra.TensorProduct.includeRight b = e) :
    IsLocalRing (integralClosureIntegers base target)

theorem

integralClosure_valuationRing_of_isLocalRing

L1745 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_valuationRing_of_isLocalRing

Documentation

A local actual integral closure in a finite separable extension of a Henselian DVF is a 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_valuationRing_of_isLocalRing
    [Algebra.IsSeparable K L]
    [IsLocalRing (integralClosureIntegers base target)] :
    ValuationRing (integralClosureIntegers base target)

theorem

integralClosure_mem_or_inv_of_isLocalRing

L1768 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_mem_or_inv_of_isLocalRing

Documentation

If the actual integral closure is local, then it satisfies the valuative dichotomy inside the extension 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_mem_or_inv_of_isLocalRing
    [Algebra.IsSeparable K L]
    [IsLocalRing (integralClosureIntegers base target)] :
    ∀ z : L,
      z ∈ (integralClosure base.toDVF.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.toDVF.valuationSubring L).toSubring

theorem

target_valuationSubring_isDiscreteValuationRing

L1779 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.target_valuationSubring_isDiscreteValuationRing

Documentation

The chosen Henselian target valuation ring remains a DVR.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem target_valuationSubring_isDiscreteValuationRing
     :
    IsDiscreteValuationRing target.toDVF.valuationSubring

Module documentation

Integral closures of valuation rings

Declarations