Corestriction with trivial 𝔽₂ coefficients

For an open subgroup U of finite index in a profinite group G, all-degree corestriction TauCeti.ContinuousCohomology.corestriction is stated for the coefficient object ofDiscreteModule ℤ U M of a discrete G-module M. With M the carrier of the trivial 𝔽₂ object, both ends of that map are the trivial 𝔽₂ objects trivialF2 U and trivialF2 G, but only up to propositional equalities of coefficient objects. This file reads corestriction through those equalities, giving the map Hⁿ(U, 𝔽₂) ⟶ Hⁿ(G, 𝔽₂) that pairs with the trivial-coefficient restriction TauCeti.trivialF2ResMap, and transports the identity cor ∘ res = [G : U].

Main definitions

• TauCeti.trivialF2CorMap: corestriction Hⁿ(U, 𝔽₂) ⟶ Hⁿ(G, 𝔽₂) with trivial coefficients.

Main results

• TauCeti.ofDiscreteModule_subgroup_trivialF2: over a subgroup U, the coefficient dictionary recovers the trivial 𝔽₂ object of U.
• TauCeti.trivialF2ResMap_comp_trivialF2CorMap, TauCeti.trivialF2CorMap_trivialF2ResMap: restriction followed by corestriction is multiplication by the index [G : U].
• TauCeti.trivialF2ResMap_explicitH1AddEquivContinuousCohomology, TauCeti.trivialF2ResMap_explicitH2AddEquivContinuousCohomology: in degrees one and two, restriction is explicit restriction of cocycles.
• TauCeti.trivialF2CorMap_explicitH1AddEquivContinuousCohomology, TauCeti.trivialF2CorMap_explicitH2AddEquivContinuousCohomology: in degrees one and two, corestriction is the explicit transversal formula on cocycles.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7).

theorem TauCeti.continuousSMul_trivialF2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(trivialF2 G)

G acts continuously on the carrier of the trivial 𝔽₂ object, which is smooth discrete.

theorem TauCeti.ofDiscreteModule_subgroup_trivialF2 (G : Type u) [Group G] (U : Subgroup G) : ofDiscreteModule ℤ ↥U ↑(trivialF2 G) = trivialF2 ↥U

Over a subgroup U, the coefficient object of the carrier of trivialF2 G is trivialF2 U: it is the restriction of ofDiscreteModule ℤ G (trivialF2 G).V = trivialF2 G (res_ofDiscreteModule, ofDiscreteModule_trivialF2, res_trivialF2). This types the transport of an operation stated for ofDiscreteModule ℤ U M, such as corestriction, to trivial 𝔽₂ coefficients.

theorem TauCeti.trivialF2Equiv_eqToHom_ofDiscreteModule_subgroup_trivialF2 (G : Type u) [Group G] (U : Subgroup G) (x : ↑(ofDiscreteModule ℤ ↥U ↑(trivialF2 G))) : (trivialF2Equiv ↥U) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x) = (trivialF2Equiv G) x

Transport along ofDiscreteModule_subgroup_trivialF2 preserves the underlying ZMod 2 value.

noncomputable def TauCeti.trivialF2CorMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : continuousCohomology n (trivialF2 ↥U) ⟶ continuousCohomology n (trivialF2 G)

Corestriction with trivial 𝔽₂ coefficients, Hⁿ(U, 𝔽₂) ⟶ Hⁿ(G, 𝔽₂), for an open finite-index subgroup U of a profinite group G: all-degree corestriction TauCeti.ContinuousCohomology.corestriction at the carrier of trivialF2 G, read through the identifications of both coefficient objects with the trivial 𝔽₂ objects.

Equations

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

theorem TauCeti.trivialF2CorMap_def (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : trivialF2CorMap G U hU n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.corestriction U (↑(trivialF2 G)) hU n) (CategoryTheory.eqToHom ⋯))

The defining equation of corestriction with trivial 𝔽₂ coefficients.

theorem TauCeti.trivialF2ResMap_comp_trivialF2CorMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp (trivialF2ResMap G U n) (trivialF2CorMap G U hU n) = U.index • CategoryTheory.CategoryStruct.id (continuousCohomology n (trivialF2 G))

cor ∘ res = [G : U] with trivial 𝔽₂ coefficients, in every degree (NSW (1.5.7)).

@[simp]

theorem TauCeti.trivialF2CorMap_trivialF2ResMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) (x : ↑(continuousCohomology n (trivialF2 G)).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (trivialF2CorMap G U hU n)) ((CategoryTheory.ConcreteCategory.hom (trivialF2ResMap G U n)) x) = U.index • x

cor (res x) = [G : U] • x with trivial 𝔽₂ coefficients, for every class x ∈ Hⁿ(G, 𝔽₂).

theorem TauCeti.trivialF2ResMap_explicitH1AddEquivContinuousCohomology (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (x : ContCohomology.H1 G ↑(trivialF2 G)) : (CategoryTheory.ConcreteCategory.hom (trivialF2ResMap G U 1)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH1AddEquivContinuousCohomology G ↑(trivialF2 G)) x)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH1AddEquivContinuousCohomology ↥U ↑(trivialF2 G)) ((ContCohomology.explicitRes1 G (↑(trivialF2 G)) U) x))

Degree-one restriction with trivial 𝔽₂ coefficients is explicit restriction of cocycles. A class of H¹(G, 𝔽₂) presented by an explicit cocycle valued in the carrier of trivialF2 G is sent to the class of its restriction TauCeti.ContCohomology.explicitRes1 to U, both read in continuous cohomology through the identifications of the coefficient objects with the trivial 𝔽₂ objects.

theorem TauCeti.trivialF2ResMap_explicitH2AddEquivContinuousCohomology (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) [LocallyCompactSpace G] [LocallyCompactSpace ↥U] (x : ContCohomology.H2 G ↑(trivialF2 G)) : (CategoryTheory.ConcreteCategory.hom (trivialF2ResMap G U 2)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH2AddEquivContinuousCohomology G ↑(trivialF2 G)) x)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH2AddEquivContinuousCohomology ↥U ↑(trivialF2 G)) ((ContCohomology.explicitRes2 G (↑(trivialF2 G)) U) x))

Degree-two restriction with trivial 𝔽₂ coefficients is explicit restriction of cocycles. A class of H²(G, 𝔽₂) presented by an explicit cocycle valued in the carrier of trivialF2 G is sent to the class of its restriction TauCeti.ContCohomology.explicitRes2 to U, both read in continuous cohomology through the identifications of the coefficient objects with the trivial 𝔽₂ objects.

theorem TauCeti.trivialF2CorMap_explicitH1AddEquivContinuousCohomology (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (x : ContCohomology.H1 ↥U ↑(trivialF2 G)) : (CategoryTheory.ConcreteCategory.hom (trivialF2CorMap G U hU 1)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH1AddEquivContinuousCohomology ↥U ↑(trivialF2 G)) x)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH1AddEquivContinuousCohomology G ↑(trivialF2 G)) ((ContCohomology.explicitCor1 G (↑(trivialF2 G)) U hU) x))

Degree-one corestriction with trivial 𝔽₂ coefficients is the explicit transversal formula. A class of H¹(U, 𝔽₂) presented by an explicit cocycle valued in the carrier of trivialF2 G is sent to the class of its explicit corestriction TauCeti.ContCohomology.explicitCor1, both read in continuous cohomology through the identifications of the coefficient objects with the trivial 𝔽₂ objects.

theorem TauCeti.trivialF2CorMap_explicitH2AddEquivContinuousCohomology (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsOpen ↑U) [U.FiniteIndex] (x : ContCohomology.H2 ↥U ↑(trivialF2 G)) : have x_1 := ⋯; (CategoryTheory.ConcreteCategory.hom (trivialF2CorMap G U hU 2)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH2AddEquivContinuousCohomology ↥U ↑(trivialF2 G)) x)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ContCohomology.explicitH2AddEquivContinuousCohomology G ↑(trivialF2 G)) ((ContCohomology.explicitCor2 G (↑(trivialF2 G)) U hU) x))

Degree-two corestriction with trivial 𝔽₂ coefficients is the explicit transversal formula, under the degree-two comparison and the canonical coefficient identifications.