ModuleMultiplicativeInducedShapiro.lean
Nyll.GaloisCohomology.ProP.MultiplicativeInducedShapiro
3 declarations indexed from sourceView source ↗ Module documentation
Shapiro for the multiplicative induced local blocks
The concrete equivariant-function module used by the local idele block decomposition has exactly Mathlib's coinduced action after applying Additive. This file supplies the representation isomorphism and hence Shapiro in all degrees, for arbitrary ambient groups and subgroups.
Declarations
ClassFieldTower.Cohomology.multiplicativeInducedRepIsoCoind
DocumentationThe multiplicative equivariant-function induced module used by the local idele blocks is Mathlib's coinduced additive representation.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
noncomputable section
namespace ClassFieldTower.Cohomology
open CyclicCohomology
variable {G : Type} [Group G] (H : Subgroup G)
variable (B : Type) [CommGroup B] [MulDistribMulAction H B]
ClassFieldTower.Cohomology.multiplicativeInducedCohomologyIso
DocumentationShapiro's lemma for the actual multiplicative induced module used in the finite-place idele decomposition, in every cohomological degree.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
noncomputable section
namespace ClassFieldTower.Cohomology
open CyclicCohomology
variable {G : Type} [Group G] (H : Subgroup G)
variable (B : Type) [CommGroup B] [MulDistribMulAction H B]
ClassFieldTower.Cohomology.multiplicativeInducedCohomology_subsingleton
DocumentationVanishing passes from a subgroup representation to its concrete multiplicative induced module via the proved Shapiro isomorphism.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
noncomputable section
namespace ClassFieldTower.Cohomology
open CyclicCohomology
variable {G : Type} [Group G] (H : Subgroup G)
variable (B : Type) [CommGroup B] [MulDistribMulAction H B]