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: each of the six statements below is the instance, at the compatible pair (U ↪ G, id), of the corresponding theorem of TauCeti/RepresentationTheory/Homological/ContCohomology/Cup/Naturality.lean, and together they 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

Multiplication on the subgroup U is continuous for the subspace topology.

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.