Module

GaloisCohomology.lean

Nyll.GaloisCohomology.Cyclic.GaloisCohomology

5 declarations indexed from sourceView source ↗

Module documentation

Cyclic Tate low-degree boundary

For a finite cyclic group generated by g, mathlib computes odd group cohomology using Rep.FiniteCyclicGroup.subCompNormHom A g. The canonical boundary comparison identifies that short-complex homology with tateCohomology A (-1).

This file applies that comparison to unit representations. The resulting objects are mathlib's Tate cohomology objects directly; no parallel low-degree model is introduced.

Imports3

Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Nyll.GaloisCohomology.Cyclic.TateComparison

Imported by4

theorem

zpowers_eq_top_of_forall_mem_zpowers

L30 ↗

CyclicCohomology.zpowers_eq_top_of_forall_mem_zpowers

Source context 3 commands

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

namespace CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

theorem zpowers_eq_top_of_forall_mem_zpowers {G : Type} [Group G] (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    Subgroup.zpowers g = ⊤

theorem

isCyclic_of_forall_mem_zpowers

L40 ↗

CyclicCohomology.isCyclic_of_forall_mem_zpowers

Source context 3 commands

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

namespace CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

theorem isCyclic_of_forall_mem_zpowers {G : Type} [Group G] (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    IsCyclic G

def

cyclic_H1_iso_HminusOne

L49 ↗

CyclicCohomology.cyclic_H1_iso_HminusOne

Documentation

Low-degree Tate periodicity in degree one: for a finite cyclic group, H¹(G,A) is canonically isomorphic to mathlib's degree-minus-one Tate cohomology.

Source context 3 commands

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

namespace CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

def cyclic_H1_iso_HminusOne {k G : Type} [CommRing k] [Group G]
    [Fintype G] (A : Rep k G) (g : G)
    (hg : ∀ x : G, x ∈ Subgroup.zpowers g) :
    groupCohomology A 1 ≅ tateCohomology A (-1)

def

unitsH1IsoTateHminusOne

L59 ↗

CyclicCohomology.unitsH1IsoTateHminusOne

Documentation

The cyclic low-degree comparison for the unit representation.

Source context 3 commands

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

namespace CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

def unitsH1IsoTateHminusOne (K L : Type) [Field K] [Field L]
    [Algebra K L] [FiniteDimensional K L] (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    groupCohomology.H1 (Rep.ofAlgebraAutOnUnits K L) ≅
      tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1)

theorem

hilbert90_unitsTateHminusOne_isZero

L69 ↗

CyclicCohomology.hilbert90_unitsTateHminusOne_isZero

Documentation

Hilbert 90 transported through the cyclic H¹ ≅ H^{-1} comparison. This is low-degree cyclic Tate cohomology for the coefficient group Lˣ: the vanishing of H¹(G,Lˣ) gives the vanishing of H^{-1}(G,Lˣ).

Source context 3 commands

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

namespace CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

theorem hilbert90_unitsTateHminusOne_isZero (K L : Type) [Field K]
    [Field L] [Algebra K L] [FiniteDimensional K L] (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    CategoryTheory.Limits.IsZero
      (tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1))

Module documentation

Cyclic Tate low-degree boundary

Declarations

zpowers_eq_top_of_forall_mem_zpowers

isCyclic_of_forall_mem_zpowers

cyclic_H1_iso_HminusOne

unitsH1IsoTateHminusOne

hilbert90_unitsTateHminusOne_isZero