Module

H2PrimeToIndexRestriction.lean

Nyll.GaloisCohomology.ProP.H2PrimeToIndexRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Prime-to-index injectivity of continuous degree-two restriction

Vanishing on an open finite-index subgroup supplies a continuous lift to the cocycle extension. The difference between this lift and the inclusion gives a coefficient character on the preimage subgroup. Its continuous transfer is multiplication by the index on the central kernel. Inverting that index in ZMod p constructs a global splitting character.

This proves injectivity without a cohomological corestriction package, finite-stage descent, or a normality assumption. The only local instances record local compactness of the closed subgroup and the finite index of its preimage under a surjective projection.

Imports5

Imported by2

instance

h2PrimeIndexCanonicalZModAddCommGroup

L38 ↗

ClassFieldTower.ProP.h2PrimeIndexCanonicalZModAddCommGroup

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

instance h2PrimeIndexCanonicalZModAddCommGroup : AddCommGroup (ZMod p)

theorem

π_eq_zero_of_restriction_of_index_not_dvd

L46 ↗

ClassFieldTower.ProP.H2CocycleExtension.π_eq_zero_of_restriction_of_index_not_dvd

Documentation

A class whose restriction vanishes is zero when the subgroup index is prime to p. The global splitting character is constructed by transferring the difference of two actual lifts, then dividing its central-kernel value by the subgroup index.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance h2PrimeIndexCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G]

Lean source · statement

theorem H2CocycleExtension.π_eq_zero_of_restriction_of_index_not_dvd
    (H : OpenSubgroup G)
    (hindex : ¬ p ∣ H.toSubgroup.index)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (hz : (Cohomology.continuousCohomologyZModPMapLifted p
      (Cohomology.subgroupInclusion H.toSubgroup) 2).hom
      (ContinuousCohomology.π (Cohomology.trivialZModPLifted p G) 2 z) = 0) :
    ContinuousCohomology.π (Cohomology.trivialZModPLifted p G) 2 z = 0

theorem

continuousH2Restriction_injective_of_index_not_dvd

L124 ↗

ClassFieldTower.ProP.continuousH2Restriction_injective_of_index_not_dvd

Documentation

Restriction of continuous trivial-coefficient H² is injective for an open subgroup of index prime to p. Normality is not required.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance h2PrimeIndexCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G]

Lean source · statement

theorem continuousH2Restriction_injective_of_index_not_dvd
    (H : OpenSubgroup G)
    (hindex : ¬ p ∣ H.toSubgroup.index) :
    Function.Injective (Cohomology.continuousCohomologyZModPMapLifted p
      (Cohomology.subgroupInclusion H.toSubgroup) 2).hom

Module documentation

Prime-to-index injectivity of continuous degree-two restriction

Declarations

h2PrimeIndexCanonicalZModAddCommGroup

π_eq_zero_of_restriction_of_index_not_dvd

continuousH2Restriction_injective_of_index_not_dvd