The cup product does not see the scalars

Let P : TopPairing X Y Z be a coefficient pairing of topological representations over a topological commutative ring R. Forgetting the scalars gives a pairing P.restrictScalarsInt of the underlying additive representations, with the same underlying biadditive map, and continuous cohomology does not see the scalars either (TauCeti.ContCohomology.restrictScalarsIntEquiv). This file proves that the two are compatible in the bidegrees (1, 1), (0, 2) and (2, 0) of total degree two: the cup product of P.restrictScalarsInt is the cup product of P, read through restrictScalarsIntEquiv (TauCeti.TopPairing.cup_one_one_restrictScalarsInt and its companions), and already on cocycles (TauCeti.TopPairing.cupCocycles_one_one_restrictScalarsInt and its companions). The reason is that both cup products are the Alexander–Whitney formula on the same iterated function spaces, and the identification of the cocycles does not change their values.

The consequence this is for: the explicit low-degree cup products of TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Product, given by cochain formulas on inhomogeneous cocycles, agree with the canonical cup product of a pairing of discrete representations over any scalars, under the comparison isomorphisms TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete and TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete (TauCeti.TopPairing.cup_one_one_explicitH1AddEquivContinuousCohomologyOfDiscrete). The agreement for the pairings TauCeti.ofDiscreteModulePairing of discrete ℤ-modules is TauCeti.ContCohomology.explicitAddEquiv_cup11; the statement here removes the restriction to ℤ, which is what the coefficient objects of the pro-p theory, objects of TopRep (ZMod p) G, need in order to compute their cup product on explicit cocycles.

Main definitions

• TauCeti.TopPairing.restrictScalarsInt: the coefficient pairing of the underlying additive representations.

Main results

• TauCeti.TopPairing.cupCocycles_one_one_restrictScalarsInt, TauCeti.TopPairing.cup_one_one_restrictScalarsInt: the cup product does not see the scalars, on one-cocycles and on cohomology in bidegree (1, 1); cupCocycles_zero_two_restrictScalarsInt, cup_zero_two_restrictScalarsInt, cupCocycles_two_zero_restrictScalarsInt and cup_two_zero_restrictScalarsInt are the same in bidegrees (0, 2) and (2, 0).
• TauCeti.TopPairing.cup_one_one_ofDiscreteModuleRestrictScalarsInt, cup_zero_two_ofDiscreteModuleRestrictScalarsInt and cup_two_zero_ofDiscreteModuleRestrictScalarsInt: for discrete representations, the cup product of the associated pairing of discrete ℤ-modules is the cup product of P, under TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv.
• TauCeti.TopPairing.cup_one_one_explicitH1AddEquivContinuousCohomologyOfDiscrete: the canonical cup product of a pairing of discrete representations over any scalars is the explicit (1,1) cup product on their carriers, (a ⌣ b) (g, h) = μ (a g) (g • b h).

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter V, §3, for the Alexander–Whitney formula.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §4, for the inhomogeneous cup product formulas.

def TauCeti.TopPairing.restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Monoid G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) : TopPairing (TopRep.restrictScalarsInt.obj X) (TopRep.restrictScalarsInt.obj Y) (TopRep.restrictScalarsInt.obj Z)

The coefficient pairing of the underlying additive representations: the pairing P with its scalars forgotten, an ℤ-bilinear pairing with the same values.

Equations

• P.restrictScalarsInt = { bil := LinearMap.restrictScalars₁₂ ℤ ℤ P.bil, cont := ⋯, equivariant := ⋯ }

@[simp]

theorem TauCeti.TopPairing.restrictScalarsInt_bil {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Monoid G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (x : ↑(TopRep.restrictScalarsInt.obj X)) (y : ↑(TopRep.restrictScalarsInt.obj Y)) : (P.restrictScalarsInt.bil x) y = (P.bil x) y

The pairing with its scalars forgotten has the values of P.

theorem TauCeti.TopPairing.cupCocycles_one_one_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 1).toModuleCat) (b : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj Y) 1).toModuleCat) : (ContCohomology.cocyclesRestrictScalarsIntEquiv Z (1 + 1)) (((P.restrictScalarsInt.cupCocycles 1 1) a) b) = ((P.cupCocycles 1 1) ((ContCohomology.cocyclesRestrictScalarsIntEquiv X 1) a)) ((ContCohomology.cocyclesRestrictScalarsIntEquiv Y 1) b)

The cup product of one-cocycles does not see the scalars: under TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv, the cup product of two one-cocycles for the pairing of the underlying additive representations is their cup product for P.

theorem TauCeti.TopPairing.cup_one_one_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(continuousCohomology 1 (TopRep.restrictScalarsInt.obj X)).toModuleCat) (b : ↑(continuousCohomology 1 (TopRep.restrictScalarsInt.obj Y)).toModuleCat) : (ContCohomology.restrictScalarsIntEquiv Z (1 + 1)) (((P.restrictScalarsInt.cup 1 1) a) b) = ((P.cup 1 1) ((ContCohomology.restrictScalarsIntEquiv X 1) a)) ((ContCohomology.restrictScalarsIntEquiv Y 1) b)

The cup product in bidegree (1, 1) does not see the scalars: under TauCeti.ContCohomology.restrictScalarsIntEquiv, the cup product of the pairing of the underlying additive representations is the cup product of P.

theorem TauCeti.TopPairing.cupCocycles_zero_two_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 0).toModuleCat) (b : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj Y) 2).toModuleCat) : (ContCohomology.cocyclesRestrictScalarsIntEquiv Z (0 + 2)) (((P.restrictScalarsInt.cupCocycles 0 2) a) b) = ((P.cupCocycles 0 2) ((ContCohomology.cocyclesRestrictScalarsIntEquiv X 0) a)) ((ContCohomology.cocyclesRestrictScalarsIntEquiv Y 2) b)

The cup product of a zero-cocycle and a two-cocycle does not see the scalars: under TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv, the cup product for the pairing of the underlying additive representations is the cup product for P.

theorem TauCeti.TopPairing.cupCocycles_two_zero_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 2).toModuleCat) (b : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj Y) 0).toModuleCat) : (ContCohomology.cocyclesRestrictScalarsIntEquiv Z (2 + 0)) (((P.restrictScalarsInt.cupCocycles 2 0) a) b) = ((P.cupCocycles 2 0) ((ContCohomology.cocyclesRestrictScalarsIntEquiv X 2) a)) ((ContCohomology.cocyclesRestrictScalarsIntEquiv Y 0) b)

The cup product of a two-cocycle and a zero-cocycle does not see the scalars: under TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv, the cup product for the pairing of the underlying additive representations is the cup product for P.

theorem TauCeti.TopPairing.cup_zero_two_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(continuousCohomology 0 (TopRep.restrictScalarsInt.obj X)).toModuleCat) (b : ↑(continuousCohomology 2 (TopRep.restrictScalarsInt.obj Y)).toModuleCat) : (ContCohomology.restrictScalarsIntEquiv Z (0 + 2)) (((P.restrictScalarsInt.cup 0 2) a) b) = ((P.cup 0 2) ((ContCohomology.restrictScalarsIntEquiv X 0) a)) ((ContCohomology.restrictScalarsIntEquiv Y 2) b)

The cup product in bidegree (0, 2) does not see the scalars: under TauCeti.ContCohomology.restrictScalarsIntEquiv, the cup product of the pairing of the underlying additive representations is the cup product of P.

theorem TauCeti.TopPairing.cup_two_zero_restrictScalarsInt {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (a : ↑(continuousCohomology 2 (TopRep.restrictScalarsInt.obj X)).toModuleCat) (b : ↑(continuousCohomology 0 (TopRep.restrictScalarsInt.obj Y)).toModuleCat) : (ContCohomology.restrictScalarsIntEquiv Z (2 + 0)) (((P.restrictScalarsInt.cup 2 0) a) b) = ((P.cup 2 0) ((ContCohomology.restrictScalarsIntEquiv X 2) a)) ((ContCohomology.restrictScalarsIntEquiv Y 0) b)

The cup product in bidegree (2, 0) does not see the scalars: under TauCeti.ContCohomology.restrictScalarsIntEquiv, the cup product of the pairing of the underlying additive representations is the cup product of P.

Discrete representations over any scalars

theorem TauCeti.TopPairing.equivariant_of_eq {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] {X Y Z : TopRep k G} (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) (g : G) (x : ↑X) (y : ↑Y) : (μ (g • x)) (g • y) = g • (μ x) y

A biadditive map with the values of P is equivariant for the actions read off from the representations.

theorem TauCeti.TopPairing.eqToHom_ofDiscreteModulePairing_bil {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] {X Y Z : TopRep k G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] [DiscreteTopology ↑Z] (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) (x : ↑X) (y : ↑Y) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) (((ofDiscreteModulePairing μ ⋯).bil x) y) = (P.restrictScalarsInt.bil ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) y)

Under the identification of the underlying additive representation of a discrete X with the discrete ℤ-module X.V, the pairing of μ on discrete ℤ-modules is the pairing of P with its scalars forgotten: the three carriers are unchanged by the transports, so this is hμ.

theorem TauCeti.TopPairing.cup_one_one_ofDiscreteModuleRestrictScalarsInt {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep k G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] [DiscreteTopology ↑Z] (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) (a : ↑(continuousCohomology 1 (ofDiscreteModule ℤ G ↑X)).toModuleCat) (b : ↑(continuousCohomology 1 (ofDiscreteModule ℤ G ↑Y)).toModuleCat) : (ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Z (1 + 1)) ((((ofDiscreteModulePairing μ ⋯).cup 1 1) a) b) = ((P.cup 1 1) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X 1) a)) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Y 1) b)

For discrete representations, the cup product of the pairing of discrete ℤ-modules is the cup product of P, under TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv, in bidegree (1, 1).

theorem TauCeti.TopPairing.cup_zero_two_ofDiscreteModuleRestrictScalarsInt {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep k G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] [DiscreteTopology ↑Z] (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) (a : ↑(continuousCohomology 0 (ofDiscreteModule ℤ G ↑X)).toModuleCat) (b : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G ↑Y)).toModuleCat) : (ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Z (0 + 2)) ((((ofDiscreteModulePairing μ ⋯).cup 0 2) a) b) = ((P.cup 0 2) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X 0) a)) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Y 2) b)

For discrete representations, the cup product of the pairing of discrete ℤ-modules is the cup product of P, under TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv, in bidegree (0, 2).

theorem TauCeti.TopPairing.cup_two_zero_ofDiscreteModuleRestrictScalarsInt {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep k G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] [DiscreteTopology ↑Z] (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) (a : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G ↑X)).toModuleCat) (b : ↑(continuousCohomology 0 (ofDiscreteModule ℤ G ↑Y)).toModuleCat) : (ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Z (2 + 0)) ((((ofDiscreteModulePairing μ ⋯).cup 2 0) a) b) = ((P.cup 2 0) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X 2) a)) ((ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv Y 0) b)

For discrete representations, the cup product of the pairing of discrete ℤ-modules is the cup product of P, under TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv, in bidegree (2, 0).

theorem TauCeti.TopPairing.cup_one_one_explicitH1AddEquivContinuousCohomologyOfDiscrete {k : Type w} [CommRing k] [TopologicalSpace k] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep k G} [DiscreteTopology ↑X] [DiscreteTopology ↑Y] [DiscreteTopology ↑Z] (P : TopPairing X Y Z) (μ : ↑X →+ ↑Y →+ ↑Z) (hμ : ∀ (x : ↑X) (y : ↑Y), (μ x) y = (P.bil x) y) [ContinuousSMul G ↑X] [ContinuousSMul G ↑Y] [ContinuousSMul G ↑Z] [LocallyCompactSpace G] (x : ContCohomology.H1 G ↑X) (y : ContCohomology.H1 G ↑Y) : ((P.cup 1 1) (X.explicitH1AddEquivContinuousCohomologyOfDiscrete x)) (Y.explicitH1AddEquivContinuousCohomologyOfDiscrete y) = Z.explicitH2AddEquivContinuousCohomologyOfDiscrete (((ContCohomology.explicitCup11 G (↑X) (↑Y) (↑Z) μ ⋯ ⋯) x) y)

The canonical cup product of a pairing of discrete representations over any scalars is the explicit (1,1) cup product on their carriers. Under the comparisons TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete and TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete, the cup product TauCeti.TopPairing.cup in bidegree (1, 1) is TauCeti.ContCohomology.explicitCup11 for the biadditive map μ with the values of P, (a ⌣ b) (g, h) = μ (a g) (g • b h).