NYLL
Module

SupportedSPlaceFactorsH2Localization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.SupportedSPlaceFactorsH2Localization
12 declarations indexed from sourceView source ↗

Module documentation

Degree-two localization of supported idele factors

The cohomology class of the S-place factors is determined by its finite coordinates in S when the outside integral blocks and infinite blocks are unramified. This detects classes by actual coordinate maps.

Imports6
Imported by2

Declarations

instance

localizedH2InfiniteAction

L44 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2InfiniteAction
Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
Lean source · statement
instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v)
instance

localizedH2InfiniteProductAction

L48 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2InfiniteProductAction
Source context 15 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
Lean source · statement
instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v)
instance

localizedH2InsideAction

L51 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2InsideAction
Source context 16 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
Lean source · statement
instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v)
instance

localizedH2InsideProductAction

L55 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2InsideProductAction
Source context 17 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
Lean source · statement
instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v)
instance

localizedH2OutsideAction

L58 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2OutsideAction
Source context 18 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
Lean source · statement
instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v)
instance

localizedH2OutsideProductAction

L62 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2OutsideProductAction
Source context 19 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
Lean source · statement
instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v)
def

sPlaceFactorsH2Localization

L67 ↗
ClassFieldTower.Martinet.Shafarevich.sPlaceFactorsH2Localization
Documentation

Evaluate the actual S-place cohomology class in each unrestricted finite tensor block belonging to S.

Source context 20 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
Lean source · full declaration
def sPlaceFactorsH2Localization :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (RelativeIdeleSPlaceFactors (K := K) (L := L) S)) 2 →+
      ∀ v : {v : V // v ∈ S},
        groupCohomology (Rep.ofMulDistribMulAction Gal(L / K) (Ain v)) 2 where
  toFun x := piMultiplicativeH2Evaluation Ain
    (prodMultiplicativeH2Evaluation (∀ v, Ain v) (∀ v, Aout v)
      (prodMultiplicativeH2Evaluation (∀ v, A∞ v)
        ((∀ v, Ain v) × (∀ v, Aout v)) x).2).1
  map_zero' := by
    simp only [map_zero, Prod.fst_zero, Prod.snd_zero]
  map_add' x y := by
    simp only [map_add, Prod.fst_add, Prod.snd_add]
theorem

sPlaceFactorsH2Localization_injective

L84 ↗
ClassFieldTower.Martinet.Shafarevich.sPlaceFactorsH2Localization_injective
Documentation

Outside unramified integral blocks and unramified infinite blocks leave only the S-indexed finite coordinates in degree two.

Source context 21 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
omit [NumberField L] in
Lean source · statement
theorem sPlaceFactorsH2Localization_injective
    (hfin : ∀ v : V, v ∉ S → ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    Function.Injective (sPlaceFactorsH2Localization K L S)
instance

localizedH2IdeleAction

L108 ↗
ClassFieldTower.Martinet.Shafarevich.localizedH2IdeleAction
Source context 20 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
Lean source · statement
instance localizedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)
def

supportedSPlaceCohomologyIso

L112 ↗
ClassFieldTower.Martinet.Shafarevich.supportedSPlaceCohomologyIso
Source context 21 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
local instance localizedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
Lean source · statement
def supportedSPlaceCohomologyIso :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)) 2 ≅
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (RelativeIdeleSPlaceFactors (K := K) (L := L) S)) 2
def

supportedSPlaceH2Localization

L131 ↗
ClassFieldTower.Martinet.Shafarevich.supportedSPlaceH2Localization
Documentation

Localize a supported idele degree-two class at all finite places in S.

Source context 21 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
local instance localizedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
Lean source · statement
def supportedSPlaceH2Localization :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)) 2 →+
      ∀ v : {v : V // v ∈ S},
        groupCohomology (Rep.ofMulDistribMulAction Gal(L / K) (Ain v)) 2
theorem

supportedSPlaceH2Localization_injective

L141 ↗
ClassFieldTower.Martinet.Shafarevich.supportedSPlaceH2Localization_injective
Documentation

The actual supported-idele class is determined by the allowed finite coordinates when all other local blocks are unramified.

Source context 21 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local notation "V" => HeightOneSpectrum (𝓞 K)
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
local notation "A∞" => (fun v : InfinitePlace K ↦ (InfinitePlace.Completion v ⊗[K] L)ˣ)
local notation "Ain" => (fun v : {v : V // v ∈ S} ↦
  (HeightOneSpectrum.adicCompletion K (Subtype.val v) ⊗[K] L)ˣ)
local notation "Aout" => (fun v : {v : V // v ∉ S} ↦
  relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) (Subtype.val v))
local instance localizedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance localizedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance localizedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance localizedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance localizedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance localizedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
local instance localizedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
Lean source · statement
theorem supportedSPlaceH2Localization_injective
    (hfin : ∀ v : V, v ∉ S → ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    Function.Injective (supportedSPlaceH2Localization K L S)

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