Sha.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 0 contain sorry, 0 declared as axioms

The Tate–Shafarevich group of a Galois module

This file defines a general notion of a Tate–Shafarevich group of a Galois module (i.e. an abelian group A equipped with a continuous action of the absolute Galois group G_K of a field K), as the intersection of the kernels of the maps Hⁿ(G_K, A) → Hⁿ(G_Kᵥ, A), induced by the map G_Kᵥ → G_K, where Kᵥ is a field extension of K for each v in an arbitrary indexing set V.

These definitions were introduced in Mathlib by Edison Xie and David Kurniadi Angdinata's pull request #43529. They are absent from this repository's Mathlib v4.33.1 dependency. The added code is copied verbatim from Mathlib.RepresentationTheory.Homological.ContCohomology.Sha at commit a4c43ae1f99cb19aabfa62308b3ea75a340e470f, except that Mathlib.FieldTheory.AbsoluteGaloisGroup is replaced by this repository's copy, which supplies Field.absoluteGaloisGroup.map.

Main definitions

ContinuousCohomology.tateShafarevich: the Tate–Shafarevich group of a Galois module.

TODOs

Add a notation for ContinuousCohomology.tateShafarevich.
Prove that ContinuousCohomology.tateShafarevich of a discrete Galois module is torsion.
Define the classical Tate–Shafarevich group in Mathlib/AlgebraicGeometry/EllipticCurve.

Implementation notes

Mathematicians seem to use "Tate–Shafarevich group" in at least three distinct contexts. They have in common the set-up that K is a global field, A is a discrete G_K-module, V is the set of places of K, and Kᵥ is the completion of K at a place v in V.

The first context is when A is finite. This is used, for example, in the statement of global Poitou-Tate duality. In this theorem, the Tate–Shafarevich group is defined exactly as in this file. It agrees with Definition 8.6.2 of [Neukirch–Schmidt–Wingberg].

The second context is when A is the Kˢ-valued points of a group scheme J such as an abelian variety. Then the Tate–Shafarevich group is usually defined as the intersection of the kernels of the maps H¹(G_K, J(Kˢ)) → H¹(G_Kᵥ, J(Kᵥˢ)). Note that in particular the module changes as well as the group, so technically this is not quite what is happening in this definition. However the inclusion H¹(G_Kᵥ, J(Kᵥˢ)) → H¹(G_Kᵥ, J(Kˢ)) is an isomorphism by the Greenberg approximation theorem, so the definition in this file is still mathematically correct. See Remark I.3.10 of [Milne].

The third context is when A is the quotient of a p-adic G_K-module by a G_K-invariant lattice, which is different from the definition in this PR. See Section 1 of [Flach].

References

Imports (3)

Imported by 2 files

def ContinuousCohomology.tateShafarevich The Tate–Shafarevich group of a Galois module line 94 source
Source documentation
The Tate–Shafarevich group of a Galois module.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, TopRep, Int, Field.absoluteGaloisGroup, Nat, AddSubgroup, TopModuleCat.toModuleCat, continuousCohomology
Proof uses: iInf, AddMonoidHom.ker, TopRep.res, ContinuousMonoidHom, Field.absoluteGaloisGroup.map, Algebra.algebraMap, LinearMap.toAddMonoidHom, RingHom.id, TopModuleCat.Hom.hom, ContinuousCohomology.map, CategoryTheory.CategoryStruct.id
46 instances, coercions and auxiliary constants left out.
```
noncomputable def tateShafarevich : AddSubgroup (continuousCohomology n A) :=
…
```
lemma ContinuousCohomology.tateShafarevich_eq_iInf line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, TopRep, Int, Field.absoluteGaloisGroup, Nat, Eq, AddSubgroup, TopModuleCat.toModuleCat, continuousCohomology, ContinuousCohomology.tateShafarevich, iInf, AddMonoidHom.ker, TopRep.res, ContinuousMonoidHom, Field.absoluteGaloisGroup.map, Algebra.algebraMap, LinearMap.toAddMonoidHom, RingHom.id, TopModuleCat.Hom.hom and 2 more
Proof uses: rfl
45 instances, coercions and auxiliary constants left out.
lemma ContinuousCohomology.tateShafarevich_eq_ker_pi line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, TopRep, Int, Field.absoluteGaloisGroup, Nat, Eq, AddSubgroup, TopModuleCat.toModuleCat, continuousCohomology, ContinuousCohomology.tateShafarevich, AddMonoidHom.ker, TopRep.res, ContinuousMonoidHom, Field.absoluteGaloisGroup.map, Algebra.algebraMap, AddMonoidHom.pi, LinearMap.toAddMonoidHom, RingHom.id, TopModuleCat.Hom.hom and 2 more
Proof uses: AddSubgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, ContinuousLinearMap, OfNat.ofNat, True, congr, congrArg, iInf, AddMonoidHom, forall_congr, congrFun', AddMonoidHom.pi_apply, iff_self
74 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ContinuousCohomology.mem_tateShafarevich line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, TopRep, Int, Field.absoluteGaloisGroup, Nat, TopModuleCat.toModuleCat, continuousCohomology, Iff, Membership.mem, AddSubgroup, ContinuousCohomology.tateShafarevich, Eq, TopRep.res, ContinuousMonoidHom, Field.absoluteGaloisGroup.map, Algebra.algebraMap, ContinuousLinearMap, RingHom.id, TopModuleCat.Hom.hom and 3 more
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, iInf, AddMonoidHom.ker, LinearMap.toAddMonoidHom, AddMonoidHom, forall_congr, iff_self
82 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.