Corestriction across a finite extension of fields

A finite extension L/K and an embedding σ : L →ₐ[K] Kˢ identify G_L with the open subgroup galoisSubgroup K L σ of G_K, of index [L : K]. This file defines corestriction Hⁿ(G_L, 𝔽₂) ⟶ Hⁿ(G_K, 𝔽₂) along L/K, with trivial 𝔽₂ coefficients and in every degree, as the transport along galoisF2Iso K L σ followed by all-degree corestriction at galoisSubgroup K L σ. It is the companion of TauCeti.galoisRes, and the two satisfy cor ∘ res = [L : K].

The composite the other way round, res ∘ cor, is the identity plus the endomorphism galoisConj. For a quadratic extension the double-coset formula makes galoisConj conjugation by the nontrivial coset of G_L in G_K; it is written through res ∘ cor rather than through an element of that coset, so no such element is chosen.

Neither map depends on σ: another embedding changes the open subgroup and its identification with G_L by conjugation by an element of G_K, and corestriction is invariant under conjugation (TauCeti.ContinuousCohomology.map_comp_corestriction_of_conj). So galoisCor and galoisConj are attached to L/K alone.

Main definitions

• TauCeti.galoisCor: corestriction from G_L to G_K on 𝔽₂-cohomology.
• TauCeti.galoisConj: the endomorphism res ∘ cor - id of the 𝔽₂-cohomology of G_L.

Main results

• TauCeti.galoisRes_comp_galoisCor, TauCeti.galoisCor_galoisRes: restriction followed by corestriction is multiplication by the degree [L : K].
• TauCeti.galoisCor_comp_galoisRes, TauCeti.galoisRes_galoisCor: corestriction followed by restriction is y ↦ y + galoisConj y.
• TauCeti.galoisConj_galoisRes: on a restricted class, galoisConj is multiplication by [L : K] - 1.
• TauCeti.galoisConj_evensConj: for a quadratic extension, galoisConj is the conjugation OpenSubgroup.evensConj of the index-two subgroup galoisSubgroup K L σ, read through galoisF2Iso.
• TauCeti.galoisCor_embedding_independent, TauCeti.galoisConj_embedding_independent: corestriction and galoisConj do 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, and (1.5.7), for corestriction through the open subgroup associated to a finite extension.

noncomputable def TauCeti.galoisCor (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L)) ⟶ continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K))

Corestriction on 𝔽₂-cohomology for the finite extension L/K, relative to σ. It is the canonical identification of G_L with galoisSubgroup K L σ, followed by corestriction from that open subgroup to G_K.

Equations

• TauCeti.galoisCor K L σ n = CategoryTheory.CategoryStruct.comp (TauCeti.galoisF2Iso K L σ n).inv (TauCeti.trivialF2CorMap (TauCeti.AbsoluteGaloisGroup K) ↑(TauCeti.galoisSubgroup K L σ) ⋯ n)

theorem TauCeti.galoisCor_def (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : galoisCor K L σ n = CategoryTheory.CategoryStruct.comp (galoisF2Iso K L σ n).inv (trivialF2CorMap (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L σ) ⋯ n)

The definition of field-extension corestriction as transport to the open subgroup followed by subgroup corestriction.

theorem TauCeti.galoisF2Iso_hom_comp_galoisCor (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : CategoryTheory.CategoryStruct.comp (galoisF2Iso K L σ n).hom (galoisCor K L σ n) = trivialF2CorMap (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L σ) ⋯ n

Read on the open subgroup, field-extension corestriction is subgroup corestriction.

theorem TauCeti.galoisF2Iso_hom_comp_galoisCor_assoc (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (galoisF2Iso K L σ n).hom (CategoryTheory.CategoryStruct.comp (galoisCor K L σ n) h) = CategoryTheory.CategoryStruct.comp (trivialF2CorMap (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L σ) ⋯ n) h

Read on the open subgroup, field-extension corestriction is subgroup corestriction.

theorem TauCeti.galoisRes_comp_galoisCor (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : CategoryTheory.CategoryStruct.comp (galoisRes K L σ n) (galoisCor K L σ n) = Module.finrank K L • CategoryTheory.CategoryStruct.id (continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K)))

cor ∘ res = [L : K] on 𝔽₂-cohomology, in every degree (NSW (1.5.7)).

@[simp]

theorem TauCeti.galoisCor_galoisRes (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) (x : ↑(continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ n)) ((CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) x) = Module.finrank K L • x

cor (res x) = [L : K] • x for every class x ∈ Hⁿ(G_K, 𝔽₂).

noncomputable def TauCeti.galoisConj (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L)) ⟶ continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L))

The endomorphism res ∘ cor - id of Hⁿ(G_L, 𝔽₂) for the finite extension L/K, relative to σ. For a quadratic extension the double-coset formula identifies res ∘ cor with the sum of a class and its conjugate under the nontrivial coset of G_L in G_K, so this is the conjugate class; it is written through restriction and corestriction so that no element of that coset is chosen.

Equations

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

theorem TauCeti.galoisConj_def (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : galoisConj K L σ n = CategoryTheory.CategoryStruct.comp (galoisCor K L σ n) (galoisRes K L σ n) - CategoryTheory.CategoryStruct.id (continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L)))

The definition of galoisConj as corestriction followed by restriction, minus the identity.

theorem TauCeti.galoisCor_comp_galoisRes (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : CategoryTheory.CategoryStruct.comp (galoisCor K L σ n) (galoisRes K L σ n) = CategoryTheory.CategoryStruct.id (continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L))) + galoisConj K L σ n

res ∘ cor = id + galoisConj on Hⁿ(G_L, 𝔽₂), the definition of galoisConj solved for res ∘ cor.

theorem TauCeti.galoisRes_galoisCor (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) (y : ↑(continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) ((CategoryTheory.ConcreteCategory.hom (galoisCor K L σ n)) y) = y + (CategoryTheory.ConcreteCategory.hom (galoisConj K L σ n)) y

res (cor y) = y + galoisConj y for every class y ∈ Hⁿ(G_L, 𝔽₂).

theorem TauCeti.galoisConj_galoisRes (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) (x : ↑(continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisConj K L σ n)) ((CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) x) = (Module.finrank K L - 1) • (CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) x

On a restricted class, galoisConj is multiplication by [L : K] - 1. For a quadratic extension a restricted class is its own conjugate.

theorem TauCeti.galoisConj_evensConj (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) (n : ℕ) : galoisConj K L σ n = CategoryTheory.CategoryStruct.comp (galoisF2Iso K L σ n).inv (CategoryTheory.CategoryStruct.comp ((galoisSubgroup K L σ).evensConj ⋯ n) (galoisF2Iso K L σ n).hom)

For a quadratic extension, galoisConj is the index-two conjugation. Read through the identification galoisF2Iso of G_L with the open subgroup galoisSubgroup K L σ of index two, galoisConj is the conjugation OpenSubgroup.evensConj of the nontrivial coset of that subgroup; this is what lets identities stated with evensConj be read on the L/K side.

Independence of the embedding

theorem TauCeti.galoisCor_embedding_independent (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : L →ₐ[K] SeparableClosure K) (n : ℕ) : galoisCor K L σ n = galoisCor K L τ n

Field-extension corestriction does not depend on the embedding: two K-embeddings σ τ : L →ₐ[K] Kˢ induce the same corestriction Hⁿ(G_L, 𝔽₂) ⟶ Hⁿ(G_K, 𝔽₂), in every degree. The automorphism γ of Kˢ carrying the identification of separable closures attached to σ to the one attached to τ conjugates galoisSubgroup K L σ onto galoisSubgroup K L τ, compatibly with the two identifications with G_L, and corestriction is invariant under conjugation.

theorem TauCeti.galoisConj_embedding_independent (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : L →ₐ[K] SeparableClosure K) (n : ℕ) : galoisConj K L σ n = galoisConj K L τ n

The endomorphism galoisConj = res ∘ cor - id does not depend on the embedding: two K-embeddings σ τ : L →ₐ[K] Kˢ induce the same endomorphism galoisConj of Hⁿ(G_L, 𝔽₂). For a quadratic extension it is conjugation by the nontrivial coset of G_L in G_K.