Module

SPlaces.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Relative.SPlaces

29 declarations indexed from sourceView source ↗

Module documentation

Finite-place support for relative ideles

This file packages a restricted-product assertion for relative ideles. At every finite place outside a finite set, a relative idele belongs to the actual product of valuation-ring unit groups supplied by the completion decomposition. The resulting supported subgroups are stable under the Galois action and exhaust the full relative idele group.

Imports8

Imported by6

def

relativeIdeleLocalTensorDecompositionSupportedSubgroup

L49 ↗

Documentation

Relative ideles that are integral units in every local tensor factor outside the finite set S.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def relativeIdeleLocalTensorDecompositionSupportedSubgroup
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (RelativeIdeleGroup K L)

theorem

mem_relativeIdeleLocalTensorDecompositionSupportedSubgroup_iff

L63 ↗

Documentation

Membership in the supported relative-idele subgroup is exactly valuation-ring integrality at every finite place outside S.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem mem_relativeIdeleLocalTensorDecompositionSupportedSubgroup_iff
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (z : RelativeIdeleGroup K L) :
    z ∈ relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S ↔
      ∀ w : HeightOneSpectrum (𝓞 K), w ∉ S →
        RelativeLocalTensorDecompositionIntegralUnitAt
          (K := K) (L := L) w
          (RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w z)

theorem

relativeIdeleLocalTensorDecompositionSupportedSubgroup_mono

L79 ↗

Documentation

Enlarging the exceptional set enlarges the supported subgroup.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdeleLocalTensorDecompositionSupportedSubgroup_mono
    {S T : Finset (HeightOneSpectrum (𝓞 K))}
    (hST : S ⊆ T) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S ≤
      relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) T

theorem

relativeIdele_mem_localTensorDecompositionSupportedSubgroup

L94 ↗

Documentation

The explicit coefficient-and-lattice support of a relative idele is an exceptional set witnessing restricted-product integrality.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeIdele_mem_localTensorDecompositionSupportedSubgroup
    (z : RelativeIdeleGroup K L) :
    z ∈ relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L)
        (relativeIdeleLocalTensorDecompositionSupport
          (K := K) (L := L) z)

theorem

iSup_relativeIdeleLocalTensorDecompositionSupportedSubgroup_eq_top

L109 ↗

Documentation

The finite-support subgroups exhaust the complete relative idele group.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem iSup_relativeIdeleLocalTensorDecompositionSupportedSubgroup_eq_top :
    ⨆ S : Finset (HeightOneSpectrum (𝓞 K)),
        relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S =
      (⊤ : Subgroup (RelativeIdeleGroup K L))

abbrev

RelativeFiniteSPlaceFactors

L129 ↗

Documentation

The finite local factors of a relative S-idele: unrestricted tensor units on S, and actual local tensor integral units away from S.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev RelativeFiniteSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))

abbrev

RelativeIdeleSPlaceFactors

L138 ↗

Documentation

The complete local-factor model attached to a finite support.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev RelativeIdeleSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))

abbrev

RelativeIdeleSPlaceLocalTensorDecompositionFactors

L145 ↗

Documentation

The same local-factor model after applying the local tensor decomposition at every finite place.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev RelativeIdeleSPlaceLocalTensorDecompositionFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))

def

relativeIdeleSPlaceFactorsEquivLocalTensorDecomposition

L164 ↗

Documentation

The componentwise local tensor decomposition identifies the finite tensor-unit factors with products of the actual completion unit groups, retaining valuation-ring units away from S.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def
    relativeIdeleSPlaceFactorsEquivLocalTensorDecomposition
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeIdeleSPlaceFactors (K := K) (L := L) S ≃*
      RelativeIdeleSPlaceLocalTensorDecompositionFactors
        (K := K) (L := L) S

theorem

relativeBasisIntegralAt_repr_mem

L185 ↗

Documentation

Membership in the chosen basis lattice is exactly the coefficient integrality needed by the restricted local-product model.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeBasisIntegralAt_repr_mem
    (w : HeightOneSpectrum (𝓞 K))
    (x : w.adicCompletion K ⊗[K] L)
    (hx : RelativeBasisIntegralAt
      (K := K) (L := L) w x)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    (Algebra.TensorProduct.basis
        (w.adicCompletion K)
        (relativeExtensionBasis
          (K := K) (L := L))).repr x i ∈
      w.adicCompletionIntegers K

def

relativeIdeleSupportedComponents

L210 ↗

Documentation

Extract all local factors from an integrally supported relative idele.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

def relativeIdeleSupportedComponents
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S →*
      RelativeIdeleSPlaceFactors (K := K) (L := L) S where
  toFun z :=
    ⟨fun w =>
        RelativeIdeleGroup.infiniteComponent
          (K := K) (L := L) w z,
      ⟨fun w =>
          RelativeIdeleGroup.finiteComponent
            (K := K) (L := L) w.1 z,
        fun w =>
          ⟨RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w.1 z,
            (mem_relativeLocalTensorDecompositionIntegralUnitSubgroup_iff
              (K := K) (L := L) w.1 _).2
              ((mem_relativeIdeleLocalTensorDecompositionSupportedSubgroup_iff
                (K := K) (L := L) S z).1 z.property
                w.1 w.2)⟩⟩⟩
  map_one' := by
    apply Prod.ext
    · funext w
      exact
        map_one
          (RelativeIdeleGroup.infiniteComponent
            (K := K) (L := L) w)
    · apply Prod.ext
      · funext w
        exact
          map_one
            (RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w.1)
      · funext w
        apply Subtype.ext
        exact
          map_one
            (RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w.1)
  map_mul' x y := by
    apply Prod.ext
    · funext w
      exact
        map_mul
          (RelativeIdeleGroup.infiniteComponent
            (K := K) (L := L) w)
          (x : RelativeIdeleGroup K L)
          (y : RelativeIdeleGroup K L)
    · apply Prod.ext
      · funext w
        exact
          map_mul
            (RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w.1)
            (x : RelativeIdeleGroup K L)
            (y : RelativeIdeleGroup K L)
      · funext w
        apply Subtype.ext
        exact
          map_mul
            (RelativeIdeleGroup.finiteComponent
              (K := K) (L := L) w.1)
            (x : RelativeIdeleGroup K L)
            (y : RelativeIdeleGroup K L)

theorem

relativeIdeleSupportedComponents_infinite

L279 ↗

Documentation

The infinite component of the displayed supported-factor map is the original infinite component of the relative idele.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdeleSupportedComponents_infinite
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S)
    (w : InfinitePlace K) :
    (relativeIdeleSupportedComponents
      (K := K) (L := L) S z).1 w =
      RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w z

theorem

relativeIdeleSupportedComponents_inside

L294 ↗

Documentation

At a finite place in S, the displayed supported-factor map is the unrestricted finite component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdeleSupportedComponents_inside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S)
    (w : {w : HeightOneSpectrum (𝓞 K) // w ∈ S}) :
    (relativeIdeleSupportedComponents
      (K := K) (L := L) S z).2.1 w =
      RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w.1 z

theorem

relativeIdeleSupportedComponents_outside_coe

L309 ↗

Documentation

Outside S, coercing the integral factor back to tensor units recovers the original finite component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdeleSupportedComponents_outside_coe
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S)
    (w : {w : HeightOneSpectrum (𝓞 K) // w ∉ S}) :
    ((relativeIdeleSupportedComponents
        (K := K) (L := L) S z).2.2 w :
      (w.1.adicCompletion K ⊗[K] L)ˣ) =
      RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w.1 z

theorem

relativeIdeleSupportedComponents_injective

L323 ↗

Documentation

All local components determine a supported relative idele.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdeleSupportedComponents_injective
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Injective
      (relativeIdeleSupportedComponents
        (K := K) (L := L) S)

def

relativeLocalIdeleDataOfSPlaceFactors

L353 ↗

Documentation

Assemble the complete S-place factor family as restricted local idele data. Away from S and the finite discriminant set, the converse part of the local tensor decomposition supplies the required coefficient integrality.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def relativeLocalIdeleDataOfSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S) :
    RelativeLocalIdeleData (K := K) (L := L)

theorem

relativeLocalIdeleDataOfSPlaceFactors_infinite

L444 ↗

Documentation

The assembled local-idele data has the prescribed infinite component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeLocalIdeleDataOfSPlaceFactors_infinite
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : InfinitePlace K) :
    (relativeLocalIdeleDataOfSPlaceFactors
      (K := K) (L := L) S x).infinite w = x.1 w

theorem

relativeLocalIdeleDataOfSPlaceFactors_finite_inside

L456 ↗

Documentation

At a finite place in S, the assembled local-idele data has the prescribed unrestricted component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeLocalIdeleDataOfSPlaceFactors_finite_inside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∈ S) :
    (relativeLocalIdeleDataOfSPlaceFactors
      (K := K) (L := L) S x).finite w =
        x.2.1 ⟨w, hw⟩

theorem

relativeLocalIdeleDataOfSPlaceFactors_finite_outside

L470 ↗

Documentation

At a finite place outside S, the assembled local-idele data is the coercion of the prescribed integral component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeLocalIdeleDataOfSPlaceFactors_finite_outside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ S) :
    (relativeLocalIdeleDataOfSPlaceFactors
      (K := K) (L := L) S x).finite w =
        (x.2.2 ⟨w, hw⟩ :
          (w.adicCompletion K ⊗[K] L)ˣ)

def

relativeIdeleOfSPlaceFactors

L483 ↗

Documentation

Assemble prescribed local factors into the actual supported relative idele.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def relativeIdeleOfSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S

theorem

relativeIdeleOfSPlaceFactors_infiniteComponent

L507 ↗

Documentation

The relative idele assembled from displayed S-place factors has the prescribed infinite component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeIdeleOfSPlaceFactors_infiniteComponent
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : InfinitePlace K) :
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w
        (relativeIdeleOfSPlaceFactors
          (K := K) (L := L) S x) =
      x.1 w

theorem

relativeIdeleOfSPlaceFactors_finiteComponent_inside

L524 ↗

Documentation

At a finite place in S, the assembled relative idele has the prescribed unrestricted component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeIdeleOfSPlaceFactors_finiteComponent_inside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∈ S) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (relativeIdeleOfSPlaceFactors
          (K := K) (L := L) S x) =
      x.2.1 ⟨w, hw⟩

theorem

relativeIdeleOfSPlaceFactors_finiteComponent_outside

L543 ↗

Documentation

At a finite place outside S, the assembled relative idele has the coercion of the prescribed integral component.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeIdeleOfSPlaceFactors_finiteComponent_outside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : RelativeIdeleSPlaceFactors (K := K) (L := L) S)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ S) :
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (relativeIdeleOfSPlaceFactors
          (K := K) (L := L) S x) =
      (x.2.2 ⟨w, hw⟩ :
        (w.adicCompletion K ⊗[K] L)ˣ)

theorem

relativeIdeleSupportedComponents_surjective

L562 ↗

Documentation

Every complete family of local factors is realized by a supported relative idele.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem relativeIdeleSupportedComponents_surjective
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (relativeIdeleSupportedComponents
        (K := K) (L := L) S)

def

relativeIdeleSupportedEquivSPlaceFactors

L592 ↗

Documentation

The exact relative finite-support decomposition:

I_{L/K}^S is the product of all archimedean tensor-unit factors, the unrestricted finite tensor-unit factors over S, and the genuine valuation-ring unit factors away from S.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def relativeIdeleSupportedEquivSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S ≃*
      RelativeIdeleSPlaceFactors (K := K) (L := L) S

def

relativeIdeleLocalTensorDecompositionSupportedSubgroupAction

L608 ↗

Documentation

The natural Galois action restricts to every finite-support subgroup.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def
    relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) S)

theorem

relativeIdeleLocalTensorDecompositionSupportedSubgroupAction_coe

L667 ↗

Documentation

Coercing the supported-subgroup action to the relative idele group recovers the ambient Galois action.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · full declaration

theorem
    relativeIdeleLocalTensorDecompositionSupportedSubgroupAction_coe
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S) :
    letI :=
      relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
        (K := K) (L := L) S
    ((σ • z :
        relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S) :
      RelativeIdeleGroup K L) =
      letI :=
        relativeIdeleRestrictedMulDistribMulAction
          (K := K) (L := L)
      σ • (z : RelativeIdeleGroup K L) :=
  rfl

def

relativeIdeleSPlaceFactorsAction

L688 ↗

Documentation

Coordinatewise Galois action on the complete local-factor model.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def relativeIdeleSPlaceFactorsAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (RelativeIdeleSPlaceFactors
        (K := K) (L := L) S)

theorem

relativeIdeleSupportedComponents_smul

L750 ↗

Documentation

The complete local-component map is equivariant.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · full declaration

theorem relativeIdeleSupportedComponents_smul
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S) :
    letI :=
      relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
        (K := K) (L := L) S
    letI :=
      relativeIdeleSPlaceFactorsAction
        (K := K) (L := L) S
    relativeIdeleSupportedComponents
        (K := K) (L := L) S (σ • z) =
      σ • relativeIdeleSupportedComponents
        (K := K) (L := L) S z := by
  let :=
    relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
      (K := K) (L := L) S
  let :=
    relativeIdeleSPlaceFactorsAction
      (K := K) (L := L) S
  apply Prod.ext
  · funext w
    let :=
      scalarTensorUnitsAction
        (K := K) (L := L) (A := w.Completion)
    exact
      RelativeIdeleGroup.infiniteComponent_smul
        (K := K) (L := L) w σ z
  · apply Prod.ext
    · funext w
      let :=
        scalarTensorUnitsAction
          (K := K) (L := L)
          (A := w.1.adicCompletion K)
      exact
        RelativeIdeleGroup.finiteComponent_smul
          (K := K) (L := L) w.1 σ z
    · funext w
      apply Subtype.ext
      let :=
        scalarTensorUnitsAction
          (K := K) (L := L)
          (A := w.1.adicCompletion K)
      exact
        RelativeIdeleGroup.finiteComponent_smul
          (K := K) (L := L) w.1 σ z

Module documentation

Finite-place support for relative ideles

Declarations