NormKernelVanishing.lean

A specified generator supplies the IsCyclic instance used throughout the cyclic cohomology constructions.

If the abstract field L extends K, this is exactly G_L regarded as a subgroup of G_K. The standard Subgroup.subgroupOf construction is the canonical representation; the containment proof only changes the subtype membership proof and therefore cannot create a second subgroup representation.

The actual coefficient module A_L for an abstract Galois extension L | K: restrict the global representation to G_K, take G_L-fixed vectors, and descend the action to G_K / G_L.

The subgroup occurring in the quotient is G_L viewed inside G_K.

Continuity of the action on the coefficient module when its carrier has the discrete topology, exactly as in this construction's definition of a continuous G-module.

the cyclic norm-kernel vanishing condition. The condition on a continuous G-module used by the construction: H⁻¹(G(L | K), A_L) is trivial for every finite cyclic abstract extension L | K.

Profinite-ness of G and continuity of A are ambient hypotheses in the construction, not parts of the cyclic norm-kernel vanishing condition itself. This predicate therefore records only the numbered vanishing condition. hLK expresses G_L ≤ G_K, hnormal that the extension is Galois, hfinite that it is finite, and g, hg that its Galois group is cyclic.

the finite-cyclic cohomology calculation. If G is finite cyclic, then H¹(G,A) ≅ H⁻¹(G,A).

The right-hand side is the actual homology object ker(N_G) / im(ρ(g) - 1), not a compatibility placeholder.

Elementwise content of the vanishing condition in the cyclic norm-kernel vanishing condition: every norm-zero element is in the image of ρ(g) - 1. This is the source used in the cyclic step of abstract Kummer theory; the conclusion is extracted from the actual homology object rather than assumed separately.