Module

Degree.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Degree

37 declarations indexed from sourceView source ↗

Module documentation

Finite valued extension consequences

This file collects theorem-level consequences around finite valued extensions: canonical local-Dedekind degree formulas, uniqueness criteria for extended valuations, and the algebra equivalence identifying an actual integral-closure valuation ring with mathlib's integralClosure.

Imports5

Imported by3

theorem

mem_maximalIdeal_of_map_mem_maximalIdeal

L37 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.mem_maximalIdeal_of_map_mem_maximalIdeal

Documentation

If an element maps into the maximal ideal of a local target ring, then the original element is in the maximal ideal of the local source ring. This is the automatic half of the center/maximal-ideal condition used in the Henselian finite-extension frontier.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation

Lean source · statement

theorem mem_maximalIdeal_of_map_mem_maximalIdeal
    {R : Type u} {S : Type w} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (f : R →+* S) {x : R}
    (hx : f x ∈ IsLocalRing.maximalIdeal S) :
    x ∈ IsLocalRing.maximalIdeal R

theorem

idealOfLE_eq_maximalIdeal_of_isIntegral

L52 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.idealOfLE_eq_maximalIdeal_of_isIntegral

Documentation

Integral valuation overrings have maximal center.

For a valuation overring R ≤ S, if the inclusion is integral, then the center of S on R is the maximal ideal of R. This is the usable form needed in the Henselian finite-extension frontier, where the remaining mathematical work is to prove integrality of the relevant extension valuation-ring inclusions.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation

Lean source · statement

theorem idealOfLE_eq_maximalIdeal_of_isIntegral
    {M : Type u} [Field M] (R S : ValuationSubring M) (hRS : R ≤ S)
    (hIntegral : (R.inclusion S hRS).IsIntegral) :
    ValuationSubring.idealOfLE R S hRS = IsLocalRing.maximalIdeal R

theorem

idealOfLE_eq_maximalIdeal_of_finite

L66 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.idealOfLE_eq_maximalIdeal_of_finite

Documentation

Finite valuation overrings have maximal center.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation

Lean source · statement

theorem idealOfLE_eq_maximalIdeal_of_finite
    {M : Type u} [Field M] (R S : ValuationSubring M) (hRS : R ≤ S)
    (hFinite : (R.inclusion S hRS).Finite) :
    ValuationSubring.idealOfLE R S hRS = IsLocalRing.maximalIdeal R

def

integralClosureValuationSubringIntegerMapOfMemOrInv

L81 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureValuationSubringIntegerMapOfMemOrInv

Documentation

The canonical integer map from the base valuation ring to the valuation subring constructed from the actual integral closure. Its definition uses the exact pullback theorem for the constructed integral-closure valuation subring, so no auxiliary alias of the base or target valuation ring is introduced.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 integralClosureValuationSubringIntegerMapOfMemOrInv
    (base : CompleteDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    base.valuationSubring →+*
      integralClosureValuationSubringOfMemOrInv
        (L := L) base.valuation hval where
  toFun a :=
    ⟨algebraMap K L (a : K),
      (integralClosureValuationSubringOfMemOrInv_pullback
        (L := L) base.valuation hval (a : K)).2 a.2⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' := by intro a b; ext; simp
  map_mul' := by intro a b; ext; simp

theorem

integralClosureValuationSubringIntegerMapOfMemOrInv_apply

L101 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureValuationSubringIntegerMapOfMemOrInv_apply

Documentation

The finite-extension integer map into the integral closure is the ambient algebra map.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 integralClosureValuationSubringIntegerMapOfMemOrInv_apply
    (base : CompleteDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (a : base.valuationSubring) :
    ((integralClosureValuationSubringIntegerMapOfMemOrInv
      (K := K) (L := L) base hval a :
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval) : L) =
      algebraMap K L (a : K)

theorem

integralClosureValuationSubringIntegerMapOfMemOrInv_injective

L120 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.integralClosureValuationSubringIntegerMapOfMemOrInv_injective

Documentation

The canonical integer map into the valuation subring built from the actual integral closure is injective. This is the ring-theoretic input needed to turn a prime over the base maximal ideal into a nonzero prime of the constructed integral-closure valuation ring.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 integralClosureValuationSubringIntegerMapOfMemOrInv_injective
    (base : CompleteDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    Function.Injective
      (integralClosureValuationSubringIntegerMapOfMemOrInv
        (K := K) (L := L) base hval)

theorem

maximalIdeal_liesOver_of_hasExtension

L147 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_liesOver_of_hasExtension

Documentation

The target maximal ideal lies over the base maximal ideal for any actual extension of the chosen valuations. This is the record-free form of the local map property used by finite-extension invariants.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 maximalIdeal_liesOver_of_hasExtension
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation] :
    target.maximalIdeal.LiesOver base.maximalIdeal

theorem

idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

L163 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

Documentation

The center of an extension valuation ring on the constructed actual integral-closure valuation subring contracts to the base maximal ideal.

This is the nontrivial half of locating the center: the center is represented as ValuationSubring.idealOfLE, and its contraction along the canonical map from the base valuation ring is computed using the HasExtension valuation inequality. A later Henselian local-integral-closure theorem can combine this with uniqueness of primes above the base maximal ideal to identify the center with the maximal ideal of the constructed integral closure.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 · full declaration

theorem idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (base : CompleteDVF.{u, v} K) (vL : _root_.Valuation L ΓL)
    [base.valuation.HasExtension vL]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    let B :=
      integralClosureValuationSubringOfMemOrInv
        (L := L) base.valuation hval
    let hvL_le : B ≤ vL.valuationSubring :=
      integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
        (L := L) base.valuation vL hval
    (ValuationSubring.idealOfLE B vL.valuationSubring hvL_le).comap
        (integralClosureValuationSubringIntegerMapOfMemOrInv
          (K := K) (L := L) base hval) =
      base.maximalIdeal := by
  let B :=
    integralClosureValuationSubringOfMemOrInv
      (L := L) base.valuation hval
  let hvL_le : B ≤ vL.valuationSubring :=
    integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
      (L := L) base.valuation vL hval
  let i : base.valuationSubring →+* B :=
    integralClosureValuationSubringIntegerMapOfMemOrInv
      (K := K) (L := L) base hval
  apply Ideal.ext
  intro a
  rw [Ideal.mem_comap]
  change B.inclusion vL.valuationSubring hvL_le (i a) ∈
      IsLocalRing.maximalIdeal vL.valuationSubring ↔
    a ∈ IsLocalRing.maximalIdeal base.valuation.valuationSubring
  rw [Valuation.mem_maximalIdeal_iff (v := vL)]
  rw [Valuation.mem_maximalIdeal_iff (v := base.valuation)]
  change vL
      ((B.inclusion vL.valuationSubring hvL_le (i a) :
        vL.valuationSubring) : L) < 1 ↔
    base.valuation (a : K) < 1
  have hcoe :
      ((B.inclusion vL.valuationSubring hvL_le (i a) :
        vL.valuationSubring) : L) =
        algebraMap K L (a : K) := by
    rfl
  rw [hcoe]
  exact Valuation.HasExtension.val_map_lt_one_iff base.valuation vL (a : K)

theorem

prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

L219 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

Documentation

In a finite separable extension, once the actual integral closure has the valuation-ring dichotomy, the constructed integral-closure valuation ring has a unique prime over the base maximal ideal.

The proof uses real structure, not a certificate: the constructed valuation ring is the actual integral closure, hence Dedekind over the base DVR; a prime whose contraction is the base maximal ideal is nonzero by injectivity of the canonical integer map, hence maximal by the dimension-one property, and then equal to the unique maximal ideal because the constructed 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 y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
    (base : CompleteDVF.{u, v} K)
    [Algebra.IsSeparable K L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (P :
      Ideal
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval))
    (hP : P.IsPrime)
    (hcomap :
      P.comap
          (integralClosureValuationSubringIntegerMapOfMemOrInv
            (K := K) (L := L) base hval) =
        base.maximalIdeal) :
    P =
      IsLocalRing.maximalIdeal
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval)

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_hasExtension

L289 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_hasExtension

Documentation

The local-Dedekind fundamental identity in record-free form: for the actual valuation rings attached to a finite valued field extension, mathlib's ramification index times mathlib's inertia degree is the field degree.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_hasExtension
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_isIntegralClosure

L301 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_isIntegralClosure

Documentation

If the target valuation ring is the integral closure of the base valuation ring in a finite separable field extension, then the local-Dedekind ramification identity holds without separately assuming module-finiteness.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_isIntegralClosure
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L] :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L

theorem

target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_local_inclusion

L321 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_local_inclusion

Documentation

Local-inclusion form of the integral-closure frontier for the chosen target valuation ring. Once the actual integral closure has the valuation-ring dichotomy, a local inclusion from the constructed integral-closure valuation subring into the target valuation ring identifies the target valuation ring with the actual integral closure.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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_integralClosure_mem_or_inv_of_local_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetLocal :
      IsLocalHom
        ((integralClosureValuationSubringOfMemOrInv
            (L := L) base.valuation hval).inclusion
          target.valuation.valuationSubring
          (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
            (L := L) base.valuation target.valuation hval))) :
    IsIntegralClosure target.valuationSubring base.valuationSubring L

theorem

target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal

L365 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal

Documentation

Center-prime form of the same integral-closure bridge. This is the form expected after the Henselian finite-extension argument proves that the center of the target valuation ring on the constructed integral-closure valuation ring is the maximal ideal.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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_integralClosure_mem_or_inv_of_center_eq_maximalIdeal
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenter :
      ValuationSubring.idealOfLE
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval)
        target.valuation.valuationSubring
        (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval) =
          IsLocalRing.maximalIdeal
            (integralClosureValuationSubringOfMemOrInv
              (L := L) base.valuation hval)) :
    IsIntegralClosure target.valuationSubring base.valuationSubring L

theorem

target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_integral_inclusion

L410 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_integral_inclusion

Documentation

Integral-inclusion form of the target integral-closure bridge. Once the actual integral closure has the valuation-ring dichotomy, integrality of the inclusion from that constructed valuation ring into the target valuation ring forces the target to be the actual integral closure.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 · full declaration

theorem
target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_integral_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetIntegral :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      (B.inclusion target.valuation.valuationSubring htarget_le).IsIntegral) :
    IsIntegralClosure target.valuationSubring base.valuationSubring L := by
  refine (
target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal
    (K := K) (L := L) base target hval ?_)
  let B :=
    integralClosureValuationSubringOfMemOrInv
      (L := L) base.valuation hval
  let htarget_le : B ≤ target.valuation.valuationSubring :=
    integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
      (L := L) base.valuation target.valuation hval
  exact idealOfLE_eq_maximalIdeal_of_isIntegral B target.valuation.valuationSubring
    htarget_le (by simpa [B, htarget_le] using htargetIntegral)

theorem

target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_mem_iff

L441 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_mem_iff

Documentation

Elementwise center form of the target integral-closure bridge.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 · full declaration

theorem target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_mem_iff
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenterMem :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      ∀ x : B,
        B.inclusion target.valuation.valuationSubring htarget_le x ∈
            IsLocalRing.maximalIdeal target.valuation.valuationSubring ↔
          x ∈ IsLocalRing.maximalIdeal B) :
    IsIntegralClosure target.valuationSubring base.valuationSubring L := by
  refine (
target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal
    (K := K) (L := L) base target hval ?_)
  let B :=
    integralClosureValuationSubringOfMemOrInv
      (L := L) base.valuation hval
  let htarget_le : B ≤ target.valuation.valuationSubring :=
    integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
      (L := L) base.valuation target.valuation hval
  exact
    idealOfLE_eq_maximalIdeal_of_mem_maximalIdeal_iff
      B target.valuation.valuationSubring htarget_le
      (by simpa [B, htarget_le] using htargetCenterMem)

theorem

moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_local_inclusion

L477 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_local_inclusion

Documentation

Module-finiteness of the target valuation ring from the Henselian frontier-shaped hypotheses: valuative dichotomy for the actual integral closure plus local inclusion into the target.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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_integralClosure_mem_or_inv_of_local_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetLocal :
      IsLocalHom
        ((integralClosureValuationSubringOfMemOrInv
            (L := L) base.valuation hval).inclusion
          target.valuation.valuationSubring
          (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
            (L := L) base.valuation target.valuation hval))) :
    Module.Finite base.valuationSubring target.valuationSubring

theorem

moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal

L501 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_center_eq_maximalIdeal

Documentation

Center-prime form of module-finiteness for the target 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 y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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_integralClosure_mem_or_inv_of_center_eq_maximalIdeal
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenter :
      ValuationSubring.idealOfLE
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval)
        target.valuation.valuationSubring
        (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval) =
          IsLocalRing.maximalIdeal
            (integralClosureValuationSubringOfMemOrInv
              (L := L) base.valuation hval)) :
    Module.Finite base.valuationSubring target.valuationSubring

theorem

moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_integral_inclusion

L529 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_integral_inclusion

Documentation

Integral-inclusion form of module-finiteness for the target 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 y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_integral_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetIntegral :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      (B.inclusion target.valuation.valuationSubring htarget_le).IsIntegral) :
    Module.Finite base.valuationSubring target.valuationSubring := by
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L :=
    target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_integral_inclusion
      (K := K) (L := L) base target hval htargetIntegral
  exact moduleFinite_target_valuationSubring_of_isIntegralClosure
    (K := K) (L := L) base target

theorem

moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_center_mem_iff

L555 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_center_mem_iff

Documentation

Elementwise center form of module-finiteness for the target 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 y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem moduleFinite_target_valuationSubring_of_integralClosure_mem_or_inv_of_center_mem_iff
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenterMem :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      ∀ x : B,
        B.inclusion target.valuation.valuationSubring htarget_le x ∈
            IsLocalRing.maximalIdeal target.valuation.valuationSubring ↔
          x ∈ IsLocalRing.maximalIdeal B) :
    Module.Finite base.valuationSubring target.valuationSubring := by
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L :=
    target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_mem_iff
      (K := K) (L := L) base target hval htargetCenterMem
  exact moduleFinite_target_valuationSubring_of_isIntegralClosure
    (K := K) (L := L) base target

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_local_inclusion

L585 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_local_inclusion

Documentation

Local-inclusion form of the local-Dedekind fundamental identity. This is the degree bridge used after the Henselian proof supplies the valuative dichotomy and target local-overring condition.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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
ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_local_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetLocal :
      IsLocalHom
        ((integralClosureValuationSubringOfMemOrInv
            (L := L) base.valuation hval).inclusion
          target.valuation.valuationSubring
          (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
            (L := L) base.valuation target.valuation hval))) :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L

theorem

ideal_degree_eq_finrank_of_center_eq_maximalIdeal

L611 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.IntegralClosureMemOrInv.ideal_degree_eq_finrank_of_center_eq_maximalIdeal

Documentation

Center-prime form of the local-Dedekind fundamental identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 IntegralClosureMemOrInv.ideal_degree_eq_finrank_of_center_eq_maximalIdeal
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenter :
      ValuationSubring.idealOfLE
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval)
        target.valuation.valuationSubring
        (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval) =
          IsLocalRing.maximalIdeal
            (integralClosureValuationSubringOfMemOrInv
              (L := L) base.valuation hval)) :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_integral_inclusion

L639 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_integral_inclusion

Documentation

Integral-inclusion form of the local-Dedekind fundamental identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem
ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_integral_inclusion
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetIntegral :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      (B.inclusion target.valuation.valuationSubring htarget_le).IsIntegral) :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L := by
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L :=
    target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_integral_inclusion
      (K := K) (L := L) base target hval htargetIntegral
  exact ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_isIntegralClosure
    (K := K) (L := L) base target

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_center_mem_iff

L666 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_center_mem_iff

Documentation

Elementwise center form of the local-Dedekind fundamental identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem
ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_center_mem_iff
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenterMem :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      ∀ x : B,
        B.inclusion target.valuation.valuationSubring htarget_le x ∈
            IsLocalRing.maximalIdeal target.valuation.valuationSubring ↔
          x ∈ IsLocalRing.maximalIdeal B) :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L := by
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L :=
    target_valuationSubring_isIntegralClosure_of_integralClosure_mem_or_inv_of_center_mem_iff
      (K := K) (L := L) base target hval htargetCenterMem
  exact ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_isIntegralClosure
    (K := K) (L := L) base target

theorem

isDefectless_of_isIntegralClosure

L696 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.isDefectless_of_isIntegralClosure

Documentation

A valued extension whose target is the integral closure is defectless.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 isDefectless_of_isIntegralClosure
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L] :
    ValuedExtension.IsDefectless base.toDVF target.toDVF

theorem

maximalIdeal_liesOver

L712 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_liesOver

Documentation

The target maximal ideal lies over the base maximal ideal for a valued extension.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 maximalIdeal_liesOver :
    target.maximalIdeal.LiesOver base.maximalIdeal

theorem

residueDegree_eq_finrank_quotient

L718 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree_eq_finrank_quotient

Documentation

Residue degree is the linear rank of the target residue field over the source residue field.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 · full declaration

theorem residueDegree_eq_finrank_quotient
     :
    letI : target.maximalIdeal.LiesOver base.maximalIdeal :=
      (maximalIdeal_liesOver base target)
    (ValuedExtension.residueDegree base.toDVF target.toDVF) =
      Module.finrank
        (base.valuationSubring ⧸ base.maximalIdeal)
        (target.valuationSubring ⧸ target.maximalIdeal) := by
  exact Ideal.inertiaDeg_eq_of_isMaximal base.maximalIdeal target.maximalIdeal

theorem

residueDegree_pos

L730 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree_pos

Documentation

The residue degree of a finite extension is strictly positive.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 residueDegree_pos
    [Module.Finite base.valuationSubring target.valuationSubring] :
    0 < (ValuedExtension.residueDegree base.toDVF target.toDVF)

theorem

residueField_finiteDimensional_of_moduleFinite

L742 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.residueField_finiteDimensional_of_moduleFinite

Documentation

A finite extension of valuation rings induces a finite-dimensional residue field extension. This is the source behind using a primitive element for the residue extension: mathlib's inertia degree is the residue-field finrank.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 residueField_finiteDimensional_of_moduleFinite
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring] :
    FiniteDimensional base.residueField target.residueField

theorem

residueDegree_ne_zero

L753 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree_ne_zero

Documentation

The residue degree of a finite extension is nonzero.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 residueDegree_ne_zero
    [Module.Finite base.valuationSubring target.valuationSubring] :
    (ValuedExtension.residueDegree base.toDVF target.toDVF) ≠ 0

theorem

ramificationIndex_ne_zero

L760 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_ne_zero

Documentation

The ramification index of a finite extension is nonzero.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ramificationIndex_ne_zero
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) ≠ 0

theorem

ramificationIndex_mul_residueDegree_eq_degree

L773 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_mul_residueDegree_eq_degree

Documentation

The actual local-Dedekind fundamental identity for the chosen valuation rings: in the local case, the mathlib ramification index times the mathlib inertia degree is the field degree.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ramificationIndex_mul_residueDegree_eq_degree
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF

theorem

ramificationIndex_mul_residueDegree_eq_degree_of_isIntegralClosure

L786 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_mul_residueDegree_eq_degree_of_isIntegralClosure

Documentation

Integral-closure form of the local-Dedekind degree identity for a valued finite separable extension.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ramificationIndex_mul_residueDegree_eq_degree_of_isIntegralClosure
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L] :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF

theorem

ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_local_inclusion

L802 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_local_inclusion

Documentation

Local-inclusion form of the canonical Dedekind degree identity. The remaining Henselian input is exactly the valuative dichotomy for the integral closure and the local-overring condition; this theorem performs the algebraic degree/e/f bridge.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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
ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_local_inclusion
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetLocal :
      IsLocalHom
        ((integralClosureValuationSubringOfMemOrInv
            (L := L) base.valuation hval).inclusion
          target.valuation.valuationSubring
          (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
            (L := L) base.valuation target.valuation hval))) :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF

theorem

degree_eq_of_center_eq_maximalIdeal

L826 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.IntegralClosureMemOrInv.degree_eq_of_center_eq_maximalIdeal

Documentation

Center-prime form of the canonical Dedekind degree identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 IntegralClosureMemOrInv.degree_eq_of_center_eq_maximalIdeal
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenter :
      ValuationSubring.idealOfLE
        (integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval)
        target.valuation.valuationSubring
        (integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval) =
          IsLocalRing.maximalIdeal
            (integralClosureValuationSubringOfMemOrInv
              (L := L) base.valuation hval)) :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF

theorem

ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_integral_inclusion

L852 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_integral_inclusion

Documentation

Integral-inclusion form of the canonical Dedekind degree identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem
ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_integral_inclusion
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetIntegral :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      (B.inclusion target.valuation.valuationSubring htarget_le).IsIntegral) :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF := by
  simpa [ramificationIndex, residueDegree,
    ramificationIndex, residueDegree, degree] using (
ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_integral_inclusion
    (K := K) (L := L) base target hval htargetIntegral)

theorem

ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_center_mem_iff

L877 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_center_mem_iff

Documentation

Elementwise center form of the canonical Dedekind degree identity.

Source context 10 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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

theorem
ramificationIndex_mul_residueDegree_eq_degree_of_integralClosure_mem_or_inv_of_center_mem_iff
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenterMem :
      let B :=
        integralClosureValuationSubringOfMemOrInv
          (L := L) base.valuation hval
      let htarget_le : B ≤ target.valuation.valuationSubring :=
        integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.valuation target.valuation hval
      ∀ x : B,
        B.inclusion target.valuation.valuationSubring htarget_le x ∈
            IsLocalRing.maximalIdeal target.valuation.valuationSubring ↔
          x ∈ IsLocalRing.maximalIdeal B) :
    (ValuedExtension.ramificationIndex base.toDVF target.toDVF) *
        ValuedExtension.residueDegree base.toDVF target.toDVF =
      ValuedExtension.degree base.toDVF target.toDVF := by
  simpa [ramificationIndex, residueDegree,
    ramificationIndex, residueDegree, degree] using
    (ideal_ramificationIdx_mul_inertiaDeg_eq_finrank_of_integralClosure_mem_or_inv_of_center_mem_iff
      (K := K) (L := L) base target hval htargetCenterMem)

theorem

ideal_ramificationIdx_mul_inertiaDeg_eq_finrank

L906 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.ideal_ramificationIdx_mul_inertiaDeg_eq_finrank

Documentation

The local-Dedekind formula in raw mathlib notation.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.Valuation
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 ideal_ramificationIdx_mul_inertiaDeg_eq_finrank
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal *
      target.maximalIdeal.inertiaDeg base.valuationSubring = Module.finrank K L

Module documentation

Finite valued extension consequences

Declarations