NYLL
Module

MultiplicativeProductH2.lean

Nyll.GaloisCohomology.ProP.MultiplicativeProductH2
5 declarations indexed from sourceView source ↗

Module documentation

Degree-two vanishing for products of multiplicative representations

Primitives are selected coordinatewise and assembled into an actual one-cochain. The local vanishing input is supplied by the proved local integer-unit and archimedean block theorems at the idele application.

Imports2
Imported by3

Declarations

theorem

isMulCoboundary₂_of_H2_subsingleton

L28 ↗
ClassFieldTower.Cohomology.isMulCoboundary₂_of_H2_subsingleton
Documentation

Vanishing of degree-two cohomology supplies an actual multiplicative one-cochain primitive.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Cohomology
open groupCohomology
variable {G : Type} [Group G]
Lean source · statement
theorem isMulCoboundary₂_of_H2_subsingleton
    {M : Type} [CommGroup M] [MulDistribMulAction G M]
    [Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G M) 2)]
    (f : G × G → M) (hf : IsMulCocycle₂ f) : IsMulCoboundary₂ f
theorem

H2_subsingleton_of_isMulCoboundary₂

L36 ↗
ClassFieldTower.Cohomology.H2_subsingleton_of_isMulCoboundary₂
Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Cohomology
open groupCohomology
variable {G : Type} [Group G]
Lean source · statement
theorem H2_subsingleton_of_isMulCoboundary₂
    {M : Type} [CommGroup M] [MulDistribMulAction G M]
    (h : ∀ f : G × G → M, IsMulCocycle₂ f → IsMulCoboundary₂ f) :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G M) 2)
instance

(anonymous instance)

L54 ↗
Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Cohomology
open groupCohomology
variable {G : Type} [Group G]
section Pi
variable {ι : Type} (M : ι → Type) [∀ i, CommGroup (M i)]
variable [∀ i, MulDistribMulAction G (M i)]
Lean source · statement
instance : MulDistribMulAction G (∀ i, M i)
theorem

piMultiplicativeH2_subsingleton

L59 ↗
ClassFieldTower.Cohomology.piMultiplicativeH2_subsingleton
Documentation

Coordinatewise primitives prove degree-two vanishing for a dependent product, including an infinite product.

Source context 8 commands

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

noncomputable section
namespace ClassFieldTower.Cohomology
open groupCohomology
variable {G : Type} [Group G]
section Pi
variable {ι : Type} (M : ι → Type) [∀ i, CommGroup (M i)]
variable [∀ i, MulDistribMulAction G (M i)]
local instance : MulDistribMulAction G (∀ i, M i) :=
  CyclicCohomology.piMulDistribMulAction G M
Lean source · statement
theorem piMultiplicativeH2_subsingleton
    [∀ i, Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G (M i)) 2)] :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G (∀ i, M i)) 2)
theorem

prodMultiplicativeH2_subsingleton

L72 ↗
ClassFieldTower.Cohomology.prodMultiplicativeH2_subsingleton
Documentation

Degree-two vanishing is preserved by a binary product.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Cohomology
open groupCohomology
variable {G : Type} [Group G]
Lean source · statement
theorem prodMultiplicativeH2_subsingleton
    (M N : Type) [CommGroup M] [CommGroup N]
    [MulDistribMulAction G M] [MulDistribMulAction G N]
    [Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G M) 2)]
    [Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G N) 2)] :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction G (M × N)) 2)

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