Module

FiniteIntegralClosure.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteIntegralClosure

21 declarations indexed from sourceView source ↗

Module documentation

Finite integral closures over complete DVFs

This file provides record-free theorems for the integral closure of a complete-DVF valuation ring in a finite separable field extension.

Imports2

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Core
Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Imported by16

theorem

integralClosure_base_maximal_map_isAdicComplete_of_finite_separable

L63 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_map_isAdicComplete_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure is complete for the ideal generated by the base maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_base_maximal_map_isAdicComplete_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    IsAdicComplete
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring
          (integralClosure base.valuationSubring L)))
      (integralClosure base.valuationSubring L)

theorem

integralClosure_henselianRing_of_finite_separable

L100 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_henselianRing_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure of the base valuation ring is Henselian along the ideal generated by the base maximal ideal.

This is independent of any pre-existing Extension record. It is the source-producing input used before canonical ramification and residue invariants have been packaged.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_henselianRing_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    HenselianRing (integralClosure base.valuationSubring L)
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring
          (integralClosure base.valuationSubring L)))

theorem

integralClosure_base_maximal_fiber_subsingleton_of_finite_separable

L122 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_fiber_subsingleton_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the residue fiber of the actual integral closure over the base maximal ideal has at most one prime.

The proof combines finite Artinian residue fibers with Henselian idempotent lifting from integralClosure_henselianRing_of_finite_separable.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_base_maximal_fiber_subsingleton_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    Subsingleton
      (PrimeSpectrum
        (base.maximalIdeal.Fiber (integralClosure base.valuationSubring L)))

theorem

integralClosure_isLocalRing_of_finite_separable

L183 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isLocalRing_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure of the base valuation ring is local.

This is the record-free localness form of the Henselian finite-extension frontier. It uses the residue-fiber singleton theorem above and integral lies-over, without assuming a chosen target valuation ring.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_isLocalRing_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    IsLocalRing (integralClosure base.valuationSubring L)

def

maximalIdeal

L255 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.CanonicalIntegralClosure.maximalIdeal

Documentation

The maximal ideal of the integral closure, using the finite separable localness theorem above.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

def CanonicalIntegralClosure.maximalIdeal
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    Ideal (integralClosure base.valuationSubring L)

theorem

integralClosure_base_maximal_map_le_maximalIdeal_of_finite_separable

L265 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_map_le_maximalIdeal_of_finite_separable

Documentation

In the actual integral closure, the ideal generated by the base maximal ideal is contained in the upstairs maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_base_maximal_map_le_maximalIdeal_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    base.maximalIdeal.map
        (algebraMap base.valuationSubring
          (integralClosure base.valuationSubring L)) ≤
      CanonicalIntegralClosure.maximalIdeal (K := K) (L := L) base

theorem

integralClosure_base_maximal_map_ne_bot_of_finite_separable

L295 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_base_maximal_map_ne_bot_of_finite_separable

Documentation

In a finite separable extension, the image of the base maximal ideal is nonzero.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosure_base_maximal_map_ne_bot_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    base.maximalIdeal.map
      (algebraMap base.valuationSubring
        (integralClosure base.valuationSubring L)) ≠ ⊥

theorem

integralClosure_not_isField_of_finite_separable

L311 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_not_isField_of_finite_separable

Documentation

The integral closure in a nontrivial finite separable extension is not a field.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosure_not_isField_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ¬ IsField (integralClosure base.valuationSubring L)

theorem

integralClosure_isDiscreteValuationRing_of_finite_separable

L331 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_isDiscreteValuationRing_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure of the base valuation ring is a DVR.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_isDiscreteValuationRing_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    IsDiscreteValuationRing (integralClosure base.valuationSubring L)

theorem

exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow

L357 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow

Documentation

In the actual integral closure, the ideal generated by the base maximal ideal is a power of the upstairs maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ n : ℕ,
      base.maximalIdeal.map
          (algebraMap base.valuationSubring
            (integralClosure base.valuationSubring L)) =
        CanonicalIntegralClosure.maximalIdeal (K := K) (L := L) base ^ n

theorem

exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow_pos

L391 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow_pos

Documentation

In the actual integral closure, the ideal generated by the base maximal ideal is a positive power of the upstairs maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem exists_integralClosure_base_maximal_map_eq_maximalIdeal_pow_pos
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ n : ℕ,
      0 < n ∧
        base.maximalIdeal.map
            (algebraMap base.valuationSubring
              (integralClosure base.valuationSubring L)) =
          CanonicalIntegralClosure.maximalIdeal (K := K) (L := L) base ^ n

theorem

integralClosure_maximalIdeal_isAdicComplete_of_finite_separable

L430 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_maximalIdeal_isAdicComplete_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure is complete for its own maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_maximalIdeal_isAdicComplete_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    IsAdicComplete
      (CanonicalIntegralClosure.maximalIdeal (K := K) (L := L) base)
      (integralClosure base.valuationSubring L)

theorem

exists_integralClosure_standard_rankOneDiscrete_valuation

L461 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_standard_rankOneDiscrete_valuation

Documentation

A packaged rank-one discrete valuation coming from the actual integral closure, together with its valuation-subring comparison.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem exists_integralClosure_standard_rankOneDiscrete_valuation
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ ΓL : Type,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vL.IsRankOneDiscrete,
            ∃ _ : (integralClosure base.valuationSubring L) ≃+*
              vL.valuationSubring,
              True

theorem

exists_integralClosure_standard_complete_valuation_data

L490 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_standard_complete_valuation_data

Documentation

The actual integral closure supplies a rank-one discrete standard adic valuation, its own maximal-ideal adic completeness, and the comparison of that valuation ring with the actual integral closure.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem exists_integralClosure_standard_complete_valuation_data
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ ΓL : Type,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vL.IsRankOneDiscrete,
            IsAdicComplete
              (CanonicalIntegralClosure.maximalIdeal (K := K) (L := L) base)
              (integralClosure base.valuationSubring L) ∧
              ∃ _ : (integralClosure base.valuationSubring L) ≃+*
                vL.valuationSubring,
                True

theorem

exists_integralClosure_standard_completeDVF

L513 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_standard_completeDVF

Documentation

The actual integral closure supplies a complete-DVF target whose valuation subring is ring-equivalent to the actual integral closure.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem exists_integralClosure_standard_completeDVF
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ target : CompleteDVF.{w, 0} L,
      (∀ z : L,
        z ∈ target.valuation.valuationSubring ↔
          z ∈ (integralClosure base.valuationSubring L).toSubring) ∧
          ∃ _ : (integralClosure base.valuationSubring L) ≃+*
            target.valuationSubring,
            True

theorem

exists_integralClosure_standard_fundamental_identity

L634 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_standard_fundamental_identity

Documentation

The standard complete-DVF target supplied by the actual integral closure, together with its valuation-extension property, integral-closure comparison, and the fundamental ramification identity.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · full declaration

theorem exists_integralClosure_standard_fundamental_identity
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ target : CompleteDVF.{w, 0} L,
      ∃ hExt : base.valuation.HasExtension target.valuation,
        letI : base.valuation.HasExtension target.valuation := hExt
        IsIntegralClosure target.valuationSubring
          base.valuationSubring L ∧
          ValuedExtension.degree base.toDVF target.toDVF =
            ValuedExtension.ramificationIndex base.toDVF target.toDVF *
              ValuedExtension.residueDegree base.toDVF target.toDVF := by
  obtain ⟨target, hmem, _hequiv⟩ :=
    exists_integralClosure_standard_completeDVF
      (K := K) (L := L) base
  have hExt : base.valuation.HasExtension target.valuation := by
    apply _root_.Valuation.HasExtension.ofComapInteger
    ext a
    change
      algebraMap K L a ∈ target.valuation.valuationSubring ↔
        a ∈ base.valuation.valuationSubring
    rw [hmem]
    exact algebraMap_mem_integralClosure_valuationSubring_iff
      (L := L) base.valuation a
  refine ⟨target, hExt, ?_⟩
  let : base.valuation.HasExtension target.valuation := hExt
  have hIntegralClosure :
      IsIntegralClosure target.valuationSubring
        base.valuationSubring L := by
    refine
      { algebraMap_injective := ?_
        isIntegral_iff := ?_ }
    · intro x y hxy
      exact Subtype.ext hxy
    · intro z
      constructor
      · intro hz
        have hzmem :
            z ∈ (integralClosure base.valuationSubring L).toSubring := hz
        exact ⟨⟨z, (hmem z).2 hzmem⟩, rfl⟩
      · rintro ⟨y, rfl⟩
        exact (hmem (y : L)).1 y.2
  refine ⟨hIntegralClosure, ?_⟩
  let :
      IsIntegralClosure target.valuationSubring
        base.valuationSubring L := hIntegralClosure
  let : IsScalarTower base.valuationSubring
      target.valuationSubring L := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    rfl
  exact isDefectless_of_isIntegralClosure
    (K := K) (L := L) base target

theorem

integralClosure_valuationRing_of_finite_separable

L689 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosure_valuationRing_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the actual integral closure of the base valuation ring is a valuation ring.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem integralClosure_valuationRing_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ValuationRing (integralClosure base.valuationSubring L)

theorem

mem_or_inv_of_finite_separable

L711 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.CanonicalIntegralClosure.mem_or_inv_of_finite_separable

Documentation

Record-free valuative dichotomy for the integral closure in a finite separable extension of a complete DVF.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · statement

theorem CanonicalIntegralClosure.mem_or_inv_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∀ z : L,
      z ∈ (integralClosure base.valuationSubring L).toSubring ∨
        z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring

theorem

exists_integralClosure_valuationSubring_of_finite_separable

L743 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.exists_integralClosure_valuationSubring_of_finite_separable

Documentation

In a finite separable extension of a complete DVF, the integral closure itself supplies a valuation subring whose canonical valuation extends the base valuation.

This is the record-free source used before a CompleteDVF target has been chosen.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ValuedExtension
open DiscreteValuationField.Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]

/- The algebra map from the base valuation ring into the integral
closure is injective. -/

Lean source · full declaration

theorem exists_integralClosure_valuationSubring_of_finite_separable
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L] :
    ∃ B : ValuationSubring L,
      ∃ hExt : base.valuation.HasExtension B.valuation,
        letI : base.valuation.HasExtension B.valuation := hExt
        B.toSubring = (integralClosure base.valuationSubring L).toSubring ∧
          IsIntegralClosure B base.valuationSubring L := by
  exact
    exists_integralClosure_valuationSubring_isIntegralClosure_of_forall_mem_or_inv
      (L := L) base.valuation
      (CanonicalIntegralClosure.mem_or_inv_of_finite_separable
        (K := K) (L := L) base)

Module documentation

Finite integral closures over complete DVFs

Declarations