Module

MultiplicativeProductH2Evaluation.lean

Nyll.GaloisCohomology.ProP.MultiplicativeProductH2Evaluation

4 declarations indexed from sourceView source ↗

Module documentation

Degree-two cohomology detected by product coordinates

An actual one-cochain primitive in each coordinate combines into a product primitive. Consequently evaluation detects degree-two classes, including for an infinite product of multiplicative coefficient groups.

Imports7

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Product
Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.TateComparison
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.Algebra.Group.TypeTags.Basic

Imported by2

instance

productEvaluationAction

L30 ↗

ClassFieldTower.Cohomology.productEvaluationAction

Source context 5 commands

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

namespace ClassFieldTower.Cohomology
open CategoryTheory groupCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable {G ι : Type} [Group G]
variable (M : ι → Type) [∀ i, CommGroup (M i)] [∀ i, MulDistribMulAction G (M i)]

Lean source · statement

instance productEvaluationAction : MulDistribMulAction G (∀ i, M i)

def

piMultiplicativeEvaluationRepHom

L34 ↗

ClassFieldTower.Cohomology.piMultiplicativeEvaluationRepHom

Documentation

Evaluation at one coordinate as a morphism of the actual representations.

Source context 6 commands

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

namespace ClassFieldTower.Cohomology
open CategoryTheory groupCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable {G ι : Type} [Group G]
variable (M : ι → Type) [∀ i, CommGroup (M i)] [∀ i, MulDistribMulAction G (M i)]
local instance productEvaluationAction : MulDistribMulAction G (∀ i, M i) :=
  CyclicCohomology.piMulDistribMulAction G M

Lean source · statement

def piMultiplicativeEvaluationRepHom (i : ι) :
    Rep.ofMulDistribMulAction G (∀ j, M j) ⟶ Rep.ofMulDistribMulAction G (M i)

def

piMultiplicativeH2Evaluation

L43 ↗

ClassFieldTower.Cohomology.piMultiplicativeH2Evaluation

Documentation

Simultaneous evaluation on degree-two cohomology.

Source context 6 commands

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

namespace ClassFieldTower.Cohomology
open CategoryTheory groupCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable {G ι : Type} [Group G]
variable (M : ι → Type) [∀ i, CommGroup (M i)] [∀ i, MulDistribMulAction G (M i)]
local instance productEvaluationAction : MulDistribMulAction G (∀ i, M i) :=
  CyclicCohomology.piMulDistribMulAction G M

Lean source · full declaration

def piMultiplicativeH2Evaluation :
    groupCohomology (Rep.ofMulDistribMulAction G (∀ i, M i)) 2 →+
      ∀ i, groupCohomology (Rep.ofMulDistribMulAction G (M i)) 2 where
  toFun x i :=
    (groupCohomology.map (A := Rep.ofMulDistribMulAction G (∀ j, M j))
      (B := Rep.ofMulDistribMulAction G (M i))
      (MonoidHom.id G) (piMultiplicativeEvaluationRepHom M i) 2).hom x
  map_zero' := by
    funext i
    exact map_zero (groupCohomology.map
      (A := Rep.ofMulDistribMulAction G (∀ j, M j))
      (B := Rep.ofMulDistribMulAction G (M i))
      (MonoidHom.id G) (piMultiplicativeEvaluationRepHom M i) 2).hom
  map_add' x y := by
    funext i
    exact map_add (groupCohomology.map
      (A := Rep.ofMulDistribMulAction G (∀ j, M j))
      (B := Rep.ofMulDistribMulAction G (M i))
      (MonoidHom.id G) (piMultiplicativeEvaluationRepHom M i) 2).hom x y

theorem

piMultiplicativeH2Evaluation_injective

L64 ↗

ClassFieldTower.Cohomology.piMultiplicativeH2Evaluation_injective

Documentation

Product degree-two classes are determined by all their evaluations.

Source context 6 commands

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

namespace ClassFieldTower.Cohomology
open CategoryTheory groupCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable {G ι : Type} [Group G]
variable (M : ι → Type) [∀ i, CommGroup (M i)] [∀ i, MulDistribMulAction G (M i)]
local instance productEvaluationAction : MulDistribMulAction G (∀ i, M i) :=
  CyclicCohomology.piMulDistribMulAction G M

Lean source · statement

theorem piMultiplicativeH2Evaluation_injective :
    Function.Injective (piMultiplicativeH2Evaluation (G := G) M)

Module documentation

Degree-two cohomology detected by product coordinates

Declarations

productEvaluationAction

piMultiplicativeEvaluationRepHom

piMultiplicativeH2Evaluation

piMultiplicativeH2Evaluation_injective