Restriction across a finite extension of fields

A finite extension L/K and an embedding σ : L →ₐ[K] Kˢ identify G_L with the open subgroup of G_K fixing σ(L). This file transports continuous cohomology with trivial 𝔽₂ coefficients across that identification and defines restriction from G_K to G_L.

The formula for galoisRes is restriction to galoisSubgroup K L σ, followed by transport along galoisSubgroupEquiv K L σ. Its direct compatible-pair form pulls back along the composite G_L → G_K. The chosen embedding is part of both formulas, but not of the resulting map: another embedding, or another extension of σ to the separable closures, changes the composite G_L → G_K by an inner automorphism of G_K, and inner automorphisms act trivially on cohomology. So galoisRes is a map attached to L/K alone, and it is functorial in towers.

Main definitions

• TauCeti.galoisF2Iso: transport of trivial-coefficient cohomology from the fixing subgroup to G_L.
• TauCeti.galoisRes: restriction from G_K to G_L.

Main results

• TauCeti.galoisRes_cup: restriction preserves the 𝔽₂-valued cup product.
• TauCeti.galoisRes_embedding_independent: restriction does not depend on the embedding.
• TauCeti.galoisRes_comp, TauCeti.galoisRes_galoisRes: restriction is functorial in a tower K ⊆ L ⊆ M.

Reference

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, for restriction through the open subgroup associated to a finite extension, and (1.5.3)(i) for its compatibility with cup products.

noncomputable def TauCeti.galoisF2Iso (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : continuousCohomology n (trivialF2 ↥↑(galoisSubgroup K L σ)) ≅ continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L))

Cohomology of the fixing subgroup of σ(L) identified with cohomology of G_L, with trivial 𝔽₂ coefficients, in every degree.

Equations

• TauCeti.galoisF2Iso K L σ n = TauCeti.trivialF2Iso (TauCeti.galoisSubgroupEquiv K L σ).symm n

@[simp]

theorem TauCeti.galoisF2Iso_hom (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : (galoisF2Iso K L σ n).hom = trivialF2Map (↑(galoisSubgroupEquiv K L σ)) n

The forward transport is cohomological pullback along G_L ≃ galoisSubgroup K L σ.

@[simp]

theorem TauCeti.galoisF2Iso_inv (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : (galoisF2Iso K L σ n).inv = trivialF2Map (↑(galoisSubgroupEquiv K L σ).symm) n

The inverse transport is pullback along the inverse topological group isomorphism.

noncomputable def TauCeti.galoisRes (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 K)) ⟶ continuousCohomology n (trivialF2 (AbsoluteGaloisGroup L))

Restriction on 𝔽₂-cohomology for the finite extension L/K, relative to σ. It is subgroup restriction followed by the canonical identification with G_L.

Equations

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

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

The definition of field-extension restriction as subgroup restriction followed by transport to the absolute Galois group of L.

theorem TauCeti.galoisRes_eq_map (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (n : ℕ) : galoisRes K L σ n = trivialF2Map ((ContinuousMonoidHom.subgroupSubtype ↑(galoisSubgroup K L σ)).comp ↑(galoisSubgroupEquiv K L σ)) n

Field-extension restriction is the compatible-pair map along the composite G_L → galoisSubgroup K L σ → G_K.

@[simp]

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

Restriction preserves the cup product on 𝔽₂-cohomology, in every bidegree: res (x ⌣ y) = res x ⌣ res y.

Independence of the embedding and towers

theorem TauCeti.galoisRes_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 : ℕ) : galoisRes K L σ n = galoisRes K L τ n

Field-extension restriction does not depend on the embedding: two K-embeddings σ τ : L →ₐ[K] Kˢ induce the same restriction Hⁿ(G_K, 𝔽₂) ⟶ Hⁿ(G_L, 𝔽₂), in every degree. The two homomorphisms G_L → G_K differ by an inner automorphism of G_K.

theorem TauCeti.galoisRes_comp (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (M : Type u) [Field M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [FiniteDimensional L M] [FiniteDimensional K M] (τ : M →ₐ[L] SeparableClosure L) (ρ : M →ₐ[K] SeparableClosure K) (n : ℕ) : CategoryTheory.CategoryStruct.comp (galoisRes K L σ n) (galoisRes L M τ n) = galoisRes K M ρ n

Restriction is functorial in a tower K ⊆ L ⊆ M: restricting from G_K to G_L and then to G_M is restriction from G_K to G_M. The three embeddings σ, τ and ρ are arbitrary and need not be compatible with one another.

theorem TauCeti.galoisRes_galoisRes (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (M : Type u) [Field M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [FiniteDimensional L M] [FiniteDimensional K M] (τ : M →ₐ[L] SeparableClosure L) (ρ : M →ₐ[K] SeparableClosure K) (n : ℕ) (x : ↑(continuousCohomology n (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisRes L M τ n)) ((CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) x) = (CategoryTheory.ConcreteCategory.hom (galoisRes K M ρ n)) x

res (res x) = res x along a tower K ⊆ L ⊆ M, for every class x ∈ Hⁿ(G_K, 𝔽₂) and arbitrary embeddings.