Module

ContinuousLowDegreeFiveTermExact.lean

Nyll.GaloisCohomology.ProP.ContinuousLowDegreeFiveTermExact

2 declarations indexed from sourceView source ↗

Module documentation

Continuous low-degree five-term exact sequence

The three kernel--range identities for inflation, restriction, and transgression assemble into the continuous low-degree five-term sequence with trivial ZMod p coefficients.

Imports2

Imported by1

Nyll.GaloisCohomology.ProP.All

instance

continuousFiveTermH1Module

L31 ↗

ClassFieldTower.Cohomology.continuousFiveTermH1Module

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance continuousFiveTermH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))

theorem

continuousLowDegreeFiveTerm_exact

L40 ↗

ClassFieldTower.Cohomology.continuousLowDegreeFiveTerm_exact

Documentation

Exactness at the three middle terms of the continuous low-degree sequence

H¹(G/U) → H¹(G) → H¹(U)ᴳ → H²(G/U) → H²(G).

Source context 9 commands