Module

IntegerRingComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.IntegerRingComparison

19 declarations indexed from sourceView source ↗

Module documentation

Integer rings in the two finite-place completion models

This file restricts the canonical equivalences between the absolute-value and adic completion models to their valuation rings. It also identifies the residue field of a rational finite-place completion.

Imports8

Imported by4

def

finitePlaceIntegerToCompletion

L37 ↗

Documentation

Embed global integers into the valuation ring of their finite-place completion.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def finitePlaceIntegerToCompletion
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓞 K) →+* 𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]

theorem

finitePlaceIntegerToCompletion_coe

L58 ↗

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finitePlaceIntegerToCompletion_coe
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) :
    ((finitePlaceIntegerToCompletion v x :
      𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]) :
        ChosenFinitePlaceBaseCompletion (K := K) v) =
      algebraMap K (ChosenFinitePlaceBaseCompletion (K := K) v) (x : K)

theorem

finitePlaceCompletionRingEquiv_toCompletion

L70 ↗

Documentation

The comparison with the adic model takes a global element to its standard finite-place embedding.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finitePlaceCompletionRingEquiv_toCompletion
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (x : K) :
    finitePlaceCompletionRingEquiv v
        (algebraMap K (ChosenFinitePlaceBaseCompletion (K := K) v) x) =
      FinitePlace.embedding v x

def

finitePlaceIdealResidueEquivLocalization

L87 ↗

Documentation

Localizing the ring of integers at a finite prime preserves its residue field. This is the ideal-theoretic end of the finite-completion residue comparison.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def finitePlaceIdealResidueEquivLocalization
    {K : Type*} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓞 K ⧸ v.asIdeal) ≃+*
      IsLocalRing.ResidueField (v.valuationSubringAtPrime K)

def

finitePlaceIdealResidueEquivCompletion

L97 ↗

Documentation

The residue field at a finite prime is canonically the residue field of its normalized absolute-value completion.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def finitePlaceIdealResidueEquivCompletion
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓞 K ⧸ v.asIdeal) ≃+*
      𝓀[ChosenFinitePlaceBaseCompletion (K := K) v]

theorem

finitePlaceIdealResidueEquivCompletion_apply_mk

L146 ↗

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finitePlaceIdealResidueEquivCompletion_apply_mk
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) :
    finitePlaceIdealResidueEquivCompletion v
        (Ideal.Quotient.mk v.asIdeal x) =
      IsLocalRing.residue
        𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]
        (finitePlaceIntegerToCompletion v x)

theorem

finitePlaceCompletion_residueField_card

L160 ↗

Documentation

The finite completion and its defining prime ideal have residue fields of the same cardinality.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finitePlaceCompletion_residueField_card
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    Nat.card 𝓀[ChosenFinitePlaceBaseCompletion (K := K) v] =
      Nat.card (𝓞 K ⧸ v.asIdeal)

theorem

finitePlaceCompletionRingEquiv_mem_integers_iff

L169 ↗

Documentation

The canonical equivalence of completion fields identifies their two valuation rings.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finitePlaceCompletionRingEquiv_mem_integers_iff
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K))
    (x : ChosenFinitePlaceBaseCompletion (K := K) v) :
    finitePlaceCompletionRingEquiv v x ∈
        v.adicCompletionIntegers K ↔
      x ∈ 𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]

def

finitePlaceCompletionIntegerRingEquiv

L195 ↗

Documentation

The canonical equivalence between the valuation ring of the absolute-value completion and mathlib's adic completion integers.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def finitePlaceCompletionIntegerRingEquiv
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    𝒪[ChosenFinitePlaceBaseCompletion (K := K) v] ≃+*
      v.adicCompletionIntegers K

def

chosenFinitePlaceLocalizedIntegerRingEquiv

L210 ↗

Documentation

The canonical equivalence between the valuation ring of the chosen localized completion and the concrete adic completion integers at its centre.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

def chosenFinitePlaceLocalizedIntegerRingEquiv
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    let W :=
      finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v)
    𝒪[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v] ≃+*
      W.adicCompletionIntegers L := by
  let vK := HeightOneSpectrum.adicAbv K v
  let w := chosenFinitePlaceExtension (L := L) v
  let W :=
    finitePlaceExtensionCentre
      (K := K) (L := L) v w
  let E :=
    ChosenFinitePlaceLocalizedCompletion
      (K := K) (L := L) v
  let eField : E ≃+* W.adicCompletion L :=
    (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
        vK (RayClass.adicAbv_isNontrivial v) w).toRingEquiv.trans
      (finitePlaceExtensionAdicCompletionRingEquiv
        (K := K) (L := L) v w)
  exact
    RingEquiv.restrict eField 𝒪[E]
      (W.adicCompletionIntegers L).toSubring (by
        intro x
        symm
        change
          eField x ∈ W.adicCompletionIntegers L ↔
            x ∈ 𝒪[E]
        change
          finitePlaceExtensionAdicCompletionRingEquiv
                (K := K) (L := L) v w
                (AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
                  vK (RayClass.adicAbv_isNontrivial v) w x) ∈
              W.adicCompletionIntegers L ↔
            x ∈ 𝒪[E]
        rw [
          finitePlaceExtensionAdicCompletionRingEquiv_mem_integers_iff,
          mem_absoluteValueCompletionIntegers_iff,
          localizedCompletion_mem_integers_iff_norm_le_one
            vK w
            (HeightOneSpectrum.isNonarchimedean_adicAbv K v) x]
        rfl)

def

standardToChosenLocalizedIntegerRingEquiv

L261 ↗

Documentation

The integer rings of the standard completion at the centre and of the chosen localized completion are canonically equivalent.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

def standardToChosenLocalizedIntegerRingEquiv
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    let W := finitePlaceExtensionCentre
      (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
    𝒪[ChosenFinitePlaceBaseCompletion (K := L) W] ≃+*
      𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v] := by
  let W := finitePlaceExtensionCentre
    (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
  exact (finitePlaceCompletionIntegerRingEquiv W).trans
    (chosenFinitePlaceLocalizedIntegerRingEquiv (K := K) (L := L) v).symm

def

chosenFinitePlaceIntegerToLocalizedCompletion

L278 ↗

Documentation

Embed global integers into the integer ring of the chosen localized completion, through the canonical comparison of completion models.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def chosenFinitePlaceIntegerToLocalizedCompletion
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓞 L) →+*
      𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]

theorem

chosenFinitePlaceIntegerToLocalizedCompletion_coe

L295 ↗

Documentation

On global integers the chosen localized integer-ring map is the standard field embedding into the algebraic localization.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem chosenFinitePlaceIntegerToLocalizedCompletion_coe
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 L) :
    ((chosenFinitePlaceIntegerToLocalizedCompletion
        (K := K) (L := L) v x :
        𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]) :
        ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v) =
      AbsoluteValue.toAlgebraicLocalization
        (HeightOneSpectrum.adicAbv K v)
        (chosenFinitePlaceExtension (L := L) v).1
        (chosenFinitePlaceExtension (L := L) v).2
        (x : L)

theorem

chosenFinitePlaceIntegerToLocalizedCompletion_equivariant

L366 ↗

Documentation

Restriction of a decomposition-group automorphism to global integers commutes with their embedding in the chosen algebraic localization.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

theorem chosenFinitePlaceIntegerToLocalizedCompletion_equivariant
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (σ : HilbertRamification.absoluteValueDecompositionGroup K
      (chosenFinitePlaceExtension (L := L) v).1)
    (x : 𝓞 L) :
    let vK := HeightOneSpectrum.adicAbv K v
    let w := chosenFinitePlaceExtension (L := L) v
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    (HilbertRamification.decompositionGroupEquivAlgebraicLocalizationAut
        vK (RayClass.adicAbv_isNontrivial v) w σ)
        ((chosenFinitePlaceIntegerToLocalizedCompletion
          (K := K) (L := L) v x :
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]) :
          ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v) =
      ((chosenFinitePlaceIntegerToLocalizedCompletion
          (K := K) (L := L) v
          (NumberField.RingOfIntegers.mapAlgEquiv (σ : L ≃ₐ[K] L) x) :
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]) :
          ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v) := by
  let vK := HeightOneSpectrum.adicAbv K v
  let w := chosenFinitePlaceExtension (L := L) v
  rw [chosenFinitePlaceIntegerToLocalizedCompletion_coe,
    chosenFinitePlaceIntegerToLocalizedCompletion_coe]
  change
    (HilbertRamification.decompositionGroupEquivAlgebraicLocalizationAut
        vK (RayClass.adicAbv_isNontrivial v) w σ)
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 (x : L)) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
        ((σ : L ≃ₐ[K] L) (x : L))
  exact
    HilbertRamification.localizationRamificationGroups_decompositionGroupEquiv_toLocalization
      vK (RayClass.adicAbv_isNontrivial v) w σ (x : L)

def

chosenFinitePlaceLocalizedResidueEquiv

L408 ↗

Documentation

The centre ideal and the chosen localized completion have canonically equivalent residue fields. This transfers ideal-theoretic Frobenius conditions to the local field on which the chosen Artin map acts.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

def chosenFinitePlaceLocalizedResidueEquiv
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    let W := finitePlaceExtensionCentre
      (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
    (𝓞 L ⧸ W.asIdeal) ≃+*
      𝓀[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v] := by
  let W := finitePlaceExtensionCentre
    (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
  exact (finitePlaceIdealResidueEquivCompletion W).trans
    (IsLocalRing.ResidueField.mapEquiv
      (standardToChosenLocalizedIntegerRingEquiv (K := K) (L := L) v))

theorem

chosenFinitePlaceLocalizedResidueEquiv_apply_mk

L425 ↗

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

theorem chosenFinitePlaceLocalizedResidueEquiv_apply_mk
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 L) :
    let W := finitePlaceExtensionCentre
      (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
    chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
        (Ideal.Quotient.mk W.asIdeal x) =
      IsLocalRing.residue
        𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]
        (chosenFinitePlaceIntegerToLocalizedCompletion
          (K := K) (L := L) v x) := by
  let W := finitePlaceExtensionCentre
    (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
  let eInteger :
      𝒪[ChosenFinitePlaceBaseCompletion (K := L) W] ≃+*
        𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v] :=
    standardToChosenLocalizedIntegerRingEquiv (K := K) (L := L) v
  have hMap :
      eInteger (finitePlaceIntegerToCompletion W x) =
        chosenFinitePlaceIntegerToLocalizedCompletion
          (K := K) (L := L) v x := by
    rfl
  calc
    chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
        (Ideal.Quotient.mk W.asIdeal x) =
      (IsLocalRing.ResidueField.mapEquiv eInteger)
        (finitePlaceIdealResidueEquivCompletion W
          (Ideal.Quotient.mk W.asIdeal x)) := by
        rfl
    _ = (IsLocalRing.ResidueField.mapEquiv eInteger)
          (IsLocalRing.residue
            𝒪[ChosenFinitePlaceBaseCompletion (K := L) W]
            (finitePlaceIntegerToCompletion W x)) := by
      exact congrArg (IsLocalRing.ResidueField.mapEquiv eInteger)
        (finitePlaceIdealResidueEquivCompletion_apply_mk W x)
    _ = IsLocalRing.residue
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]
          (eInteger (finitePlaceIntegerToCompletion W x)) := by
      rfl
    _ = IsLocalRing.residue
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]
          (chosenFinitePlaceIntegerToLocalizedCompletion
            (K := K) (L := L) v x) := by
      exact congrArg
        (IsLocalRing.residue
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v]) hMap

theorem

chosenFinitePlaceLocalizedResidueEquiv_equivariant

L477 ↗

Documentation

The chosen comparison from the prime-ideal residue field to the localized completion residue field respects the decomposition-group action.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

theorem chosenFinitePlaceLocalizedResidueEquiv_equivariant
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (σ : HilbertRamification.absoluteValueDecompositionGroup K
      (chosenFinitePlaceExtension (L := L) v).1)
    (x : 𝓞 L) :
    let vK := HeightOneSpectrum.adicAbv K v
    let w := chosenFinitePlaceExtension (L := L) v
    let W := finitePlaceExtensionCentre (K := K) (L := L) v w
    let C := ChosenFinitePlaceBaseCompletion (K := K) v
    let E := ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
        (Ideal.Quotient.mk W.asIdeal
          (NumberField.RingOfIntegers.mapAlgEquiv (σ : L ≃ₐ[K] L) x)) =
      LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure C E
        ((HilbertRamification.decompositionGroupEquivAlgebraicLocalizationAut
          vK (RayClass.adicAbv_isNontrivial v) w) σ)
        (chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
          (Ideal.Quotient.mk W.asIdeal x)) := by
  let vK := HeightOneSpectrum.adicAbv K v
  let w := chosenFinitePlaceExtension (L := L) v
  let W := finitePlaceExtensionCentre (K := K) (L := L) v w
  let C := ChosenFinitePlaceBaseCompletion (K := K) v
  let E := ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v
  let f : E ≃ₐ[C] E :=
    (HilbertRamification.decompositionGroupEquivAlgebraicLocalizationAut
      vK (RayClass.adicAbv_isNontrivial v) w) σ
  let y : 𝒪[E] := chosenFinitePlaceIntegerToLocalizedCompletion
    (K := K) (L := L) v x
  have hInt :
      LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure C E f y =
        chosenFinitePlaceIntegerToLocalizedCompletion (K := K) (L := L) v
          (NumberField.RingOfIntegers.mapAlgEquiv (σ : L ≃ₐ[K] L) x) := by
    apply Subtype.ext
    rw [LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure_apply]
    exact chosenFinitePlaceIntegerToLocalizedCompletion_equivariant
      (K := K) (L := L) v σ x
  calc
    chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
        (Ideal.Quotient.mk W.asIdeal
          (NumberField.RingOfIntegers.mapAlgEquiv (σ : L ≃ₐ[K] L) x)) =
        IsLocalRing.residue 𝒪[E]
          (chosenFinitePlaceIntegerToLocalizedCompletion (K := K) (L := L) v
            (NumberField.RingOfIntegers.mapAlgEquiv (σ : L ≃ₐ[K] L) x)) :=
      chosenFinitePlaceLocalizedResidueEquiv_apply_mk (K := K) (L := L) v _
    _ = IsLocalRing.residue 𝒪[E]
          (LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure C E f y) :=
      congrArg (IsLocalRing.residue 𝒪[E]) hInt.symm
    _ = LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure C E f
          (IsLocalRing.residue 𝒪[E] y) :=
      (LocalFieldTheory.galoisGroupResidueFieldEquivOfIsIntegralClosure_residue
        C E f y).symm
    _ = LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure C E f
          (chosenFinitePlaceLocalizedResidueEquiv (K := K) (L := L) v
            (Ideal.Quotient.mk W.asIdeal x)) := by
      exact congrArg
        (LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure C E f)
        (chosenFinitePlaceLocalizedResidueEquiv_apply_mk
          (K := K) (L := L) v x).symm

theorem

chosenFinitePlaceLocalized_residueField_card

L545 ↗

Documentation

The residue cardinality of the chosen localized extension is the norm of its centre ideal.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

theorem chosenFinitePlaceLocalized_residueField_card
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    let W := finitePlaceExtensionCentre
      (K := K) (L := L) v (chosenFinitePlaceExtension (L := L) v)
    Nat.card 𝓀[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v] =
      Nat.card (𝓞 L ⧸ W.asIdeal) := by
  exact Nat.card_congr (chosenFinitePlaceLocalizedResidueEquiv
    (K := K) (L := L) v).symm.toEquiv

theorem

rationalFinitePlaceCompletion_residueField_card

L560 ↗

Documentation

The residue field of the absolute-value completion at a rational finite place has cardinality equal to the natural prime represented by that place.

Source context 6 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem rationalFinitePlaceCompletion_residueField_card
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Nat.card
        𝓀[ChosenFinitePlaceBaseCompletion (K := ℚ) v] =
      ((Rat.HeightOneSpectrum.primesEquiv
        (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)

Module documentation

Integer rings in the two finite-place completion models

Declarations