Module

TateComparison.lean

Nyll.GaloisCohomology.Cyclic.TateComparison

3 declarations indexed from sourceView source ↗

Module documentation

Boundary-degree Tate cohomology for finite cyclic groups

This file identifies mathlib's Tate cohomology in degrees 0 and -1 with the standard finite-cyclic short complexes. It adds no alternative cohomology model: both targets are the homology objects already defined by mathlib.

Imports2

Mathlib.RepresentationTheory.Homological.FiniteCyclic
Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Imported by8

def

isoZeroBoundary

L28 ↗

TateCohomology.isoZeroBoundary

Documentation

Degree-zero Tate cohomology is the homology of the standard boundary short complex A --N--> A --d₀₁--> C¹(G, A) for every finite group.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace TateCohomology
universe u

Lean source · statement

def isoZeroBoundary {R G : Type u} [CommRing R] [Group G] [Fintype G]
    (A : Rep R G) :
    tateCohomology A 0 ≅
      (ShortComplex.mk A.norm.toModuleCatHom (groupCohomology.d₀₁ A)
        (Rep.norm_comp_d_eq_zero A)).homology

def

isoFiniteCyclicZero

L53 ↗

TateCohomology.isoFiniteCyclicZero

Documentation

For a finite cyclic group generated by g, degree-zero Tate cohomology is the homology of A --N--> A --(ρ(g) - 1)--> A.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace TateCohomology
universe u

Lean source · statement

def isoFiniteCyclicZero {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    tateCohomology A 0 ≅
      (Rep.FiniteCyclicGroup.normHomCompSub A g).homology

def

isoFiniteCyclicNegOne

L89 ↗

TateCohomology.isoFiniteCyclicNegOne

Documentation

For a finite cyclic group generated by g, degree-minus-one Tate cohomology is the homology of A --(ρ(g) - 1)--> A --N--> A.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace TateCohomology
universe u

Lean source · statement

def isoFiniteCyclicNegOne {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]
    (A : Rep R G) (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    tateCohomology A (-1) ≅
      (Rep.FiniteCyclicGroup.subCompNormHom A g).homology

Module documentation

Boundary-degree Tate cohomology for finite cyclic groups

Declarations

isoZeroBoundary

isoFiniteCyclicZero

isoFiniteCyclicNegOne