A function $\alpha \colon G \to A$ is a crossed homomorphism (1-cocycle) iff it satisfies the
cocycle identity $\alpha(\tau\sigma) = \alpha(\tau) + \tau \cdot \alpha(\sigma)$, identified here
with groupCohomology.IsCocycle₁.
Instances For
A bundled crossed homomorphism: a function $G \to A$ together with a proof of the cocycle condition.
- toFun : G → A
- cocycle_condition : IsCrossedHom self.toFun
Instances For
A CrossedHom G A can be coerced to a function $G \to A$ in a FunLike manner.
Crossed homomorphisms are determined by their function values: two crossed homs agreeing pointwise are equal.
The coercion of a constructed CrossedHom.mk f hf to a function is f itself.
The cocycle condition rewritten in the convenient form $\alpha(\tau\sigma) = \alpha(\tau) + \tau \cdot \alpha(\sigma)$.
A bundled crossed hom is a crossed hom (as a predicate on its underlying function).
The zero crossed homomorphism $\alpha \equiv 0$.
Instances For
Pointwise addition of two crossed homomorphisms is again a crossed homomorphism.
Instances For
Pointwise negation of a crossed homomorphism is again a crossed homomorphism.
Instances For
The zero element of CrossedHom G A.
Pointwise addition on CrossedHom G A.
Pointwise negation on CrossedHom G A.
The zero crossed hom evaluates to $0$ at every $g \in G$.
Sum of two crossed homs evaluates pointwise.
Negation of a crossed hom evaluates pointwise.
Crossed homomorphisms form an additive commutative group under pointwise operations.
A continuous crossed homomorphism: a crossed hom whose underlying function is continuous.
- toFun : G → A
- cocycle_condition : IsCrossedHom self.toFun
- continuous_toFun : Continuous self.toFun
Instances For
A ContCrossedHom G A can be coerced to a function $G \to A$.
Continuous crossed homs are determined by their pointwise values.
Coercion of a constructed ContCrossedHom.mk f hf returns f.
Restated cocycle identity for continuous crossed homs: $\alpha(\tau\sigma) = \alpha(\tau) + \tau \cdot \alpha(\sigma)$.
The underlying function of a continuous crossed hom is continuous.
Underlying crossed-hom property of a continuous crossed hom.
Restatement of the cocycle condition in Mathlib's IsCocycle₁ form.
The zero continuous crossed homomorphism $\alpha \equiv 0$, which is continuous as a constant function.
Instances For
Pointwise sum of two continuous crossed homomorphisms is again continuous.
Instances For
Pointwise negation of a continuous crossed homomorphism is continuous.
Instances For
Zero on ContCrossedHom.
Pointwise addition on ContCrossedHom.
Pointwise negation on ContCrossedHom.
The zero continuous crossed hom evaluates to $0$ everywhere.
Sum of two continuous crossed homs evaluates pointwise.
Negation of a continuous crossed hom evaluates pointwise.
Continuous crossed homomorphisms form an additive commutative group.
A function $\alpha \colon G \to A$ is a principal crossed homomorphism (1-coboundary) iff it has the form $\alpha(\sigma) = \sigma \cdot P - P$ for some $P \in A$.
Instances For
Unfolding: $\alpha$ is a coboundary iff there exists $P \in A$ with $\sigma \cdot P - P = \alpha(\sigma)$ for all $\sigma$.
Every principal (1-coboundary) crossed homomorphism is itself a crossed homomorphism (1-cocycle).
The principal crossed hom $\sigma \mapsto \sigma \cdot P - P$ associated to a point $P \in A$.
Instances For
The principal crossed hom at $P$ evaluates as $\sigma \mapsto \sigma \cdot P - P$.
The subgroup of principal crossed homomorphisms (1-coboundaries) inside the additive group of all crossed homomorphisms.
Instances For
Membership criterion for the subgroup of principal crossed homomorphisms.
The principal continuous crossed hom $\sigma \mapsto \sigma \cdot P - P$ associated to
$P \in A$, viewed as a ContCrossedHom.
Instances For
Evaluation formula for the continuous principal crossed hom at $P$.
The subgroup of continuous principal crossed homomorphisms inside ContCrossedHom G A.
Instances For
Membership criterion for the subgroup of continuous principal crossed homomorphisms.
The first (continuous) Galois cohomology group: $H^1(G, A) := Z^1 / B^1$ where $Z^1$ is the group of continuous crossed homs and $B^1$ the subgroup of principal ones.
Instances For
The canonical projection $\mathrm{ContCrossedHom}(G, A) \to H^1(G, A)$.
Instances For
Equality criterion in $H^1$: $[\alpha] = [\beta]$ iff $\alpha - \beta$ is a principal crossed homomorphism.
The absolute Galois group $\mathrm{Gal}(\bar k/k)$ of a field $k$, realized as $k$-algebra automorphisms of an algebraic closure of $k$.
Instances For
The Krull topology on the absolute Galois group: open subgroups are stabilizers of finite extensions.
The points of an elliptic curve over the algebraic closure $\bar k$: $E(\bar k)$.
Instances For
The group structure on $E(\bar k)$ coming from the Weierstrass curve's affine point group law.
The Galois group $\mathrm{Gal}(\bar k/k)$ acts on $E(\bar k)$ by transporting points along each $k$-algebra automorphism of $\bar k$.
Instances For
Promote the Galois DistribMulAction on $E(\bar k)$ to an instance.
We endow $E(\bar k)$ with the discrete topology, which is appropriate for the topology on the cocycle group.
Confirmation that the topology on $E(\bar k)$ chosen above is the discrete topology.
Addition on $E(\bar k)$ is continuous (vacuously, since the topology is discrete).
Negation on $E(\bar k)$ is continuous (vacuously, in the discrete topology).
The Galois action on $E(\bar k)$ is continuous (in the Krull topology on $\mathrm{Gal}(\bar k/k)$ and the discrete topology on $E(\bar k)$): the stabilizer of every point is open, since it contains the open subgroup fixing a finite subextension containing the coordinates of $P$.
Instances For
Promote galoisContinuousSMul to an instance.
The realisation of the Weil-Châtelet group via Galois cohomology: $H^1(\mathrm{Gal}(\bar k/k), E(\bar k))$.