NYLL
Module

FinitePlaceCompletionInstances.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.IdeleClassPowerLocalUnitQuotient.FinitePlaceCompletionInstances
3 declarations indexed from sourceView source ↗

Module documentation

Canonical structures on finite completions

This module installs the complete discrete valuation, characteristic-zero, and finite residue-field structures used by finite-place class-field arithmetic.

Imports3
Imported by8

Declarations

instance

finitePlaceAdicCompletion_isCompleteDiscrete

L30 ↗
GlobalClassFieldTheory.ClassFieldAxiom.finitePlaceAdicCompletion_isCompleteDiscrete
Documentation

The distinguished valuation on a finite completion of a number field is complete discrete.

Source context 5 commands

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

open scoped NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · full declaration
instance finitePlaceAdicCompletion_isCompleteDiscrete
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
      (Valued.v :
        Valuation (v₀.adicCompletion K)
          (WithZero (Multiplicative ℤ))) where
  isRankOneDiscrete := inferInstance
  isAdicComplete :=
    ValuationTheory.Valuations.rankOneDiscreteValuationSubring_isAdicComplete
instance

finitePlaceAdicCompletion_charZero

L41 ↗
GlobalClassFieldTheory.ClassFieldAxiom.finitePlaceAdicCompletion_charZero
Documentation

A finite completion of a number field has characteristic zero.

Source context 5 commands

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

open scoped NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance finitePlaceAdicCompletion_charZero
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    CharZero (v₀.adicCompletion K)
instance

finitePlaceAdicCompletion_residueFinite

L48 ↗
GlobalClassFieldTheory.ClassFieldAxiom.finitePlaceAdicCompletion_residueFinite
Documentation

The residue field of a finite completion of a number field is finite.

Source context 5 commands

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

open scoped NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance finitePlaceAdicCompletion_residueFinite
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    Finite
      (IsLocalRing.ResidueField
        (Valued.v :
          Valuation (v₀.adicCompletion K)
            (WithZero (Multiplicative ℤ))).valuationSubring)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.