ModuleH1NormalSubgroupDescent.lean
Nyll.GaloisCohomology.ProP.H1NormalSubgroupDescent
4 declarations indexed from sourceView source ↗ Module documentation
Degree-one descent along a normal subgroup
A one-cocycle that vanishes on a normal subgroup takes values in the subgroup invariants and descends to the quotient. Subtracting a boundary on the normal subgroup gives the degree-one vanishing induction step for arbitrary coefficients. The construction is used to propagate cyclic class-formation vanishing to finite solvable extensions.
Imports3
- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
- Mathlib.RepresentationTheory.Invariants
- Mathlib.GroupTheory.QuotientGroup.Basic
Imported by2
Declarations
ClassFieldTower.Cohomology.h1Cocycle_value_invariant_of_vanishes
DocumentationA one-cocycle vanishing on a normal subgroup has invariant values.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
open groupCohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
variable (A : Rep k G) (N : Subgroup G) [N.Normal]
ClassFieldTower.Cohomology.descendedH1Cocycle
DocumentationDescend a one-cocycle vanishing on a normal subgroup to the quotient, with coefficients in the invariant subrepresentation.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
open groupCohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
variable (A : Rep k G) (N : Subgroup G) [N.Normal]
ClassFieldTower.Cohomology.descendedH1Cocycle_mk
DocumentationThe descended cocycle agrees with the original one on quotient representatives.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
open groupCohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
variable (A : Rep k G) (N : Subgroup G) [N.Normal]
ClassFieldTower.Cohomology.h1_subsingleton_of_normalSubgroup
DocumentationThe normal-subgroup induction step for degree-one vanishing. A primitive on the subgroup is subtracted first; a quotient primitive then completes the primitive on the full group.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
open groupCohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
variable (A : Rep k G) (N : Subgroup G) [N.Normal]