feat(RepresentationTheory/Homological/ContCohomology/Sha): define Sha by Whysoserioushah · Pull Request #43529 · leanprover-community/mathlib4

Whysoserioushah · 2026-09-07T11:11:07Z

This PR defines the Tate-Shafarevich group in a general setting as intersections of kernels of the natural map between galois cohomology groups.

co-authored-by: @Multramate

github-actions · 2026-09-07T11:12:16Z

PR summary 7202562696

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RepresentationTheory.Homological.ContCohomology.Sha` (new file)	2371

Declarations diff (regex)

+ mem_tateSha
+ tateSha
+ tateSha_eq_iInf
+ tateSha_eq_ker_pi

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- stale; merge master and push to refresh)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5724928).

+5 new declarations
−0 removed declarations

+ContinuousCohomology.coe_tateSha
+ContinuousCohomology.mem_tateSha
+ContinuousCohomology.tateSha
+ContinuousCohomology.tateSha_eq_iInf
+ContinuousCohomology.tateSha_eq_ker_pi

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5062	1

Current commit 7202562696
Reference commit 38f65a093a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Multramate

Is this in the right file? Maybe we can call the file tateSha.

tb65536 · 2026-09-07T12:47:58Z

Can you add a PR description?

eric-wieser · 2026-09-08T10:23:46Z

Wikipedia says

It is known that the Tate–Shafarevich group is a torsion group

Is this a short proof?

Multramate · 2026-09-08T10:38:15Z

Wikipedia says

It is known that the Tate–Shafarevich group is a torsion group

Is this a short proof?

I think this requires A to be torsion. Then it follows from the fact that if your Galois group is profinite then cohomology is torsion. I don't know if this already exists in mathlib but it might.

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

tb65536 · 2026-09-08T13:07:22Z

Thanks!

maintainer delegate

github-actions · 2026-09-08T13:07:55Z

🚀 Pull request has been placed on the maintainer queue by tb65536.

eric-wieser

bors d+

Didn't I hear that you wanted to add scoped notation here?

mathlib-bors · 2026-09-08T13:12:10Z

✌️ Whysoserioushah can now approve this pull request until 2026-09-22 13:12 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Whysoserioushah · 2026-09-08T14:05:43Z

bors r+

@Multramate

…#43529) This PR defines the Tate-Shafarevich group in a general setting as intersections of kernels of the natural map between galois cohomology groups. co-authored-by: @Multramate Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>

Whysoserioushah · 2026-09-08T14:24:00Z

bors r-

mathlib-bors · 2026-09-08T14:24:05Z

Bors build canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

kbuzzard

(I'm in the middle of a review, here are some preliminary comments)

kbuzzard · 2026-09-08T14:29:08Z

+/-- The Tate-Shafarevich group of a continuous representation. -/
+@[simps!]
+noncomputable def tateSha : AddSubgroup (continuousCohomology n A) :=
+  ⨅ v, (map (Field.absoluteGaloisGroup.map (algebraMap K (f v))) (𝟙 _) n).hom.toAddMonoidHom.ker


This is not what it says in the module docstring, for two technical reasons.

H^1(K,X) means H^1(Gal(K^sep/K),X), not H^1(Gal(K-bar/K),X) (indeed Gal(K-bar/K) makes no sense mathematically)

You claim in the module docstring that Sha is the intersection of the kernels of H^1(K,A(Ksep))->H^1(Kv,A(Kvsep)), but I think that your definition is the intersection of the kernels of H^1(K,A(Ksep))->H^1(Kv,A(Ksep)) (the group changes but not the module). For a general A and K and f I don't see any reason why these should be the same. For an abelian variety over a global field with completions these things are the same but this is a nonobvious result and I don't think that this should be swept under the carpet.

Where did we say K-bar?

Ahh absoluteGaloisGroup is in terms of K-bar, why is it not in terms of K-sep?

OK, so the answer is mathlib's definition is wrong, and it's not our problem :)

Well, these two definitions are the same :)

I'm planning on thinking about this a bit tomorrow morning.

The nonobvious result @kbuzzard mentions is Greenberg approximation I believe? We might have to take in a map A -> A_v instead? Unless we're willing to just modify the docstring to say we only need it when H^1(A) = H^1(A_v).

For (1) we have #19616 to fix the issue, for (2) I agree maybe this is an unfixable issue for abstraction

kbuzzard · 2026-09-08T14:32:23Z

+Here `Kᵥ` is a `K`-algebra for each place `v` in an arbitrary indexing set `V`,
+which induces maps between absolute Galois groups and hence maps between cohomology groups.
+
+When `V` is the set of places of a global field `K`, `A` is the set of rational points of an abelian


This is not correct: A is not the rational points (which typically means K-points), it's the K^sep-points.

Multramate · 2026-09-08T15:17:56Z

On another note, I think we should call this file SelmerSha and add API for Selmer groups in the sense of Rubin.

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

define Sha

15241f2

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Sep 7, 2026

move

26339ba

Whysoserioushah changed the title ~~feat(RepresentationTheory/Continuous/Sha): define Sha~~ feat(RepresentationTheory/Homological/ContCohomology/Sha): define Sha Sep 7, 2026

Multramate approved these changes Sep 7, 2026

View reviewed changes

Whysoserioushah and others added 2 commits September 7, 2026 12:16

mk_all

d67da78

Merge branch 'master' into edison/tateSha

4678786

tb65536 reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

tb65536 reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

tb65536 reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

Whysoserioushah and others added 4 commits September 7, 2026 15:53

push

96d36ac

generalize universe

c77cc72

squeeze line

b6f3b14

Merge branch 'master' into edison/tateSha

6a4416b

eric-wieser reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

eric-wieser reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

eric-wieser reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

Whysoserioushah added 2 commits September 8, 2026 11:17

use notatio

03332c5

remove name

5cf6305

use more notation and add reference

d2f510d

Whysoserioushah and others added 2 commits September 8, 2026 11:41

formatting

5724928

Merge branch 'master' into edison/tateSha

9ee825e

tb65536 reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

tb65536 approved these changes Sep 8, 2026

View reviewed changes

Update Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

83d744f

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 8, 2026

eric-wieser approved these changes Sep 8, 2026

View reviewed changes

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 8, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 8, 2026

eric-wieser reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

Update Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

49dd67c

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Sep 8, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 8, 2026

mathlib-bors Bot removed ready-to-merge This PR has been sent to bors. bors-staging This PR is currently being built by bors on the staging branch. labels Sep 8, 2026

kbuzzard reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

kbuzzard reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

kbuzzard reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

kbuzzard reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

kbuzzard reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean Outdated

Whysoserioushah and others added 5 commits September 9, 2026 10:10

Update Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

05fdefa

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

fix

9e57efc

fix

d13da10

Update Mathlib/RepresentationTheory/Homological/ContCohomology/Sha.lean

a542c77

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

fix name

7202562

Uh oh!

Conversation

Whysoserioushah commented Sep 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7202562696

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- stale; merge master and push to refresh)

Uh oh!

Multramate left a comment

Choose a reason for hiding this comment

Uh oh!

tb65536 commented Sep 7, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Sep 8, 2026

Uh oh!

Multramate commented Sep 8, 2026

Uh oh!

Uh oh!

tb65536 commented Sep 8, 2026

Uh oh!

github-actions Bot commented Sep 8, 2026

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Sep 8, 2026

Uh oh!

Uh oh!

Whysoserioushah commented Sep 8, 2026

Uh oh!

Whysoserioushah commented Sep 8, 2026

Uh oh!

mathlib-bors Bot commented Sep 8, 2026

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Multramate commented Sep 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Whysoserioushah commented Sep 7, 2026 •

edited

Loading

github-actions Bot commented Sep 7, 2026 •

edited

Loading