ModuleFiniteTowerBaseUnitsH2.lean
Nyll.GaloisCohomology.Kummer.FiniteTowerBaseUnitsH2
2 declarations indexed from sourceView source ↗ Module documentation
Base-unit coefficients along a field tower
The inclusions Kˣ → Lˣ → Nˣ give an actual equivariant coefficient map for Gal(N/L), starting with the trivial action on Kˣ.
Imports6
- Nyll.GaloisCohomology.Kummer.FiniteCyclicBaseUnitsH2
- Mathlib.Algebra.Category.ModuleCat.Basic
- Mathlib.Algebra.Group.Units.Hom
- Mathlib.Algebra.Module.LinearMap.Defs
- Mathlib.RepresentationTheory.Rep.Basic
- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Imported by4
Declarations
ClassFieldTower.Cohomology.finiteTowerBaseUnitsRepHom
DocumentationInclusion of base units along the two given algebra maps.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L N : Type) [Field K] [Field L] [Field N]
[Algebra K L] [Algebra L N]
ClassFieldTower.Cohomology.finiteTowerBaseUnitsH2Map
DocumentationThe induced degree-two coefficient map for the actual field tower.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (K L N : Type) [Field K] [Field L] [Field N]
[Algebra K L] [Algebra L N]