ModuleMultiplicativeBinaryProductH2Evaluation.lean
Nyll.GaloisCohomology.ProP.MultiplicativeBinaryProductH2Evaluation
4 declarations indexed from sourceView source ↗ Module documentation
Coordinate evaluation of multiplicative H²
Constructs the two coordinate maps for a product of multiplicative representations and proves their combined degree-two evaluation is injective.
Declarations
ClassFieldTower.Cohomology.firstRepHom
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 N : Type) [CommGroup M] [CommGroup N]
variable [MulDistribMulAction G M] [MulDistribMulAction G N]
ClassFieldTower.Cohomology.secondRepHom
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 N : Type) [CommGroup M] [CommGroup N]
variable [MulDistribMulAction G M] [MulDistribMulAction G N]
ClassFieldTower.Cohomology.prodMultiplicativeH2Evaluation
DocumentationThe pair of actual coordinate evaluations 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 N : Type) [CommGroup M] [CommGroup N]
variable [MulDistribMulAction G M] [MulDistribMulAction G N]
ClassFieldTower.Cohomology.prodMultiplicativeH2Evaluation_injective
DocumentationTwo coordinate primitives assemble to a primitive in the product.
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 N : Type) [CommGroup M] [CommGroup N]
variable [MulDistribMulAction G M] [MulDistribMulAction G N]