Module

CompletionTransport.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.OutsideIntegralInduced.CompletionTransport

3 declarations indexed from sourceView source ↗

Module documentation

Transporting integer rings across finite-place cosets

This file transports completion fields and their valuation rings from every right coset of a decomposition group to the chosen algebraic localization.

Imports2

Imported by7

def

rightCosetCompletionRingEquivLocalized

L42 ↗

Documentation

A completion belonging to a right coset, transported first by Galois conjugation and then into the chosen algebraic localization.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section CompletionTransport
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)

Lean source · full declaration

def rightCosetCompletionRingEquivLocalized
    (q : InducedRightCosets (absoluteValueDecompositionGroup K w.1)) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    (rightCosetExtensionEquiv vK hvK w q).1.Completion ≃+*
      LocalizedCompletion vK w := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  change
    (absoluteValueExtensionConjugate
      vK w (Quotient.out q)).1.Completion ≃+*
      LocalizedCompletion vK w
  exact
    (conjugateExtensionCompletionRingEquiv
      vK w (Quotient.out q)).trans
      (localizedCompletionEquivCompletion vK hvK w).symm.toRingEquiv

theorem

rightCosetCompletionRingEquivLocalized_norm_eq

L63 ↗

Documentation

The right-coset transport is an isometry for the inherited norms.

Source context 11 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section CompletionTransport
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
omit [NumberField K] [NumberField L] in

Lean source · full declaration

theorem rightCosetCompletionRingEquivLocalized_norm_eq
    (q : InducedRightCosets (absoluteValueDecompositionGroup K w.1))
    (x : (absoluteValueExtensionConjugate
      vK w (Quotient.out q)).1.Completion) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    ‖rightCosetCompletionRingEquivLocalized vK hvK w q x‖ =
      ‖x‖ := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let z :=
    conjugateExtensionCompletionRingEquiv
      vK w (Quotient.out q) x
  have hcoe :
      (((localizedCompletionEquivCompletion vK hvK w).symm z :
          LocalizedCompletion vK w) : w.1.Completion) = z := by
    have h :=
      localizedCompletionEquivCompletion_coe
        vK hvK w
          ((localizedCompletionEquivCompletion vK hvK w).symm z)
    rw [AlgEquiv.apply_symm_apply] at h
    exact h.symm
  change
    ‖(((localizedCompletionEquivCompletion vK hvK w).symm z :
        LocalizedCompletion vK w) : w.1.Completion)‖ = ‖x‖
  rw [hcoe]
  exact
    conjugateExtensionCompletionRingEquiv_norm_eq
      vK w (Quotient.out q) x

def

rightCosetCompletionIntegersRingEquivLocalized

L96 ↗

Documentation

The same transport restricted to the two valuation integer rings.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section CompletionTransport
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)

Lean source · full declaration

def rightCosetCompletionIntegersRingEquivLocalized
    (hvKna : IsNonarchimedean (vK : K → ℝ))
    (q : InducedRightCosets (absoluteValueDecompositionGroup K w.1)) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
      localizedCompletionFinitePlaceValued vK w hvKna
    letI : ValuativeRel (LocalizedCompletion vK w) :=
      localizedCompletionFinitePlaceValuativeRel vK w hvKna
    (absoluteValueCompletionIntegers
      (absoluteValueExtensionConjugate
        vK w (Quotient.out q)).1
      (absoluteValueExtension_isNonarchimedean
        vK hvKna
        (absoluteValueExtensionConjugate
          vK w (Quotient.out q)))) ≃+*
      𝒪[LocalizedCompletion vK w] := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
    localizedCompletionFinitePlaceValued vK w hvKna
  letI : ValuativeRel (LocalizedCompletion vK w) :=
    localizedCompletionFinitePlaceValuativeRel vK w hvKna
  let e :
      (absoluteValueExtensionConjugate
        vK w (Quotient.out q)).1.Completion ≃+*
        LocalizedCompletion vK w :=
    rightCosetCompletionRingEquivLocalized vK hvK w q
  refine e.restrict _ _ ?_
  intro x
  rw [mem_absoluteValueCompletionIntegers_iff,
    localizedCompletion_mem_integers_iff_norm_le_one]
  have hnorm :=
    rightCosetCompletionRingEquivLocalized_norm_eq
      vK hvK w q x
  change ‖e x‖ = ‖x‖ at hnorm
  rw [hnorm]

Module documentation

Transporting integer rings across finite-place cosets

Declarations

rightCosetCompletionRingEquivLocalized

rightCosetCompletionRingEquivLocalized_norm_eq

rightCosetCompletionIntegersRingEquivLocalized