Module

FinitePlaces.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormApproximation.FinitePlaces

28 declarations indexed from sourceView source ↗

Module documentation

Weak approximation for actual local norm quotients

For a finite Galois extension L / K and a finite set S of finite places of K, this file chooses an actual extension of every v ∈ S, forms the corresponding algebraic localization L_w / K_v, and transports its local norm subgroup to mathlib's concrete adic completion. These transported norm subgroups are open. Multiplicative weak approximation therefore gives a surjection

Kˣ → ∏ v ∈ S, K_vˣ / N(L_wˣ).

All choices are made from the extension theorem for absolute values; none of the local conclusions is included as input data.

Imports12

Imported by9

def

finitePlaceCompletionBaseMap

L57 ↗

Documentation

The canonical dense embedding used to compare the absolute-value completion at v with the concrete adic completion.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceCompletionBaseMap
    (v : HeightOneSpectrum (𝓞 K)) :
    WithAbs (NumberField.HeightOneSpectrum.adicAbv K v) →+*
      v.adicCompletion K

theorem

finitePlaceCompletionBaseMap_apply

L66 ↗

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionBaseMap_apply
    (v : HeightOneSpectrum (𝓞 K))
    (x : WithAbs
      (NumberField.HeightOneSpectrum.adicAbv K v)) :
    finitePlaceCompletionBaseMap v x =
      FinitePlace.embedding v
        (WithAbs.equiv
          (NumberField.HeightOneSpectrum.adicAbv K v) x)

theorem

finitePlaceCompletionBaseMap_norm

L76 ↗

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionBaseMap_norm
    (v : HeightOneSpectrum (𝓞 K))
    (x : WithAbs
      (NumberField.HeightOneSpectrum.adicAbv K v)) :
    ‖finitePlaceCompletionBaseMap v x‖ = ‖x‖

theorem

finitePlaceCompletionBaseMap_isometry

L86 ↗

Documentation

The base embedding is an isometry.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionBaseMap_isometry
    (v : HeightOneSpectrum (𝓞 K)) :
    Isometry (finitePlaceCompletionBaseMap v)

def

finitePlaceCompletionRingHom

L93 ↗

Documentation

Extension of the base embedding to the absolute-value completion.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceCompletionRingHom
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completion →+*
      v.adicCompletion K

theorem

finitePlaceCompletionRingHom_coe

L102 ↗

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionRingHom_coe
    (v : HeightOneSpectrum (𝓞 K))
    (x : WithAbs
      (NumberField.HeightOneSpectrum.adicAbv K v)) :
    finitePlaceCompletionRingHom v
        (x :
          (NumberField.HeightOneSpectrum.adicAbv K v).Completion) =
      finitePlaceCompletionBaseMap v x

theorem

finitePlaceCompletionRingHom_isometry

L114 ↗

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionRingHom_isometry
    (v : HeightOneSpectrum (𝓞 K)) :
    Isometry (finitePlaceCompletionRingHom v)

theorem

finitePlaceCompletionRingHom_surjective

L121 ↗

Documentation

The completed comparison map is onto the concrete adic completion.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceCompletionRingHom_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    Function.Surjective (finitePlaceCompletionRingHom v)

def

finitePlaceCompletionRingEquiv

L153 ↗

Documentation

The two concrete models of K_v are canonically isomorphic.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceCompletionRingEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completion ≃+*
      v.adicCompletion K

def

finitePlaceCompletionContinuousMulEquiv

L162 ↗

Documentation

The preceding ring equivalence, with its native topologies.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

def finitePlaceCompletionContinuousMulEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completion ≃ₜ*
      v.adicCompletion K where
  __ := (finitePlaceCompletionRingEquiv v).toMulEquiv
  continuous_toFun :=
    (finitePlaceCompletionRingHom_isometry v).continuous
  continuous_invFun :=
    ((finitePlaceCompletionRingHom_isometry v).right_inv
      (finitePlaceCompletionRingEquiv v).right_inv).continuous

def

finitePlaceCompletionUnitsContinuousMulEquiv

L175 ↗

Documentation

The induced topological multiplicative equivalence on unit groups.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceCompletionUnitsContinuousMulEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completionˣ ≃ₜ*
      (v.adicCompletion K)ˣ

def

chosenFinitePlaceExtension

L185 ↗

Documentation

The chosen extension of the v-adic absolute value to L. The embedding is supplied by algebraic closedness of the completion's algebraic closure.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def chosenFinitePlaceExtension
    (v : HeightOneSpectrum (𝓞 K)) :
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L

abbrev

ChosenFinitePlaceLocalizedCompletion

L195 ↗

Documentation

The chosen actual localization L_w above the finite place v.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev ChosenFinitePlaceLocalizedCompletion
    (v : HeightOneSpectrum (𝓞 K))

def

chosenFinitePlaceLocalNormSubgroup

L204 ↗

Documentation

The concrete local norm subgroup at v. It is first formed in the absolute-value completion model and then transported to the adic completion used by the idele library.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def chosenFinitePlaceLocalNormSubgroup
    (v : HeightOneSpectrum (𝓞 K)) :
    Subgroup (v.adicCompletion K)ˣ

theorem

chosenFinitePlaceLocalNormSubgroup_isOpen

L226 ↗

Documentation

The local norm subgroup transported to the actual finite idele coordinate is open.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem chosenFinitePlaceLocalNormSubgroup_isOpen
    (v : HeightOneSpectrum (𝓞 K)) :
    IsOpen
      (chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v :
        Set (v.adicCompletion K)ˣ)

abbrev

ChosenFinitePlaceNormQuotient

L299 ↗

Documentation

The actual local norm quotient in the concrete finite-place completion used by ideles.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev ChosenFinitePlaceNormQuotient
    (v : HeightOneSpectrum (𝓞 K))

def

ChosenFinitePlaceIntrinsicNormQuotient

L307 ↗

Documentation

The same local quotient in the absolute-value completion and LocalizedCompletion model used by local class field theory.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def ChosenFinitePlaceIntrinsicNormQuotient
    (v : HeightOneSpectrum (𝓞 K)) : Type

instance

chosenFinitePlaceIntrinsicNormQuotientCommGroup

L322 ↗

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceIntrinsicNormQuotientCommGroup
    (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup
      (ChosenFinitePlaceIntrinsicNormQuotient
        (K := K) (L := L) v)

def

chosenFinitePlaceNormQuotientEquiv

L333 ↗

Documentation

Comparison between the intrinsic local-class-field norm quotient and the concrete quotient occurring in the finite idele coordinate.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def chosenFinitePlaceNormQuotientEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    ChosenFinitePlaceIntrinsicNormQuotient
        (K := K) (L := L) v ≃*
      ChosenFinitePlaceNormQuotient
        (K := K) (L := L) v

theorem

chosenFinitePlaceNormQuotientEquiv_normClass

L367 ↗

Source context 9 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · full declaration

theorem chosenFinitePlaceNormQuotientEquiv_normClass
    (v : HeightOneSpectrum (𝓞 K))
    (x :
      (NumberField.HeightOneSpectrum.adicAbv K v).Completionˣ) :
    let vK :=
      NumberField.HeightOneSpectrum.adicAbv K v
    let w := chosenFinitePlaceExtension (L := L) v
    let hK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) w.1
    let : SMul K w.1.Completion := hK.toSMul
    let : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    chosenFinitePlaceNormQuotientEquiv
        (K := K) (L := L) v
        (normClass vK.Completion
          (LocalizedCompletion vK w) x) =
      QuotientGroup.mk'
        (chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v)
        (finitePlaceCompletionUnitsContinuousMulEquiv v x) := by
  let vK :=
    NumberField.HeightOneSpectrum.adicAbv K v
  let w := chosenFinitePlaceExtension (L := L) v
  let hK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let : Algebra vK.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vK w.1 w.2
  rfl

def

chosenFinitePlaceNormQuotientFamilyEquiv

L400 ↗

Documentation

Product comparison over a finite set of places.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def chosenFinitePlaceNormQuotientFamilyEquiv
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (∀ v : ↥S,
        ChosenFinitePlaceIntrinsicNormQuotient
          (K := K) (L := L) v.1) ≃*
      (∀ v : ↥S,
        ChosenFinitePlaceNormQuotient
          (K := K) (L := L) v.1)

def

principalLocalNormQuotientMap

L414 ↗

Documentation

The diagonal map from global units to the chosen finite family of actual local norm quotients.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def principalLocalNormQuotientMap
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Kˣ →*
      (∀ v : ↥S,
        ChosenFinitePlaceNormQuotient
          (K := K) (L := L) v.1)

theorem

principalLocalNormQuotientMap_apply

L426 ↗

Source context 9 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem principalLocalNormQuotientMap_apply
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : Kˣ) (v : ↥S) :
    principalLocalNormQuotientMap
        (K := K) (L := L) S x v =
      QuotientGroup.mk'
        (chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v.1)
        ((IdeleGroup.principalIdele K x).2 v.1)

theorem

principalLocalNormQuotientMap_surjective

L440 ↗

Documentation

Actual multiplicative local norm approximation: every prescribed finite family of classes modulo N(L_wˣ) is represented by one global element of Kˣ.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem principalLocalNormQuotientMap_surjective
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (principalLocalNormQuotientMap
        (K := K) (L := L) S)

def

principalIntrinsicLocalNormQuotientMap

L455 ↗

Documentation

The same diagonal approximation map with target written directly as a product of LocalFieldTheory.NormQuotients.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def principalIntrinsicLocalNormQuotientMap
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Kˣ →*
      (∀ v : ↥S,
        ChosenFinitePlaceIntrinsicNormQuotient
          (K := K) (L := L) v.1)

theorem

principalIntrinsicLocalNormQuotientMap_surjective

L467 ↗

Documentation

Surjectivity in the intrinsic NormQuotient model.

Source context 8 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem principalIntrinsicLocalNormQuotientMap_surjective
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (principalIntrinsicLocalNormQuotientMap
        (K := K) (L := L) S)

theorem

mem_ker_principalLocalNormQuotientMap_iff

L488 ↗

Documentation

Kernel membership has the expected simultaneous local-norm description.

Source context 9 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem mem_ker_principalLocalNormQuotientMap_iff
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : Kˣ) :
    x ∈
        (principalLocalNormQuotientMap
          (K := K) (L := L) S).ker ↔
      ∀ v : ↥S,
        (IdeleGroup.principalIdele K x).2 v.1 ∈
          chosenFinitePlaceLocalNormSubgroup
            (K := K) (L := L) v.1

theorem

principalLocalNormQuotientMap_ker

L513 ↗

Documentation

The kernel is the intersection of the pullbacks of the actual local norm subgroups.

Source context 9 commands

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

open scoped NumberField NNReal
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem principalLocalNormQuotientMap_ker
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (principalLocalNormQuotientMap
      (K := K) (L := L) S).ker =
      ⨅ v : ↥S,
        (chosenFinitePlaceLocalNormSubgroup
          (K := K) (L := L) v.1).comap
          ((IdeleGroup.finiteComponent v.1).comp
            (IdeleGroup.principalIdele K))

Module documentation

Weak approximation for actual local norm quotients

Declarations