Commit 2026-06-09 15:16 23b0068d

View on Github →

feat(RepresentationTheory/Homological): define Tate cohomology (#38553) co-authored-by : class field theory team

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean

added theorem groupCohomology.map_cochainsFunctor_eval_shortExact

added theorem groupCohomology.δ_naturality

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean

added theorem groupHomology.map_chainsFunctor_eval_shortExact

Created Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean

added theorem Rep.comp_eq_zero

added theorem Rep.d_comp_tateNorm

added theorem Rep.norm_comp_d_eq_zero

added def Rep.tateNorm

added theorem Rep.tateNorm_comp_d

added theorem Rep.tateNorm_eq

added theorem TateCohomology.exact₁

added theorem TateCohomology.exact₃

added def TateCohomology.isoGroupCohomology

added def TateCohomology.isoGroupHomology

added theorem TateCohomology.map_tateComplexFunctor_shortExact

added theorem TateCohomology.map_δ

added def TateCohomology.tateComplex.evalNeg

added def TateCohomology.tateComplex.evalNonneg

added theorem TateCohomology.δ_map

added theorem TateCohomology.δ_naturality

added def tateCohomologyFunctor

added def tateComplex.map

added theorem tateComplex.map_add

added theorem tateComplex.map_zero

added def tateComplexConnectData

added def tateComplexFunctor

added theorem tateComplex_d_neg

added theorem tateComplex_d_neg_one

added theorem tateComplex_d_ofNat