Documentation

AdeleRingLocallyCompact.FromLocalClassFieldTheory.LocalClassFieldTheory

Results imported from LocalClassFieldTheory

This file contains several helper results imported from an older Lean 3 version of LocalClassFieldTheory. Note that many of these results have been generalised to discrete valuation rings in the latest version, but we include them here as specialisations to the v-adic completion of the field of fractions of a Dedekind domain.

Links to precise commits from the old repository are included alongside each result. Results without any links are new.

source
theorem Multiplicative.ofAdd_neg_one_lt_one :
↑(Multiplicative.ofAdd (-1)) < 1

https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/for_mathlib/with_zero.lean#L129

source
def IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (π : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) :
Prop

An element π ∈ v.adicCompletion K is a uniformizer if it has valuation ofAdd(-1).

https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L137

Equations
Instances For
    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) :
    ∃ (π : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer π

    Uniformizers exist in the field completion v.adicCompletion K.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/complete.lean#L95

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.ne_zero_iff_valuation_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) :
    x ≠ 0 ↔ Valued.v x ≠ 0
    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.isUnit_of_valuation_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hx : Valued.v x = 1) :
    IsUnit x
    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.isUniformizer_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer π) :
    π ≠ 0

    A uniformizer is non-zero in Kᵥ.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) :
    ∃ (π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)), IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π

    Uniformizers exist in the ring of v-adic integers.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/complete.lean#L79

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.valuation_eq_one_of_isUnit {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hx : IsUnit x) :
    Valued.v ↑x = 1

    The valuation of a unit is 1.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUnit_of_valuation_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hx : Valued.v ↑x = 1) :
    IsUnit x

    A v-adic integer with valuation 1 is a unit.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUnit_iff_valuation_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) :
    IsUnit x ↔ Valued.v ↑x = 1

    A v-adic integer is a unit if and only if it has valuation 1.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L97

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.not_isUnit_iff_valuation_lt_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) :
    ¬IsUnit x ↔ Valued.v ↑x < 1

    A v-adic integer is not a unit if and only if it has valuation < 1.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L116

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) :
    π ≠ 0

    A uniformizer is non-zero in Oᵥ.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L178

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_ne_zero' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) :
    ↑π ≠ 0

    A uniformizer is non-zero inside Kᵥ.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L185

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_not_isUnit {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) :
    ¬IsUnit π

    A uniformizer is not a unit in the v-adic integers.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L191

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.eq_pow_uniformizer_mul_unit {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hx : ↑x ≠ 0) (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) :
    ∃ (n : ℕ) (u : (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))ˣ), x = π ^ n * ↑u

    Any v-adic integer can be written as a unit multiplied by a power of a uniformizer.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L259

    source
    theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_is_generator {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) :
    Valued.maximalIdeal (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) = Ideal.span {π}

    A uniformizer generates the maximal ideal of the v-adic integers.

    https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/discrete_valuation_ring/basic.lean#L295

    source
    instance IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField_finite {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} :
    Finite (Valued.ResidueField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

    The residue field of the v-adic integers is finite.

    Equations
    • ⋯ = ⋯