The second cohomology of a cyclic Galois extension

Let L/K be a finite Galois extension whose Galois group is cyclic, generated by g. The cohomology of a finite cyclic group is two-periodic, and in degree 2 it is the quotient of the g-fixed coefficients by the image of the norm (Rep.FiniteCyclicGroup.groupCohomologyπEven). For the coefficients Lˣ the fixed part is Kˣ and the image of the norm is the norm group N_{L/K}(Lˣ), so

H²(Gal(L/K), Lˣ) ≃ Kˣ / N_{L/K}(Lˣ).

This file writes TauCeti.cyclicClass hg a for the class of a ∈ Kˣ under this identification at the generator g. It is represented by the carry cocycle (gⁱ, gʲ) ↦ a if i + j ≥ [L : K] and 1 otherwise, for 0 ≤ i, j < [L : K] (TauCeti.H2π_eq_cyclicClass), so the identification depends on the choice of generator. This explicit representative is what connects the norm quotient to crossed products: classically, the crossed product of the carry cocycle of a is the cyclic algebra (L/K, g, a).

Along a tower K ⊆ L ⊆ M of cyclic Galois extensions whose generators are compatible, inflation sends the class of a to the class of a ^ [M : L] (TauCeti.map_cyclicClass). More generally, for cyclic Galois extensions L/K and M'/K' with K ⊆ K', L ⊆ M' and generators satisfying g'|_L = g ^ d, the map induced by restriction Gal(M'/K') → Gal(L/K) sends the class of a to the class of a ^ (d · [M' : K'] / [L : K]) (TauCeti.map_cyclicClass_baseChange).

Independently of any generator, Hilbert's Theorem 90 makes H¹(Gal(L/K), Lˣ) vanish, so the order of H²(Gal(L/K), Lˣ) is the Herbrand quotient of Lˣ (TauCeti.natCard_H2_units_eq_herbrandQuotient). This is the form in which a computation of that Herbrand quotient, such as h(Lˣ) = [L : K] for local fields, bounds H².

Main definitions

• TauCeti.cyclicClass: the class in H²(Gal(L/K), Lˣ) of an element of Kˣ, by two-periodicity at a generator of Gal(L/K).
• TauCeti.cyclicNormQuotientEquiv: the identification Kˣ / N_{L/K}(Lˣ) ≃ H²(Gal(L/K), Lˣ) it induces.

Main results

• TauCeti.exists_unitsMap_eq_of_smul_eq: a unit of L fixed by a generator of Gal(L/K) comes from K.
• TauCeti.cyclicClass_apply: the cyclic class is the explicit two-periodicity class of the embedded ground-field unit.
• TauCeti.cyclicClass_surjective: every class in H²(Gal(L/K), Lˣ) is the class of an element of Kˣ.
• TauCeti.cyclicClass_eq_zero_iff: the class of a vanishes exactly when a is a norm from L.
• TauCeti.H2π_eq_cyclicClass: a 2-cocycle with the values of the carry cocycle of a represents the class of a.
• TauCeti.exists_H2π_eq_cyclicClass: such a carry representative exists.
• TauCeti.map_cyclicClass: inflation along a tower of cyclic Galois extensions sends the class of a to the class of a ^ [M : L].
• TauCeti.map_cyclicClass_baseChange: base change of cyclic Galois extensions with g'|_L = g ^ d sends the class of a to the class of a ^ (d · [M' : K'] / [L : K]).
• TauCeti.natCard_H2_units_eq_herbrandQuotient: the order of H²(Gal(L/K), Lˣ) is the Herbrand quotient of Lˣ.

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter VIII, §4, and Chapter XIV, §1.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §4.7.

theorem TauCeti.exists_unitsMap_eq_of_smul_eq {K L : Type} [Field K] [Field L] [Algebra K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {x : Lˣ} (hx : g • x = x) : ∃ (a : Kˣ), (Units.map ↑(algebraMap K L)) a = x

A unit fixed by a generator comes from the base field: if g generates Gal(L/K), a unit of L fixed by g is the image of a unit of K.

noncomputable def TauCeti.cyclicClass {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) : Additive Kˣ →+ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))

The class in H²(Gal(L/K), Lˣ) of an element of Kˣ, for a cyclic Galois extension with generator g: the image of a, which is fixed by g, under two-periodicity of the cohomology of the cyclic group Gal(L/K) at g. It is represented by the carry cocycle of a at g.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.cyclicClass_apply {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (a : Kˣ) : have x := ⋯; let x := IsCyclic.commGroup; (cyclicClass hg) (Additive.ofMul a) = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) g hg 2 ⋯)) ⟨Rep.toAdditive.symm (Additive.ofMul ((Units.map ↑(algebraMap K L)) a)), ⋯⟩

The cyclic class of a ground-field unit is its image under two-periodicity.

theorem TauCeti.cyclicClass_surjective {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) : Function.Surjective ⇑(cyclicClass hg)

Every class in H²(Gal(L/K), Lˣ) is the class of an element of Kˣ.

@[simp]

theorem TauCeti.cyclicClass_eq_zero_iff {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {a : Kˣ} : (cyclicClass hg) (Additive.ofMul a) = 0 ↔ a ∈ normGroup K L

The class of a ∈ Kˣ in H²(Gal(L/K), Lˣ) vanishes exactly when a is a norm from L.

Inflation along a tower of cyclic Galois extensions

theorem TauCeti.map_cyclicClass {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {M : Type} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [FiniteDimensional K M] [IsGalois K M] {g' : Gal(M/K)} (hg' : ∀ (σ : Gal(M/K)), σ ∈ Subgroup.zpowers g') (hgg' : (AlgEquiv.restrictNormalHom L) g' = g) (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (AlgEquiv.restrictNormalHom L) (unitsInflationHom K L M) 2)) ((cyclicClass hg) (Additive.ofMul a)) = (cyclicClass hg') (Additive.ofMul (a ^ Module.finrank L M))

Inflation of cyclic classes. For cyclic Galois extensions K ⊆ L ⊆ M whose generators are compatible, g'|_L = g, inflation H²(Gal(L/K), Lˣ) → H²(Gal(M/K), Mˣ) sends the class of a ∈ Kˣ to the class of a ^ [M : L].

Base change of cyclic Galois extensions

theorem TauCeti.map_cyclicClass_baseChange {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {K' M' : Type} [Field K'] [Field M'] [Algebra K K'] [Algebra K' M'] [Algebra K M'] [IsScalarTower K K' M'] [Algebra L M'] [IsScalarTower K L M'] [FiniteDimensional K' M'] [IsGalois K' M'] {g' : Gal(M'/K')} (hg' : ∀ (σ : Gal(M'/K')), σ ∈ Subgroup.zpowers g') (d : ℕ) (hgg' : (AlgEquiv.restrictScalars K g').restrictNormal L = g ^ d) (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K L K' M') 2)) ((cyclicClass hg) (Additive.ofMul a)) = (cyclicClass hg') (Additive.ofMul ((Units.map ↑(algebraMap K K')) a ^ (d * Module.finrank K' M' / Module.finrank K L)))

Base change of cyclic classes. Let L/K and M'/K' be cyclic Galois extensions with K ⊆ K' and L ⊆ M', whose generators satisfy g'|_L = g ^ d. Then the map H²(Gal(L/K), Lˣ) → H²(Gal(M'/K'), M'ˣ) induced by restriction Gal(M'/K') → Gal(L/K) and the inclusion Lˣ → M'ˣ sends the class of a ∈ Kˣ to the class of a ^ (d · [M' : K'] / [L : K]).

@[simp]

theorem TauCeti.cyclicClass_eq_iff {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {a b : Kˣ} : (cyclicClass hg) (Additive.ofMul a) = (cyclicClass hg) (Additive.ofMul b) ↔ a / b ∈ normGroup K L

The classes of a and b agree exactly when a / b is a norm from L.

theorem TauCeti.H2π_eq_cyclicClass {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (z : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) (a : Kˣ) (hz : ∀ (i j : ℕ), i < orderOf g → j < orderOf g → Additive.toMul (z (g ^ i, g ^ j)) = if orderOf g ≤ i + j then (Units.map ↑(algebraMap K L)) a else 1) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) z = (cyclicClass hg) (Additive.ofMul a)

The class of a is the class of its carry cocycle. A 2-cocycle z of Gal(L/K) with values in Lˣ whose values at (gⁱ, gʲ), for 0 ≤ i, j < n with n the order of g, are a if i + j ≥ n and 1 otherwise represents cyclicClass hg a.

theorem TauCeti.exists_H2π_eq_cyclicClass {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (a : Kˣ) : ∃ (z : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))), (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) z = (cyclicClass hg) (Additive.ofMul a) ∧ ∀ (i j : ℕ), i < orderOf g → j < orderOf g → Additive.toMul (z (g ^ i, g ^ j)) = if orderOf g ≤ i + j then (Units.map ↑(algebraMap K L)) a else 1

The class of a has a carry representative: some 2-cocycle of Gal(L/K) with values in Lˣ represents cyclicClass hg a and takes the value a at (gⁱ, gʲ) if i + j ≥ n and 1 otherwise, for 0 ≤ i, j < n with n the order of g.

noncomputable def TauCeti.cyclicNormQuotientEquiv {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) : Additive (Kˣ ⧸ normGroup K L) ≃+ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))

H² of a cyclic Galois extension is the norm quotient: Kˣ / N_{L/K}(Lˣ) ≃ H²(Gal(L/K), Lˣ), sending the class of a to cyclicClass hg a (cyclicNormQuotientEquiv_mk). It depends on the generator g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.cyclicNormQuotientEquiv_mk {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (a : Kˣ) : (cyclicNormQuotientEquiv hg) (Additive.ofMul ↑a) = (cyclicClass hg) (Additive.ofMul a)

cyclicNormQuotientEquiv sends the class of a ∈ Kˣ to cyclicClass hg a.

theorem TauCeti.natCard_H2_units_eq_herbrandQuotient {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsCyclic Gal(L/K)] : ↑(Nat.card ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction Gal(L/K) Lˣ))) = TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ)

The order of H² of a cyclic extension is the Herbrand quotient of its units. For a finite extension L/K whose automorphism group is cyclic, Hilbert's Theorem 90 (groupCohomology.H1ofAutOnUnitsUnique) makes H¹(Aut(L/K), Lˣ) vanish, so the order of H²(Aut(L/K), Lˣ) is the Herbrand quotient of Lˣ.