Module

AdicCompletion.lean

Nyll.AlgebraicCurves.Valuations.AdicCompletion

39 declarations indexed from sourceView source ↗

Module documentation

AdicCompletion

Adic completions of a Dedekind-domain fraction field retain the discrete valuation, integral subring, and residue field at the chosen height-one prime.

Imports10

Mathlib.Topology.Algebra.Valued.ValuationTopology
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.Analysis.Normed.Ring.Lemmas
Mathlib.NumberTheory.RamificationInertia.Inertia
Mathlib.RingTheory.Valuation.Discrete.Basic
Mathlib.Topology.Path
Mathlib.Algebra.Group.Int.TypeTags
Mathlib.RingTheory.Valuation.Discrete.RankOne

Imported by12

instance

(anonymous instance)

L38 ↗

Source context 3 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
open IsDedekindDomain

Lean source · full declaration

instance {R : Type*} [CommRing R] [IsDedekindDomain R] (K : Type*) [Field K] [Countable K]
    [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    TopologicalSpace.SeparableSpace (v.adicCompletion K) where
  exists_countable_dense :=
    ⟨_, Set.countable_range _, HeightOneSpectrum.denseRange_algebraMap (K := K) (v := v)⟩

lemma

intValuation_eq_coe_neg_multiplicity

L44 ↗

IsDedekindDomain.HeightOneSpectrum.intValuation_eq_coe_neg_multiplicity

Source context 3 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
open IsDedekindDomain

Lean source · statement

lemma intValuation_eq_coe_neg_multiplicity {A : Type*} [CommRing A] [IsDedekindDomain A]
    (v : HeightOneSpectrum A) {a : A} (hnz : a ≠ 0) :
    v.intValuation a = WithZero.exp (-(multiplicity v.asIdeal (Ideal.span {a}) : ℤ))

theorem

maximalIdeal_le

L63 ↗

IsLocalRing.maximalIdeal_le

Source context 1 command

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

section

Lean source · statement

theorem IsLocalRing.maximalIdeal_le {R : Type*} [CommSemiring R] [IsLocalRing R] {J :
  Ideal R}
    (hJ : J ≠ ⊤) (h : IsLocalRing.maximalIdeal R ≤ J) :
    J.IsMaximal

lemma

subtype_inj

L75 ↗

ValuationSubring.subtype_inj

Source context 2 commands

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

section
variable {F : Type*} [Field F]

Lean source · statement

lemma ValuationSubring.subtype_inj {R : ValuationSubring F} {x y : R} :
    R.subtype x = R.subtype y ↔ x = y

theorem

valued_eq_one_of_isUnit

L79 ↗

ValuationSubring.valued_eq_one_of_isUnit

Source context 2 commands

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

section
variable {F : Type*} [Field F]

Lean source · statement

theorem ValuationSubring.valued_eq_one_of_isUnit {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring)
    (hx : IsUnit x) : Valued.v x.val = 1

theorem

isUnit_of_valued_eq_one

L89 ↗

ValuationSubring.isUnit_of_valued_eq_one

Source context 2 commands

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

section
variable {F : Type*} [Field F]

Lean source · statement

theorem ValuationSubring.isUnit_of_valued_eq_one {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring)
    (hx : Valued.v x.val = 1) : IsUnit x

theorem

isUnit_iff_valued_eq_one

L99 ↗

ValuationSubring.isUnit_iff_valued_eq_one

Source context 2 commands

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

section
variable {F : Type*} [Field F]

Lean source · statement

theorem ValuationSubring.isUnit_iff_valued_eq_one {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring) :
    IsUnit x ↔ Valued.v x.val = 1

lemma

exists_ofAdd_natCast_of_le_one

L113 ↗

IsDedekindDomain.HeightOneSpectrum.exists_ofAdd_natCast_of_le_one

Source context 4 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
section Multiplicative
open scoped WithZero

Lean source · statement

lemma exists_ofAdd_natCast_of_le_one {x : ℤᵐ⁰} (hx : x ≠ 0) (hx' : x ≤ 1) :
    ∃ (k : ℕ), (Multiplicative.ofAdd (-(k : ℤ))) = x

lemma

exists_ofAdd_natCast_lt

L125 ↗

IsDedekindDomain.HeightOneSpectrum.exists_ofAdd_natCast_lt

Source context 4 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
section Multiplicative
open scoped WithZero

Lean source · statement

lemma exists_ofAdd_natCast_lt {x : ℤᵐ⁰} (hx : x ≠ 0) :
    ∃ (k : ℕ), (Multiplicative.ofAdd (-(k : ℤ))) < x

lemma

ne_zero_of_some_le_intValuation

L143 ↗

IsDedekindDomain.HeightOneSpectrum.ne_zero_of_some_le_intValuation

Source context 3 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)

Lean source · statement

lemma ne_zero_of_some_le_intValuation {a : A} {m : Multiplicative ℤ} (h : m ≤ v.intValuation a)
    : a ≠ 0

lemma

emultiplicity_eq_of_valuation_eq_ofAdd

L148 ↗

IsDedekindDomain.HeightOneSpectrum.emultiplicity_eq_of_valuation_eq_ofAdd

Source context 3 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)

Lean source · statement

lemma emultiplicity_eq_of_valuation_eq_ofAdd {a : A} {k : ℕ}
    (hv : v.intValuation a = (Multiplicative.ofAdd (-(k : ℤ)))) :
    emultiplicity v.asIdeal (Ideal.span {a}) = k

lemma

exists_adicValued_mul_sub_le

L160 ↗

IsDedekindDomain.HeightOneSpectrum.exists_adicValued_mul_sub_le

Source context 3 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)

Lean source · statement

lemma exists_adicValued_mul_sub_le {a b : A} {γ : WithZero (Multiplicative ℤ)} (hγ : γ ≠ 0)
    (hle : γ ≤ v.intValuation a)
    (hle' : v.intValuation b ≤ v.intValuation a) :
    ∃ y, v.intValuation (y * a - b) ≤ γ

lemma

exists_adicValued_sub_lt_of_adicValued_le_one

L187 ↗

IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicValued_le_one

Source context 4 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open MonoidWithZeroHom in

Lean source · statement

lemma exists_adicValued_sub_lt_of_adicValued_le_one {x : (WithVal (v.valuation K))}
    (γ : ((WithZero (Multiplicative ℤ)))ˣ) (hx : Valued.v x ≤ 1) :
    ∃a, Valued.v ((algebraMap A K a) - (x : v.adicCompletion K)) < γ.val

instance

(anonymous instance)

L231 ↗

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · full declaration

instance : Valuation.IsRankOneDiscrete vK where
  exists_generator_lt_one' := by
    have h : (v.valuation K).IsRankOneDiscrete := Valuation.IsRankOneDiscrete.mk' (valuation K v)
    exact ⟨h.generator, by rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq],
      h.generator_lt_one⟩

theorem

closureAlgebraMapIntegers_eq_integers

L238 ↗

IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers

Source context 6 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
open Valuation.IsRankOneDiscrete in

Lean source · statement

theorem closureAlgebraMapIntegers_eq_integers :
    closure (algebraMap A (v.adicCompletion K)).range =
    SetLike.coe (v.adicCompletionIntegers K)

theorem

denseRange_of_integerAlgebraMap

L274 ↗

IsDedekindDomain.HeightOneSpectrum.denseRange_of_integerAlgebraMap

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

theorem denseRange_of_integerAlgebraMap :
    DenseRange (algebraMap A (v.adicCompletionIntegers K))

theorem

exists_adicValued_sub_lt_of_adicCompletionInteger

L288 ↗

IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicCompletionInteger

Source context 6 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
open Valuation.IsRankOneDiscrete in

Lean source · statement

theorem exists_adicValued_sub_lt_of_adicCompletionInteger
    (x : v.adicCompletionIntegers K) (γ : ℤᵐ⁰ˣ) :
    ∃a, Valued.v ((algebraMap A K a) - (x : v.adicCompletion K)) < γ.val

abbrev

completionIdeal

L311 ↗

IsDedekindDomain.HeightOneSpectrum.completionIdeal

Documentation

The maximal ideal of the integral valuation subring of the adic completion.

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

abbrev completionIdeal : Ideal (v.adicCompletionIntegers K)

lemma

mem_completionIdeal_iff

L314 ↗

IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

lemma mem_completionIdeal_iff (x : v.adicCompletionIntegers K) :
    x ∈ completionIdeal K v ↔ Valued.v x.val < 1

lemma

algebraMap_completionIntegers

L318 ↗

IsDedekindDomain.HeightOneSpectrum.algebraMap_completionIntegers

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

lemma algebraMap_completionIntegers (x : A) :
    (algebraMap A (v.adicCompletionIntegers K) x) = (algebraMap A (v.adicCompletion K) x)

instance

(anonymous instance)

L322 ↗

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

instance : (v.completionIdeal K).LiesOver v.asIdeal

def

ResidueFieldToCompletionResidueField

L330 ↗

IsDedekindDomain.HeightOneSpectrum.ResidueFieldToCompletionResidueField

Documentation

The residue-field map induced by the inclusion into the completed integral subring.

Source context 6 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
open IsLocalRing in

Lean source · statement

def ResidueFieldToCompletionResidueField :
    A ⧸ v.asIdeal →+* ResidueField (v.adicCompletionIntegers K)

def

ResidueFieldEquivCompletionResidueField

L336 ↗

IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField

Documentation

The original residue field identified with the residue field of the completion.

Source context 6 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
open IsLocalRing in

Lean source · statement

def ResidueFieldEquivCompletionResidueField :
    A ⧸ v.asIdeal ≃+* ResidueField (v.adicCompletionIntegers K)

theorem

inertiaDeg_asIdeal_completionIdeal

L354 ↗

IsDedekindDomain.HeightOneSpectrum.inertiaDeg_asIdeal_completionIdeal

Source context 6 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
attribute [local instance 9999] Algebra.toModule in

Lean source · statement

theorem inertiaDeg_asIdeal_completionIdeal :
    (v.completionIdeal K).inertiaDeg A = 1

theorem

exists_forall_adicValued_sub_lt

L370 ↗

IsDedekindDomain.HeightOneSpectrum.exists_forall_adicValued_sub_lt

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

theorem exists_forall_adicValued_sub_lt {ι : Type*} (s : Finset ι)
    (e : ι → (WithZero (Multiplicative ℤ))ˣ) (valuation : ι → HeightOneSpectrum A)
    (injective : Function.Injective valuation)
    (x : (i : ι) → (valuation i).adicCompletionIntegers K) :
    ∃ a, ∀ i ∈ s, Valued.v ((algebraMap A K a) - (x i).val) < (e i).val

lemma

eq_mul_nonZeroDivisor_inv_adicCompletionIntegers

L400 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_mul_nonZeroDivisor_inv_adicCompletionIntegers

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

lemma adicCompletion.eq_mul_nonZeroDivisor_inv_adicCompletionIntegers (v : HeightOneSpectrum A)
    (x : v.adicCompletion K) :
    ∃a ∈ nonZeroDivisors A, ∃b ∈ v.adicCompletionIntegers K, x = (algebraMap A K a)⁻¹ • b

lemma

eq_mul_pi_adicCompletionIntegers

L411 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_mul_pi_adicCompletionIntegers

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · full declaration

lemma adicCompletion.eq_mul_pi_adicCompletionIntegers {ι : Type*} [Finite ι]
    (valuation : ι → HeightOneSpectrum A) (x : (i : ι) → (valuation i).adicCompletion K) :
      ∃k : K, ∃y ∈ Set.pi Set.univ (fun (i : ι) ↦ ((valuation i).adicCompletionIntegers K).carrier),
      x = k • y := by
  classical
  let := Fintype.ofFinite ι
  choose f hf using fun (i : ι) =>
    eq_mul_nonZeroDivisor_inv_adicCompletionIntegers K (valuation i) (x i)
  use (algebraMap A K (∏ i : ι, f i))⁻¹, (algebraMap A K (∏ i : ι, f i)) • x
  have hz : ∀ (i : ι), (algebraMap A K) (f i) ≠ 0 := fun i =>
    IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors K (fun _ ↦ id) (hf i).left
  constructor
  · rintro i -
    obtain ⟨b, hb, hx⟩ := (hf i).right
    beta_reduce
    rw [Pi.smul_apply, algebraMap_smul, Subsemiring.coe_carrier_toSubmonoid,
        Subring.coe_toSubsemiring, SetLike.mem_coe, ValuationSubring.mem_toSubring, hx,
        ← Finset.prod_erase_mul _ f (Finset.mem_univ i), mul_smul,
        ← IsScalarTower.smul_assoc (f i), Algebra.smul_def (f i), mul_inv_cancel₀ (hz i), one_smul,
        Algebra.smul_def]
    apply mul_mem (coe_mem_adicCompletionIntegers _ _) hb
  · rw [smul_smul, inv_mul_cancel₀, one_smul]
    simp [Finset.prod_ne_zero_iff, hz]

theorem

exists_uniformizer

L438 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.exists_uniformizer

Source context 7 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
open scoped algebraMap in

Lean source · statement

theorem exists_uniformizer (v : HeightOneSpectrum A) :
    ∃ π : v.adicCompletionIntegers K, Valued.v π.1 = Multiplicative.ofAdd (- 1 : ℤ)

theorem

uniformizer_ne_zero

L446 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformizer_ne_zero

Source context 7 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in

Lean source · statement

theorem uniformizer_ne_zero {v : HeightOneSpectrum A}
    {π : v.adicCompletionIntegers K} (hπ : Valued.v π.1 = Multiplicative.ofAdd (-1 : ℤ)) :
    π ≠ 0

theorem

uniformizer_not_isUnit

L454 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformizer_not_isUnit

Source context 9 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in
open scoped Multiplicative in

Lean source · statement

theorem uniformizer_not_isUnit {π : v.adicCompletionIntegers K}
    (hπ : Valued.v π.1 = Multiplicative.ofAdd (-1 : ℤ)) :
    ¬IsUnit (π : v.adicCompletionIntegers K)

theorem

eq_pow_uniformizer_mul_unit

L466 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.eq_pow_uniformizer_mul_unit

Source context 8 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in

Lean source · statement

theorem eq_pow_uniformizer_mul_unit {x : v.adicCompletionIntegers K} (hx : x ≠ 0)
    {π : v.adicCompletionIntegers K} (hπ : Valued.v π.1 = Multiplicative.ofAdd (-1 : ℤ)) :
    ∃ (n : ℕ) (u : (v.adicCompletionIntegers K)ˣ), x = π ^ n * u

theorem

maximalIdeal_eq_span_uniformizer

L491 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.maximalIdeal_eq_span_uniformizer

Source context 9 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in
open scoped algebraMap in

Lean source · statement

theorem maximalIdeal_eq_span_uniformizer {π : v.adicCompletionIntegers K}
    (hπ : Valued.v π.1 = Multiplicative.ofAdd (-1 : ℤ)) :
    IsLocalRing.maximalIdeal (v.adicCompletionIntegers K) =
      Ideal.span {(π : v.adicCompletionIntegers K)}

instance

(anonymous instance)

L505 ↗

Source context 8 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in

Lean source · full declaration

instance : Ring.DimensionLEOne (v.adicCompletionIntegers K) where
  maximalOfPrime {𝔭} h𝔭_ne_bot h𝔭_prime := by
    let ⟨x, hx⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h𝔭_ne_bot
    let ⟨π, hπ⟩ := exists_uniformizer K v
    obtain ⟨n, ⟨u, rfl⟩⟩ := eq_pow_uniformizer_mul_unit K v hx.2 hπ
    simp only [Units.isUnit, Ideal.mul_unit_mem_iff_mem, ne_eq, mul_eq_zero, pow_eq_zero_iff',
      Units.ne_zero, or_false, not_and, Decidable.not_not] at hx
    by_cases hn : n = 0
    · simp only [hn, pow_zero, ← 𝔭.eq_top_iff_one, implies_true, and_true] at hx
      exact h𝔭_prime.ne_top hx |>.elim
    · rw [h𝔭_prime.pow_mem_iff_mem n (by omega), ← 𝔭.span_singleton_le_iff_mem,
        ← maximalIdeal_eq_span_uniformizer K v hπ] at hx
      exact IsLocalRing.maximalIdeal_le h𝔭_prime.ne_top hx.1

instance

(anonymous instance)

L520 ↗

Source context 9 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in
open scoped algebraMap in

Lean source · statement

instance : IsPrincipalIdealRing (v.adicCompletionIntegers K)

instance

(anonymous instance)

L530 ↗

Source context 8 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in

Lean source · full declaration

instance : IsDiscreteValuationRing (v.adicCompletionIntegers K) where
  not_a_field' := by
    let ⟨π, hπ⟩ := exists_uniformizer K v
    rw [maximalIdeal_eq_span_uniformizer K v hπ]
    intro h
    simp only [Ideal.span_singleton_eq_bot] at h
    exact uniformizer_ne_zero hπ h

instance

(anonymous instance)

L539 ↗

Source context 9 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in
open scoped Valued in

Lean source · statement

instance : IsDiscreteValuationRing (𝒪[v.adicCompletion K])

lemma

mem_completionIdeal_pow

L542 ↗

IsDedekindDomain.HeightOneSpectrum.adicCompletion.mem_completionIdeal_pow

Source context 8 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
namespace adicCompletion
variable {K} in
variable {K} in

Lean source · statement

lemma mem_completionIdeal_pow {n : ℕ} (x : v.adicCompletionIntegers K) :
    x ∈ (v.completionIdeal K) ^ n ↔ Valued.v x.val ≤ ↑(Multiplicative.ofAdd (-(n : ℤ)))

lemma

mem_completionIdeal_iff'

L572 ↗

IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff'

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

lemma mem_completionIdeal_iff' (x : v.adicCompletionIntegers K) :
    x ∈ v.completionIdeal K ↔ Valued.v x.val ≤ ↑(Multiplicative.ofAdd (-(1 : ℤ)))

lemma

completionIdeal_ne_bot

L577 ↗

IsDedekindDomain.HeightOneSpectrum.completionIdeal_ne_bot

Source context 5 commands

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

section
namespace IsDedekindDomain.HeightOneSpectrum
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
open scoped WithZero
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)

Lean source · statement

lemma completionIdeal_ne_bot : completionIdeal K v ≠ ⊥

Module documentation

AdicCompletion

Declarations