Data witnessing the bijection between the Weil-Châtelet set of $E$-torsors over $k$ (mod
$k$-isomorphism) and the first cohomology group $H^1(G, E_{\mathrm{pts}})$: a well-defined,
injective, and surjective cocycleMap.
- cocycleMap : ETorsor k W E_pts → GaloisCohomology.H1 G E_pts
- cocycleMap_wellDefined (T₁ T₂ : ETorsor k W E_pts) : T₁.Equiv T₂ → self.cocycleMap T₁ = self.cocycleMap T₂
- cocycleMap_injective (T₁ T₂ : ETorsor k W E_pts) : self.cocycleMap T₁ = self.cocycleMap T₂ → T₁.Equiv T₂
- cocycleMap_surjective : Function.Surjective self.cocycleMap
Instances For
Data of a Galois action on a torsor T: a Galois map $\sigma \mapsto \sigma_C$ acting on
points of T, equivariant with the $E$-action and a group homomorphism in $\sigma$, together
with a continuity condition.
- cont (Q₀ : T.C_pts) : Continuous fun (σ : G) => self.σ_C σ Q₀ -ᵥ Q₀
Instances For
The canonical cocycle attached to a torsor T: deferred to a sorry; it should produce a
continuous crossed homomorphism $G \to E_{\mathrm{pts}}$ from the Galois action on T.
Instances For
Galois descent (surjectivity onto cocycles): every continuous crossed homomorphism $\alpha \colon G \to E_{\mathrm{pts}}$ arises as the canonical cocycle of some $E$-torsor over $k$.
Existence of a Galois action on any torsor T: explicit construction via twisting by the
canonical cocycle at a chosen base point.
Instances For
Restatement of the group-action axiom for GaloisActionOnTorsor: $\sigma_C(\tau\sigma) = \sigma_C(\tau) \circ \sigma_C(\sigma)$.
For any base point $Q_0 \in C_T$, the function $\sigma \mapsto \sigma_C(Q_0) -_v Q_0$ is a crossed homomorphism $G \to E_{\mathrm{pts}}$.
The construction of the cocycle map at the level of $E$-torsors: given a torsor $T$, choose a base point, take the Galois-action cocycle $\sigma \mapsto \sigma_C(Q_0) -_v Q_0$, and pass to its class in $H^1$.
Instances For
Restated compatibility: a $k$-isomorphism $e$ between torsors that intertwines the $E$-actions also intertwines the Galois actions, when this is given as a hypothesis.
A $k$-isomorphism between torsors is automatically Galois-equivariant: the proof is deferred.
The cocycle map is well-defined on equivalence classes of $E$-torsors: equivalent torsors produce cohomologous cocycles, hence equal classes in $H^1$.
The cocycle map is injective on torsor equivalence classes: torsors that map to the same class in $H^1$ are equivalent (as $k$-isomorphic torsors).
For any continuous crossed homomorphism $\alpha$, there is a torsor $T$ and a point $Q_0 \in C_T$ such that the Galois action on $T$ realises $\alpha$ as $\sigma \mapsto \sigma_C(Q_0) -_v Q_0$.
For each continuous crossed homomorphism $\alpha$, there is an $E$-torsor $T$ whose image
under cocycleMap_construction is the class of $\alpha$ in $H^1$.
The cocycle map $\mathrm{ETorsor}(k, W, E) \to H^1(G, E_{\mathrm{pts}})$ is surjective.
Bundled WCH1Data: the cocycle map together with its well-definedness, injectivity, and
surjectivity proofs.
Instances For
The Weil-Châtelet set is in bijection with $H^1(G, E_{\mathrm{pts}})$: existence of a bijection $\mathrm{WC}(E/k) \simeq H^1$.
Explicit bijection $\mathrm{WC}(E/k) \simeq H^1(G, E_{\mathrm{pts}})$ given a choice of
WCH1Data.
Instances For
Transport the abelian group structure on $H^1$ to WC via the bijection of
wc_h1_setEquiv, making WC k W E_pts into an AddCommGroup.
Instances For
The Weil-Châtelet group is isomorphic, as an additive group, to $H^1(G, E_{\mathrm{pts}})$,
once we transport the group structure via the bijection of wc_h1_setEquiv.
Instances For
Corollary 26.25: the Weil-Châtelet set $\mathrm{WC}(E/k)$ admits an abelian group structure under which it is isomorphic to $H^1(\mathrm{Gal}(\bar k/k), E(\bar k))$.