Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Inflation

Inflation preserves explicit low-degree cup products #

Let N be a normal subgroup of G. An equivariant pairing M × A → P restricts to a pairing Mᴺ × Aᴺ → Pᴺ on the invariant coefficients over G ⧸ N. Inflation preserves each of the six explicit cup products:

inf (a ⌣ b) = inf a ⌣ inf b.

The equality already holds on cocycle representatives: inflation precomposes cochains with the quotient map and includes their invariant values into the ambient coefficient modules.

Main statements #

Reference #

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

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl0_explicitCup00 (G : Type uG) [Group G] (M : Type uM) [AddCommGroup M] [DistribMulAction G M] (A : Type uA) [AddCommGroup A] [DistribMulAction G A] (P : Type uP) [AddCommGroup P] [DistribMulAction G P] (N : Subgroup G) [N.Normal] (μ : M →+ A →+ P) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M))) (b : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A))) :
(explicitInfl0 G P N) (((explicitCup00 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯) a) b) = ((explicitCup00 G M A P μ hequiv) ((explicitInfl0 G M N) a)) ((explicitInfl0 G A N) b)

Inflation preserves the (0,0) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl1_explicitCup01 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) P)] (μ : M →+ A →+ P) (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M))) (b : H1 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)) :
(explicitInfl1 G P N) (((explicitCup01 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) a) b) = ((explicitCup01 G M A P μ hμ hequiv) ((explicitInfl0 G M N) a)) ((explicitInfl1 G A N) b)

Inflation preserves the (0,1) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl1_explicitCup10 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [DistribMulAction G A] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) P)] (μ : M →+ A →+ P) (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : H1 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) (b : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A))) :
(explicitInfl1 G P N) (((explicitCup10 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) a) b) = ((explicitCup10 G M A P μ hμ hequiv) ((explicitInfl1 G M N) a)) ((explicitInfl0 G A N) b)

Inflation preserves the (1,0) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl2_explicitCup02 (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [DistribMulAction G M] (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) P)] (μ : M →+ A →+ P) (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M))) (b : H2 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)) :
(explicitInfl2 G P N) (((explicitCup02 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) a) b) = ((explicitCup02 G M A P μ hμ hequiv) ((explicitInfl0 G M N) a)) ((explicitInfl2 G A N) b)

Inflation preserves the (0,2) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl2_explicitCup11 (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) P)] (μ : M →+ A →+ P) (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : H1 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) (b : H1 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A)) :
(explicitInfl2 G P N) (((explicitCup11 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) a) b) = ((explicitCup11 G M A P μ hμ hequiv) ((explicitInfl1 G M N) a)) ((explicitInfl1 G A N) b)

Inflation preserves the (1,1) cup product.

source
@[simp]
theorem TauCeti.ContCohomology.explicitInfl2_explicitCup20 (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (A : Type uA) [AddCommGroup A] [TopologicalSpace A] [DistribMulAction G A] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) P)] (μ : M →+ A →+ P) (hμ : Continuous fun (p : M × A) => (μ p.1) p.2) (hequiv : ∀ (g : G) (m : M) (a : A), (μ (g • m)) (g • a) = g • (μ m) a) (a : H2 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) (b : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) A))) :
(explicitInfl2 G P N) (((explicitCup20 (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) M)) (↥(FixedPoints.addSubgroup (↥N) A)) (↥(FixedPoints.addSubgroup (↥N) P)) (N.fixedPointsPairing μ ⋯) ⋯ ⋯) a) b) = ((explicitCup20 G M A P μ hμ hequiv) ((explicitInfl2 G M N) a)) ((explicitInfl0 G A N) b)

Inflation preserves the (2,0) cup product.