Module

CanonicalExtension.lean

Nyll.ClassFieldTheory.LocalFieldTheory.Padic.Cyclotomic.Unramified.CanonicalExtension

32 declarations indexed from sourceView source ↗

Module documentation

The canonical valuation on the unramified extension of `ℚ_p`

The unramified cyclotomic construction is proved for the additive exponential valuation. This file identifies that presentation, for ℚ_[p], with the concrete complete-DVF valuation used by the local class field theory files. It also specializes the least-exponent degree formula to roots of unity of order p ^ f - 1.

The canonical exponential valuation on `ℚ_p`

Residue field and the `p ^ f - 1` cyclotomic degree

The actual finite-extension valuation and unramified conclusion

Imports19

Imported by5

theorem

prime_coprime_pow_sub_one

L45 ↗

AlgebraicNumberTheory.Valuations.prime_coprime_pow_sub_one

Documentation

A prime is coprime to one less than a positive power of itself.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem prime_coprime_pow_sub_one (p f : ℕ) [hp : Fact p.Prime]
    (hf : 0 < f) :
    p.Coprime (p ^ f - 1)

theorem

padicCyclotomicUnramifiedResidueDegree_prime_pow_sub_one

L61 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree_prime_pow_sub_one

Documentation

For m = p^f - 1, the least positive exponent with p^d = 1 mod m is exactly f. This is the arithmetic specialization used in the unramified branch of local cyclotomic reciprocity.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramifiedResidueDegree_prime_pow_sub_one
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f) :
    padicCyclotomicUnramifiedResidueDegree (p ^ f - 1) p
        (prime_coprime_pow_sub_one p f hf) = f

theorem

padicFieldAbsoluteValue_nonarchimedean

L96 ↗

AlgebraicNumberTheory.Valuations.padicFieldAbsoluteValue_nonarchimedean

Documentation

The norm absolute value on ℚ_p is nonarchimedean in the literal sense used in the unramified-extension construction.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFieldAbsoluteValue_nonarchimedean
    (p : ℕ) [Fact p.Prime] :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (NormedField.toAbsoluteValue ℚ_[p])

theorem

padicFieldAbsoluteValue_complete

L105 ↗

AlgebraicNumberTheory.Valuations.padicFieldAbsoluteValue_complete

Documentation

The norm absolute value on ℚ_p is complete.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFieldAbsoluteValue_complete
    (p : ℕ) [Fact p.Prime] :
    IsCompleteForAbsoluteValue (NormedField.toAbsoluteValue ℚ_[p])

theorem

padicFieldAbsoluteValue_isNontrivial

L127 ↗

AlgebraicNumberTheory.Valuations.padicFieldAbsoluteValue_isNontrivial

Documentation

The norm absolute value on ℚ_p is nontrivial.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFieldAbsoluteValue_isNontrivial
    (p : ℕ) [Fact p.Prime] :
    (NormedField.toAbsoluteValue ℚ_[p]).IsNontrivial

def

padicFieldExponentialValuation

L137 ↗

AlgebraicNumberTheory.Valuations.padicFieldExponentialValuation

Documentation

The canonical additive exponential valuation on ℚ_p, obtained from the standard norm by the conversion v(x) = -log |x|.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicFieldExponentialValuation
    (p : ℕ) [Fact p.Prime] :
    LubinTate.Valuations.ExponentialValuation ℚ_[p]

theorem

padicFieldExponentialValuationSubring_eq_completeDVF

L146 ↗

AlgebraicNumberTheory.Valuations.padicFieldExponentialValuationSubring_eq_completeDVF

Documentation

The valuation ring of the preceding exponential valuation is literally the valuation ring of the concrete complete-DVF package on ℚ_p.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFieldExponentialValuationSubring_eq_completeDVF
    (p : ℕ) [Fact p.Prime] :
    LubinTate.Valuations.exponentialValuationSubringAsValuationSubring
        (padicFieldExponentialValuation p) =
      (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
        padicCompleteDVF p).valuation.valuationSubring

theorem

padicCyclotomicUnramified_padicExponentialValuation_henselian

L204 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicExponentialValuation_henselian

Documentation

The concrete complete ℚ_p valuation is Henselian, expressed through the exponential valuation required by the unramified cyclotomic construction.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padicExponentialValuation_henselian
    (p : ℕ) [Fact p.Prime] :
    ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring
        (padicFieldExponentialValuation p)).valuation

def

padicCyclotomicUnramified_padicExponentialResidueFieldEquivZMod

L230 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicExponentialResidueFieldEquivZMod

Documentation

The residue field of the exponential valuation on ℚ_p is canonically ZMod p. The construction passes through the same valuation-subring equivalence used by the concrete complete-DVF package.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicCyclotomicUnramified_padicExponentialResidueFieldEquivZMod
    (p : ℕ) [Fact p.Prime] :
    padicCyclotomicUnramifiedResidueField
        (padicFieldExponentialValuation p) ≃+* ZMod p

theorem

padicCyclotomicUnramified_padicExponentialResidueField_card

L259 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicExponentialResidueField_card

Documentation

The residue field used by the unramified cyclotomic theorem has cardinality p.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padicExponentialResidueField_card
    (p : ℕ) [Fact p.Prime]
    [Fintype (padicCyclotomicUnramifiedResidueField
      (padicFieldExponentialValuation p))] :
    Fintype.card (padicCyclotomicUnramifiedResidueField
      (padicFieldExponentialValuation p)) = p

theorem

padicCyclotomic_finrank_prime_pow_sub_one

L276 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomic_finrank_prime_pow_sub_one

Documentation

the unramified cyclotomic theorem on the canonical ℚ_p valuation, specialized to the unramified cyclotomic level of order p ^ f - 1: a field generated by a primitive root of that exact order has degree f.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomic_finrank_prime_pow_sub_one
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    Module.finrank ℚ_[p] L = f

def

padicFiniteExtensionAbsoluteValue

L304 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionAbsoluteValue

Documentation

The unique nonarchimedean absolute value on a finite extension of ℚ_p, constructed by the norm formula in the norm-formula theorem.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicFiniteExtensionAbsoluteValue
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] :
    AbsoluteValue L ℝ

theorem

padicFiniteExtensionAbsoluteValue_nonarchimedean

L323 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionAbsoluteValue_nonarchimedean

Documentation

The norm-formula absolute value is nonarchimedean.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionAbsoluteValue_nonarchimedean
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (padicFiniteExtensionAbsoluteValue p L)

theorem

padicFiniteExtensionAbsoluteValue_extends

L342 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionAbsoluteValue_extends

Documentation

The norm-formula absolute value extends the standard ℚ_p absolute value exactly.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionAbsoluteValue_extends
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    (x : ℚ_[p]) :
    padicFiniteExtensionAbsoluteValue p L
        (algebraMap ℚ_[p] L x) =
      NormedField.toAbsoluteValue ℚ_[p] x

theorem

padicFiniteExtensionAbsoluteValue_complete

L363 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionAbsoluteValue_complete

Documentation

The canonical norm-formula absolute value on every finite extension of ℚ_p is complete.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionAbsoluteValue_complete
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] :
    IsCompleteForAbsoluteValue
      (padicFiniteExtensionAbsoluteValue p L)

theorem

padicCyclotomicUnramified_padicFiniteExtensionAbsoluteValue_comp_algHom

L384 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicFiniteExtensionAbsoluteValue_comp_algHom

Documentation

The canonical norm-formula absolute values on finite extensions of ℚ_p are functorial for ℚ_p-algebra embeddings. This is the valued-field tower bridge used in the global Kronecker--Weber argument: no compatibility hypothesis has to be carried by the embedding.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padicFiniteExtensionAbsoluteValue_comp_algHom
    (p : ℕ) [Fact p.Prime]
    {E D : Type*} [Field E] [Field D]
    [Algebra ℚ_[p] E] [Algebra ℚ_[p] D]
    [FiniteDimensional ℚ_[p] E] [FiniteDimensional ℚ_[p] D]
    (i : E →ₐ[ℚ_[p]] D) :
    (padicFiniteExtensionAbsoluteValue p D).comp
        (f := i.toRingHom) i.injective =
      padicFiniteExtensionAbsoluteValue p E

theorem

padicFiniteExtensionAbsoluteValue_algHom

L425 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionAbsoluteValue_algHom

Documentation

Pointwise form of padicCyclotomicUnramified_padicFiniteExtensionAbsoluteValue_comp_algHom.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionAbsoluteValue_algHom
    (p : ℕ) [Fact p.Prime]
    {E D : Type*} [Field E] [Field D]
    [Algebra ℚ_[p] E] [Algebra ℚ_[p] D]
    [FiniteDimensional ℚ_[p] E] [FiniteDimensional ℚ_[p] D]
    (i : E →ₐ[ℚ_[p]] D) (x : E) :
    padicFiniteExtensionAbsoluteValue p D (i x) =
      padicFiniteExtensionAbsoluteValue p E x

theorem

padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_comap_algHom

L440 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_comap_algHom

Documentation

Pulling the canonical valuation ring of a finite ℚ_p-extension back along a ℚ_p-algebra embedding gives the canonical valuation ring of the source. This is the valuation-subring form of the preceding functoriality theorem, suitable for inertia maps.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_comap_algHom
    (p : ℕ) [Fact p.Prime]
    {E D : Type*} [Field E] [Field D]
    [Algebra ℚ_[p] E] [Algebra ℚ_[p] D]
    [FiniteDimensional ℚ_[p] E] [FiniteDimensional ℚ_[p] D]
    (i : E →ₐ[ℚ_[p]] D) :
    (absoluteValueUnitBallSubring
        (padicFiniteExtensionAbsoluteValue p D)
        (padicFiniteExtensionAbsoluteValue_nonarchimedean p D)).comap
          i.toRingHom =
      absoluteValueUnitBallSubring
        (padicFiniteExtensionAbsoluteValue p E)
        (padicFiniteExtensionAbsoluteValue_nonarchimedean p E)

def

padicFiniteExtensionExponentialValuation

L472 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionExponentialValuation

Documentation

The preceding absolute value in the additive exponential presentation used by the unramified cyclotomic theorem.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicFiniteExtensionExponentialValuation
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] :
    LubinTate.Valuations.ExponentialValuation L

theorem

padicFiniteExtensionExponentialValuation_extends

L482 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionExponentialValuation_extends

Documentation

The finite-extension exponential valuation restricts exactly to the canonical exponential valuation of ℚ_p.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionExponentialValuation_extends
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    (x : ℚ_[p]) :
    padicFiniteExtensionExponentialValuation p L
        (algebraMap ℚ_[p] L x) =
      padicFieldExponentialValuation p x

theorem

padicFiniteExtensionExponentialValuation_algHom

L498 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionExponentialValuation_algHom

Documentation

The canonical exponential valuations on finite extensions of ℚ_p are functorial under ℚ_p-algebra embeddings.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionExponentialValuation_algHom
    (p : ℕ) [Fact p.Prime]
    {E D : Type} [Field E] [Field D]
    [Algebra ℚ_[p] E] [Algebra ℚ_[p] D]
    [FiniteDimensional ℚ_[p] E] [FiniteDimensional ℚ_[p] D]
    (i : E →ₐ[ℚ_[p]] D) (x : E) :
    padicFiniteExtensionExponentialValuation p D (i x) =
      padicFiniteExtensionExponentialValuation p E x

theorem

padicFiniteExtension_exponentialRamificationIndex_le_of_algHom

L519 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtension_exponentialRamificationIndex_le_of_algHom

Documentation

Ramification index is monotone under an embedding of finite extensions of ℚ_p. The larger field's canonical valuation pulls back exactly to the smaller field's canonical valuation, and multiplicativity in the resulting valued-field tower gives the inequality.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtension_exponentialRamificationIndex_le_of_algHom
    (p : ℕ) [Fact p.Prime]
    {E D : Type} [Field E] [Field D]
    [Algebra ℚ_[p] E] [Algebra ℚ_[p] D]
    [FiniteDimensional ℚ_[p] E] [FiniteDimensional ℚ_[p] D]
    (i : E →ₐ[ℚ_[p]] D) :
    exponentialRamificationIndex
        (padicFieldExponentialValuation p)
        (padicFiniteExtensionExponentialValuation p E) ≤
      exponentialRamificationIndex
        (padicFieldExponentialValuation p)
        (padicFiniteExtensionExponentialValuation p D)

theorem

padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_eq_integralClosure

L540 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_eq_integralClosure

Documentation

The valuation ring selected by the norm-formula extension is the actual integral closure of the standard complete-DVF valuation ring of ℚ_p. This is the ring-level uniqueness bridge between the exponential valuation and the canonical finite-extension construction.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padicFiniteExtensionValuationSubring_eq_integralClosure
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] :
    (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring
        (padicFiniteExtensionExponentialValuation p L)).toSubring =
      (integralClosure
        (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring
        L).toSubring

theorem

padicCyclotomicUnramified_valuationSubring_eq_integralClosure

L560 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_valuationSubring_eq_integralClosure

Documentation

An integral-closure valuation ring is equal, as a subring of the field, to the usual integralClosure subring.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_valuationSubring_eq_integralClosure
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [IsIntegralClosure W V L] :
    W.toSubring = (integralClosure V L).toSubring

def

padicCyclotomicUnramified_padicExponentialValuationSubringEquivCompleteDVF

L577 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicExponentialValuationSubringEquivCompleteDVF

Documentation

Identity-on-elements equivalence between the exponential valuation ring of ℚ_p and the standard complete-DVF valuation ring.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicCyclotomicUnramified_padicExponentialValuationSubringEquivCompleteDVF
    (p : ℕ) [Fact p.Prime] :
    LubinTate.Valuations.exponentialValuationSubring
        (padicFieldExponentialValuation p) ≃+*
      (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
        padicCompleteDVF p).valuationSubring

def

padicCyclotomicUnramified_padicFiniteExtensionValuationSubringEquiv

L606 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padicFiniteExtensionValuationSubringEquiv

Documentation

If a complete-DVF target is the actual integral closure, its valuation ring is identity-equivalent to the norm-formula valuation ring.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

def padicCyclotomicUnramified_padicFiniteExtensionValuationSubringEquiv
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    (target : ValuationTheory.DiscreteValuationField.CompleteDVF L)
    [IsIntegralClosure target.valuationSubring
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring L] :
    LubinTate.Valuations.exponentialValuationSubring
        (padicFiniteExtensionExponentialValuation p L) ≃+*
      target.valuationSubring

theorem

padicFiniteExtensionExponentialValuationSubring_eq_completeDVF

L654 ↗

AlgebraicNumberTheory.Valuations.padicFiniteExtensionExponentialValuationSubring_eq_completeDVF

Documentation

The norm-formula valuation ring on a finite extension of ℚ_p is the valuation ring of any complete-DVF model given by the integral closure.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicFiniteExtensionExponentialValuationSubring_eq_completeDVF
    (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    (target : ValuationTheory.DiscreteValuationField.CompleteDVF L)
    [IsIntegralClosure target.valuationSubring
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring L] :
    LubinTate.Valuations.exponentialValuationSubringAsValuationSubring
        (padicFiniteExtensionExponentialValuation p L) =
      target.valuation.valuationSubring

theorem

padicCyclotomic_finiteUnramified_of_coprime

L675 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomic_finiteUnramified_of_coprime

Documentation

the unramified cyclotomic theorem(i), specialized to the actual ℚ_p valuation: adjoining roots of unity of any order prime to p is unramified in the degree/residue-degree sense.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomic_finiteUnramified_of_coprime
    (p r : ℕ) [hp : Fact p.Prime] (hpr : p.Coprime r)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ r)
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    FiniteUnramifiedExtension
      (padicFieldExponentialValuation p)
      (padicFiniteExtensionExponentialValuation p L)
      (padicFiniteExtensionExponentialValuation_extends p L)

theorem

padicCyclotomicUnramified_padic_finiteUnramified_prime_pow_sub_one

L699 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padic_finiteUnramified_prime_pow_sub_one

Documentation

The p ^ f - 1 form of padicCyclotomic_finiteUnramified_of_coprime.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padic_finiteUnramified_prime_pow_sub_one
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    FiniteUnramifiedExtension
      (padicFieldExponentialValuation p)
      (padicFiniteExtensionExponentialValuation p L)
      (padicFiniteExtensionExponentialValuation_extends p L)

theorem

padicCyclotomic_ramificationIndex_eq_one_prime_pow_sub_one

L714 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomic_ramificationIndex_eq_one_prime_pow_sub_one

Documentation

The canonical ramification index of the integral-closure complete-DVF extension is one. This is the valuation-ring form of the unramified conclusion, independent of the chosen valuation presentation.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomic_ramificationIndex_eq_one_prime_pow_sub_one
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤)
    (target : ValuationTheory.DiscreteValuationField.CompleteDVF L)
    [hExt :
      (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
        padicCompleteDVF p).valuation.HasExtension
        target.valuation]
    [IsIntegralClosure target.valuationSubring
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).toDVF
      target.toDVF = 1

theorem

padicCyclotomicUnramified_padic_isFiniteUnramified_prime_pow_sub_one

L832 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_padic_isFiniteUnramified_prime_pow_sub_one

Documentation

Complete-DVF form of the unramified cyclotomic theorem(i): the canonical integral-closure extension is finite unramified.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · statement

theorem padicCyclotomicUnramified_padic_isFiniteUnramified_prime_pow_sub_one
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤)
    (target : ValuationTheory.DiscreteValuationField.CompleteDVF L)
    [hExt :
      (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
        padicCompleteDVF p).valuation.HasExtension
        target.valuation]
    [IsIntegralClosure target.valuationSubring
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsFiniteUnramified
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).toDVF
      target.toDVF

theorem

exists_padicCyclotomic_completeDVF_isFiniteUnramified_degree_eq

L879 ↗

AlgebraicNumberTheory.Valuations.exists_padicCyclotomic_completeDVF_isFiniteUnramified_degree_eq

Documentation

Canonical unramified cyclotomic endpoint over ℚ_p: the actual integral closure supplies a complete-DVF extension which is finite unramified and has degree exactly f.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped WithZero

Lean source · full declaration

theorem exists_padicCyclotomic_completeDVF_isFiniteUnramified_degree_eq
    (p f : ℕ) [hp : Fact p.Prime] (hf : 0 < f)
    {L : Type*} [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L]
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
    (hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    ∃ target : ValuationTheory.DiscreteValuationField.CompleteDVF.{_, 0} L,
      ∃ hExt :
        (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
          padicCompleteDVF p).valuation.HasExtension
          target.valuation,
        letI :
          (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
            padicCompleteDVF p).valuation.HasExtension
            target.valuation := hExt
        IsIntegralClosure target.valuationSubring
            (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
              padicCompleteDVF p).valuationSubring L ∧
          ValuationTheory.DiscreteValuationField.ValuedExtension.IsFiniteUnramified
              (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).toDVF
              target.toDVF ∧
            ValuationTheory.DiscreteValuationField.ValuedExtension.degree
              (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).toDVF
              target.toDVF = f := by
  let : Algebra.IsSeparable ℚ_[p] L := by infer_instance
  let base := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p
  obtain ⟨target, hExt, hTarget, _hfundamental⟩ :=
    (open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension in
      exists_integralClosure_standard_fundamental_identity
        (K := ℚ_[p]) (L := L) base)
  let : base.valuation.HasExtension target.valuation := hExt
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L := hTarget
  refine ⟨target, hExt, hTarget, ?_, ?_⟩
  · exact padicCyclotomicUnramified_padic_isFiniteUnramified_prime_pow_sub_one
      p f hf hζ hζgen target
  · exact
      (ValuationTheory.DiscreteValuationField.ValuedExtension.degree_eq_finrank
        base.toDVF target.toDVF).trans
        (padicCyclotomic_finrank_prime_pow_sub_one
          p f hf hζ hζgen)

Module documentation

The canonical valuation on the unramified extension of ℚ_p

The canonical exponential valuation on ℚ_p

Residue field and the p ^ f - 1 cyclotomic degree

The actual finite-extension valuation and unramified conclusion

Declarations

The canonical valuation on the unramified extension of `ℚ_p`

The canonical exponential valuation on `ℚ_p`

Residue field and the `p ^ f - 1` cyclotomic degree