Module

EverywhereUnramifiedSupportedIdeleH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.EverywhereUnramifiedSupportedIdeleH2

10 declarations indexed from sourceView source ↗

Module documentation

H² of the everywhere-integral relative idele subgroup

The finite integral and infinite unrestricted tensor blocks have already been proved to have zero H². Coordinatewise primitives assemble across their products, and the actual equivariant S-place factor decomposition identifies the result with the relative idele subgroup integral at every finite place. No unproved Shapiro or restricted-product glue is assumed.

The six component actions below have pairwise distinct coefficient types: three factor families and their products. The seventh action is the supported-idele subgroup action. Each canonical action is fixed once, with no alternative tower or repeated statement/proof setup.

Imports4

Imported by3

instance

supportedH2InfiniteAction

L49 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2InfiniteAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v)

instance

supportedH2InfiniteProductAction

L53 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2InfiniteProductAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)

Lean source · statement

instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v)

instance

supportedH2InsideAction

L56 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2InsideAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞

Lean source · statement

instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v)

instance

supportedH2InsideProductAction

L60 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2InsideProductAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (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 supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v)

instance

supportedH2OutsideAction

L63 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2OutsideAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain

Lean source · statement

instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v)

instance

supportedH2OutsideProductAction

L67 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2OutsideProductAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1

Lean source · statement

instance supportedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v)

theorem

everywhereUnramifiedEmptySPlaceFactorsH2_subsingleton

L73 ↗

ClassFieldTower.Martinet.Shafarevich.everywhereUnramifiedEmptySPlaceFactorsH2_subsingleton

Documentation

All actual S-place factors for empty finite support have zero H² in an everywhere-unramified extension.

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance supportedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
omit [NumberField L] in

Lean source · statement

theorem everywhereUnramifiedEmptySPlaceFactorsH2_subsingleton
    (hfin : ∀ v : V, ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (RelativeIdeleSPlaceFactors (K := K) (L := L) S)) 2)

instance

supportedH2IdeleAction

L94 ↗

ClassFieldTower.Martinet.Shafarevich.supportedH2IdeleAction

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance supportedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout

Lean source · statement

instance supportedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)

theorem

everywhereUnramifiedSupportedIdeleH2_subsingleton

L100 ↗

ClassFieldTower.Martinet.Shafarevich.everywhereUnramifiedSupportedIdeleH2_subsingleton

Documentation

The subgroup of actual relative ideles integral at every finite place has zero H² in an everywhere-unramified extension.

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance supportedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
local instance supportedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S

Lean source · statement

theorem everywhereUnramifiedSupportedIdeleH2_subsingleton
    (hfin : ∀ v : V, ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)) 2)

theorem

everywhereUnramifiedSupportedIdeleTwoCocycle_isCoboundary

L126 ↗

ClassFieldTower.Martinet.Shafarevich.everywhereUnramifiedSupportedIdeleTwoCocycle_isCoboundary

Documentation

A supported idele two-cocycle has an actual supported idele one-cochain primitive.

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)
local notation "S" => (∅ : Finset V)
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 supportedH2InfiniteAction (v : InfinitePlace K) :
    MulDistribMulAction Gal(L / K) (A∞ v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance supportedH2InfiniteProductAction : MulDistribMulAction Gal(L / K) (∀ v, A∞ v) :=
  piMulDistribMulAction Gal(L / K) A∞
local instance supportedH2InsideAction (v : {v : V // v ∈ S}) :
    MulDistribMulAction Gal(L / K) (Ain v) :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.1.adicCompletion K)
local instance supportedH2InsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Ain v) :=
  piMulDistribMulAction Gal(L / K) Ain
local instance supportedH2OutsideAction (v : {v : V // v ∉ S}) :
    MulDistribMulAction Gal(L / K) (Aout v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v.1
local instance supportedH2OutsideProductAction : MulDistribMulAction Gal(L / K) (∀ v, Aout v) :=
  piMulDistribMulAction Gal(L / K) Aout
local instance supportedH2IdeleAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S

Lean source · statement

theorem everywhereUnramifiedSupportedIdeleTwoCocycle_isCoboundary
    (hfin : ∀ v : V, ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K)
    (f : Gal(L / K) × Gal(L / K) →
      relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)
    (hf : groupCohomology.IsMulCocycle₂ f) : groupCohomology.IsMulCoboundary₂ f

Module documentation

H² of the everywhere-integral relative idele subgroup

Declarations