Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Restriction

Restriction preserves explicit low-degree cup products #

Restriction along a subgroup preserves each of the six cup products on explicit continuous cohomology:

res (a ⌣ b) = res a ⌣ res b.

This is the low-degree inhomogeneous form of the naturality of the cup product. On cocycle representatives it is an equality, not merely an equality modulo coboundaries: restriction is precomposition with the subgroup inclusion, and the pairing and the translation factor in the cup formula are unchanged. The six statements below expose that compatibility in every bidegree (p, q) with p + q ≤ 2.

Main statements #

Reference #

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

source
@[simp]
theorem TauCeti.ContCohomology.explicitRes0_explicitCup00 (G : Type uG) [Group G] (M : Type uM) [AddCommGroup M] [DistribMulAction G M] (N : Type uN) [AddCommGroup N] [DistribMulAction G N] (P : Type uP) [AddCommGroup P] [DistribMulAction G P] (U : Subgroup G) (μ : M →+ N →+ P) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : ↥(H0 G M)) (b : ↥(H0 G N)) :
(explicitRes0 G P U) (((explicitCup00 G M N P μ hequiv) a) b) = ((explicitCup00 (↥U) M N P μ ⋯) ((explicitRes0 G M U) a)) ((explicitRes0 G N U) b)

Restriction preserves the (0,0) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitRes1_explicitCup01 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : ↥(H0 G M)) (b : H1 G N) :
(explicitRes1 G P U) (((explicitCup01 G M N P μ hμ hequiv) a) b) = ((explicitCup01 (↥U) M N P μ hμ ⋯) ((explicitRes0 G M U) a)) ((explicitRes1 G N U) b)

Restriction preserves the (0,1) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitRes1_explicitCup10 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : H1 G M) (b : ↥(H0 G N)) :
(explicitRes1 G P U) (((explicitCup10 G M N P μ hμ hequiv) a) b) = ((explicitCup10 (↥U) M N P μ hμ ⋯) ((explicitRes1 G M U) a)) ((explicitRes0 G N U) b)

Restriction preserves the (1,0) cup product.

source
theorem TauCeti.ContCohomology.instContinuousMulSubtypeMemSubgroup_tauCeti (G : Type uG) [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) :
ContinuousMul ↥U
source
@[simp]
theorem TauCeti.ContCohomology.explicitRes2_explicitCup02 (G : Type uG) [Group G] [TopologicalSpace G] [ContinuousMul G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : ↥(H0 G M)) (b : H2 G N) :
(explicitRes2 G P U) (((explicitCup02 G M N P μ hμ hequiv) a) b) = ((explicitCup02 (↥U) M N P μ hμ ⋯) ((explicitRes0 G M U) a)) ((explicitRes2 G N U) b)

Restriction preserves the (0,2) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitRes2_explicitCup11 (G : Type uG) [Group G] [TopologicalSpace G] [ContinuousMul G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : H1 G M) (b : H1 G N) :
(explicitRes2 G P U) (((explicitCup11 G M N P μ hμ hequiv) a) b) = ((explicitCup11 (↥U) M N P μ hμ ⋯) ((explicitRes1 G M U) a)) ((explicitRes1 G N U) b)

Restriction preserves the (1,1) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitRes2_explicitCup20 (G : Type uG) [Group G] [TopologicalSpace G] [ContinuousMul G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [DistribMulAction G N] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (U : Subgroup G) (μ : M →+ N →+ P) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (a : H2 G M) (b : ↥(H0 G N)) :
(explicitRes2 G P U) (((explicitCup20 G M N P μ hμ hequiv) a) b) = ((explicitCup20 (↥U) M N P μ hμ ⋯) ((explicitRes2 G M U) a)) ((explicitRes0 G N U) b)

Restriction preserves the (2,0) cup product.