NYLL
Module

Reassociation.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.Reassociation
9 declarations indexed from sourceView source ↗

Module documentation

Reassociation of supported relative-idele factors

The factor model of a supported relative idele is reassociated into the finite family of unrestricted places and the product of integral factors outside the support. The comparison respects the concrete Galois actions.

Imports4
Imported by2

Declarations

abbrev

RelativeOutsideSPlaceFactors

L40 ↗
Documentation

The product of the actual integral tensor-unit factors outside S.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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 RelativeOutsideSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 K)))
def

relativeOutsideSPlaceFactorsAction

L49 ↗
Documentation

The componentwise Galois action on the integral factors outside S.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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 relativeOutsideSPlaceFactorsAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeOutsideSPlaceFactors
        (K := K) (L := L) S)
def

relativeUnrestrictedProdOutsideAction

L73 ↗
Documentation

The componentwise Galois action on the product of unrestricted and outside-integral local factors.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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 relativeUnrestrictedProdOutsideAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeUnrestrictedSPlaceFactors
          (K := K) (L := L) S ×
        RelativeOutsideSPlaceFactors
          (K := K) (L := L) S)
def

relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside

L90 ↗
Documentation

Reassociate all supported local factors as (unrestricted factors) × (outside integral factors).

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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
    relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RelativeIdeleSPlaceFactors (K := K) (L := L) S ≃*
      RelativeUnrestrictedSPlaceFactors
          (K := K) (L := L) S ×
        RelativeOutsideSPlaceFactors
          (K := K) (L := L) S where
  toFun z :=
    ⟨fun i =>
      match i with
      | Sum.inl w => z.1 w
      | Sum.inr w => z.2.1 w,
      z.2.2⟩
  invFun z :=
    ⟨fun w => z.1 (Sum.inl w),
      ⟨fun w => z.1 (Sum.inr w), z.2⟩⟩
  left_inv _ := rfl
  right_inv z := by
    apply Prod.ext
    · funext i
      cases i <;> rfl
    · rfl
  map_mul' x y := by
    apply Prod.ext
    · funext i
      cases i <;> rfl
    · rfl
theorem

relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside_smul

L122 ↗
Documentation

The reassociation of supported local factors is Galois equivariant.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K L : Type}
    [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
    relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside_smul
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (z : RelativeIdeleSPlaceFactors
      (K := K) (L := L) S) :
    relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside
        (K := K) (L := L) S
        ((relativeIdeleSPlaceFactorsAction
          (K := K) (L := L) S).smul σ z) =
      (relativeUnrestrictedProdOutsideAction
        (K := K) (L := L) S).smul σ
        (relativeIdeleSPlaceFactorsEquivUnrestrictedProdOutside
          (K := K) (L := L) S z)
def

relativeIdeleSupportedEquivUnrestrictedProdOutside

L144 ↗
Documentation

The complete supported relative-idele group, with its restricted-product condition already built into the subtype, is the product of the unrestricted local factors in S and the integral local factors outside S.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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
    relativeIdeleSupportedEquivUnrestrictedProdOutside
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S ≃*
      RelativeUnrestrictedSPlaceFactors
          (K := K) (L := L) S ×
        RelativeOutsideSPlaceFactors
          (K := K) (L := L) S
theorem

relativeIdeleSupportedEquivUnrestrictedProdOutside_smul

L161 ↗
Documentation

The supported relative-idele decomposition is equivariant for the concrete Galois action on every factor.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K L : Type}
    [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
    relativeIdeleSupportedEquivUnrestrictedProdOutside_smul
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L)
    (z : relativeIdeleLocalTensorDecompositionSupportedSubgroup
      (K := K) (L := L) S) :
    relativeIdeleSupportedEquivUnrestrictedProdOutside
        (K := K) (L := L) S
        ((relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
          (K := K) (L := L) S).smul σ z) =
      (relativeUnrestrictedProdOutsideAction
        (K := K) (L := L) S).smul σ
        (relativeIdeleSupportedEquivUnrestrictedProdOutside
          (K := K) (L := L) S z)
def

relativeIdeleSupportedHerbrandH0EquivUnrestrictedProdOutside

L206 ↗
Documentation

Transport of degree-zero Tate cohomology from the actual supported relative ideles to the unrestricted and outside-integral factorization.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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
    relativeIdeleSupportedHerbrandH0EquivUnrestrictedProdOutside
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    letI :=
      relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
        (K := K) (L := L) S
    letI :=
      relativeUnrestrictedProdOutsideAction
        (K := K) (L := L) S
    HerbrandH0 (L ≃ₐ[K] L)
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S) ≃*
      HerbrandH0 (L ≃ₐ[K] L)
        (RelativeUnrestrictedSPlaceFactors
            (K := K) (L := L) S ×
          RelativeOutsideSPlaceFactors
            (K := K) (L := L) S) := by
  letI :=
    relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
      (K := K) (L := L) S
  letI :=
    relativeUnrestrictedProdOutsideAction
      (K := K) (L := L) S
  exact
    herbrandH0EquivariantMulEquiv
      (relativeIdeleSupportedEquivUnrestrictedProdOutside
        (K := K) (L := L) S)
      (relativeIdeleSupportedEquivUnrestrictedProdOutside_smul
        (K := K) (L := L) S)
def

relativeIdeleSupportedHerbrandHMinusOneEquivUnrestrictedProdOutside

L239 ↗
Documentation

Transport of degree-minus-one Tate cohomology from the actual supported relative ideles to the unrestricted and outside-integral factorization.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
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
    relativeIdeleSupportedHerbrandHMinusOneEquivUnrestrictedProdOutside
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (σ : L ≃ₐ[K] L) :
    letI :=
      relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
        (K := K) (L := L) S
    letI :=
      relativeUnrestrictedProdOutsideAction
        (K := K) (L := L) S
    HerbrandHMinusOne (L ≃ₐ[K] L)
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup
          (K := K) (L := L) S) σ ≃*
      HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeUnrestrictedSPlaceFactors
            (K := K) (L := L) S ×
          RelativeOutsideSPlaceFactors
            (K := K) (L := L) S) σ := by
  letI :=
    relativeIdeleLocalTensorDecompositionSupportedSubgroupAction
      (K := K) (L := L) S
  letI :=
    relativeUnrestrictedProdOutsideAction
      (K := K) (L := L) S
  exact
    herbrandHMinusOneEquivariantMulEquiv
      (relativeIdeleSupportedEquivUnrestrictedProdOutside
        (K := K) (L := L) S)
      (relativeIdeleSupportedEquivUnrestrictedProdOutside_smul
        (K := K) (L := L) S) σ

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