The character of a quadratic field extension

A quadratic extension L/K, together with an embedding σ : L →ₐ[K] Kˢ, cuts out an index-two open subgroup of G_K. Its index-two character gives a class χ_{L/K} ∈ H¹(G_K, 𝔽₂). Although the subgroup is initially described using σ, quadratic fixing subgroups are normal and therefore independent of the embedding, so the resulting class is attached to the extension alone.

This is the field-extension form of OpenSubgroup.indexTwoCharacterClass. It is the character used by the index-two exact sequence and by the norm-of-restriction formula for the Evens norm.

Main definitions and results

• TauCeti.galoisCharacter: the class χ_{L/K} ∈ H¹(G_K, 𝔽₂).
• TauCeti.galoisCharacter_embedding_independent: the class does not depend on the embedding of L into Kˢ.

Reference

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §§5–6.

noncomputable def TauCeti.galoisCharacter (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The quadratic character χ_{L/K}. It is the class in H¹(G_K, 𝔽₂) of the index-two character whose kernel is the subgroup fixing the embedded copy σ(L).

Equations

• TauCeti.galoisCharacter K L σ hL = (TauCeti.galoisSubgroup K L σ).indexTwoCharacterClass ⋯

theorem TauCeti.galoisCharacter_def (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) : galoisCharacter K L σ hL = (galoisSubgroup K L σ).indexTwoCharacterClass ⋯

The quadratic character is the index-two character class of the Galois subgroup cut out by the chosen embedding.

theorem TauCeti.galoisCharacter_embedding_independent (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : L →ₐ[K] SeparableClosure K) (hL : Module.finrank K L = 2) : galoisCharacter K L σ hL = galoisCharacter K L τ hL

The quadratic character is independent of the embedding L →ₐ[K] Kˢ.