Module

H2FiniteIndexTrace.lean

Nyll.GaloisCohomology.GroupTheory.H2FiniteIndexTrace

6 declarations indexed from sourceView source ↗

Module documentation

Subgroup index annihilates H² when restricted H² vanishes

The coefficient trace is the existing finite-index coinduction-induction isomorphism followed by the induction counit. Its composite with the coinduction unit is the index. Shapiro then supplies the vanishing intermediate cohomology object.

Imports7

Mathlib.RepresentationTheory.FiniteIndex
Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.GroupTheory.Coset.Card
Mathlib.GroupTheory.Sylow
Mathlib.GroupTheory.OrderOfElement

Imported by2

def

finiteIndexCoefficientTrace

L33 ↗

ClassFieldTower.Cohomology.finiteIndexCoefficientTrace

Documentation

The actual coefficient trace from the coinduced restricted representation.

Source context 5 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]

Lean source · statement

def finiteIndexCoefficientTrace :
    Rep.coind H.subtype (Rep.res H.subtype A) ⟶ A

theorem

inductionCounit_mk

L40 ↗

ClassFieldTower.Cohomology.inductionCounit_mk

Source context 6 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]
omit [H.FiniteIndex] in

Lean source · statement

theorem inductionCounit_mk (g : G) (a : A) :
    ((Rep.indResHomEquiv H.subtype (Rep.res H.subtype A) A).symm (𝟙 _)).hom
      (Representation.IndV.mk H.subtype (Rep.res H.subtype A).ρ g a) =
        A.ρ g⁻¹ a

theorem

coinductionUnit_comp_finiteIndexCoefficientTrace

L55 ↗

ClassFieldTower.Cohomology.coinductionUnit_comp_finiteIndexCoefficientTrace

Documentation

Coinduction followed by the coefficient trace is multiplication by the subgroup index.

Source context 5 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]

Lean source · statement

theorem coinductionUnit_comp_finiteIndexCoefficientTrace :
    Rep.resCoindToHom H.subtype A (Rep.res H.subtype A) (𝟙 _) ≫
      finiteIndexCoefficientTrace A H = H.index • 𝟙 A

theorem

H2_map_nsmul_id

L83 ↗

ClassFieldTower.Cohomology.H2_map_nsmul_id

Source context 5 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]

Lean source · statement

theorem H2_map_nsmul_id (m : ℕ)
    (c : groupCohomology A 2) :
    groupCohomology.map (MonoidHom.id G) (m • 𝟙 A) 2 c = m • c

theorem

index_nsmul_H2_eq_zero_of_restricted_isZero

L96 ↗

ClassFieldTower.Cohomology.index_nsmul_H2_eq_zero_of_restricted_isZero

Documentation

If actual H² on a finite-index subgroup vanishes, its index kills every ambient H² class.

Source context 5 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]

Lean source · statement

theorem index_nsmul_H2_eq_zero_of_restricted_isZero
    (hH : Limits.IsZero (groupCohomology (Rep.res H.subtype A) 2))
    (c : groupCohomology A 2) : H.index • c = 0

theorem

H2_eq_zero_of_sylow_restrictions_isZero

L116 ↗

ClassFieldTower.Cohomology.H2_eq_zero_of_sylow_restrictions_isZero

Documentation

Vanishing on every Sylow subgroup detects vanishing of actual H².

Source context 5 commands

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

open CategoryTheory
open scoped BigOperators
namespace ClassFieldTower.Cohomology
noncomputable section
variable {R G : Type} [CommRing R] [Group G] (A : Rep R G) (H : Subgroup G) [H.FiniteIndex]

Lean source · statement

theorem H2_eq_zero_of_sylow_restrictions_isZero [Finite G]
    (h : ∀ (p : ℕ) [Fact p.Prime] (P : Sylow p G),
      Limits.IsZero (groupCohomology (Rep.res (P : Subgroup G).subtype A) 2))
    (c : groupCohomology A 2) : c = 0

Module documentation

Subgroup index annihilates H² when restricted H² vanishes

Declarations

finiteIndexCoefficientTrace

inductionCounit_mk

coinductionUnit_comp_finiteIndexCoefficientTrace

H2_map_nsmul_id

index_nsmul_H2_eq_zero_of_restricted_isZero

H2_eq_zero_of_sylow_restrictions_isZero