NYLL
Module

LocalBlocks.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.LocalBlocks
11 declarations indexed from sourceView source ↗

Module documentation

The local blocks occurring in a relative S-idele

For a finite set S of finite places, the unrestricted factors consist of every infinite place and the finite places in S. This file packages those two kinds of concrete tensor factors into one finite dependent family and identifies it equivariantly with the induced local blocks of the local tensor decomposition.

Imports3
Imported by9

Declarations

def

chosenInfinitePlaceAbove

L40 ↗
Documentation

A fixed infinite place of L above the given infinite place of K.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def chosenInfinitePlaceAbove
    (v : InfinitePlace K) : InfinitePlace L
theorem

chosenInfinitePlaceAbove_comap

L48 ↗
Documentation

The chosen infinite place above v restricts back to v.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem chosenInfinitePlaceAbove_comap
    (v : InfinitePlace K) :
    (chosenInfinitePlaceAbove (L := L) v).comap
        (algebraMap K L) = v
abbrev

RelativeUnrestrictedSPlaceIndex

L57 ↗
Documentation

Infinite places and the selected finite places form the finite unrestricted index family of a relative S-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 LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
abbrev RelativeUnrestrictedSPlaceIndex
    (S : Finset (HeightOneSpectrum (𝓞 K)))
def

relativeUnrestrictedSPlaceDatum

L63 ↗
Documentation

The chosen local-place data at every unrestricted place.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def relativeUnrestrictedSPlaceDatum
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeUnrestrictedSPlaceIndex (K := K) S →
      LocalPlaceDatum K L
  | Sum.inl v =>
      { base := v.1
        base_isNontrivial := v.isNontrivial
        extension :=
          infinitePlaceAbsoluteValueExtension
            v (chosenInfinitePlaceAbove (L := L) v)
            (chosenInfinitePlaceAbove_comap
              (L := L) v) }
  | Sum.inr v =>
      { base := HeightOneSpectrum.adicAbv K v.1
        base_isNontrivial :=
          RayClass.adicAbv_isNontrivial v.1
        extension :=
          chosenFinitePlaceExtension
            (L := L) v.1 }
abbrev

RelativeUnrestrictedSPlaceFactor

L84 ↗
Documentation

The actual tensor-unit type attached to one unrestricted place.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
abbrev RelativeUnrestrictedSPlaceFactor
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeUnrestrictedSPlaceIndex (K := K) S → Type
  | Sum.inl v => (v.Completion ⊗[K] L)ˣ
  | Sum.inr v => (v.1.adicCompletion K ⊗[K] L)ˣ
instance

relativeUnrestrictedSPlaceFactorCommGroup

L91 ↗
Documentation

Each unrestricted local tensor-unit factor is a commutative 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 LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance relativeUnrestrictedSPlaceFactorCommGroup
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (i : RelativeUnrestrictedSPlaceIndex (K := K) S) :
    CommGroup
      (RelativeUnrestrictedSPlaceFactor
        (K := K) (L := L) S i)
abbrev

RelativeUnrestrictedSPlaceFactors

L100 ↗
Documentation

The finite family of actual unrestricted tensor factors.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
abbrev RelativeUnrestrictedSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))
def

relativeUnrestrictedSPlaceFactorsAction

L109 ↗
Documentation

The componentwise scalar-conjugation action on the unrestricted tensor factors.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def relativeUnrestrictedSPlaceFactorsAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeUnrestrictedSPlaceFactors
        (K := K) (L := L) S)
def

relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily

L137 ↗
Documentation

The componentwise local tensor equivalence for every unrestricted place in 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 LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def
    relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeUnrestrictedSPlaceFactors
        (K := K) (L := L) S ≃*
      LocalBlockFamily
        (relativeUnrestrictedSPlaceDatum
          (K := K) (L := L) S)
theorem

relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily_smul

L165 ↗
Documentation

The unrestricted-factor realization is equivariant for the full global Galois action.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem
    relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily_smul
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (z : RelativeUnrestrictedSPlaceFactors
      (K := K) (L := L) S) :
    relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily
        (K := K) (L := L) S
        ((relativeUnrestrictedSPlaceFactorsAction
          (K := K) (L := L) S).smul σ z) =
      (localBlockFamilyAction
          (relativeUnrestrictedSPlaceDatum
            (K := K) (L := L) S)).smul σ
        (relativeUnrestrictedSPlaceFactorsEquivLocalBlockFamily
          (K := K) (L := L) S z)
def

relativeUnrestrictedSPlaceFactorsEquivProd

L239 ↗
Documentation

Reassociate the displayed unrestricted factors of RelativeIdeleSPlaceFactors as the finite dependent family above.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open CyclicCohomology
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def relativeUnrestrictedSPlaceFactorsEquivProd
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeUnrestrictedSPlaceFactors
        (K := K) (L := L) S ≃*
      (∀ v : InfinitePlace K,
          (v.Completion ⊗[K] L)ˣ) ×
        (∀ v :
          {v : HeightOneSpectrum (𝓞 K) // v ∈ S},
          (v.1.adicCompletion K ⊗[K] L)ˣ) where
  toFun z :=
    ⟨fun v => z (Sum.inl v),
      fun v => z (Sum.inr v)⟩
  invFun z
    | Sum.inl v => z.1 v
    | Sum.inr v => z.2 v
  left_inv z := by
    funext i
    cases i <;> rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl

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