The Alexander–Whitney cup product on homogeneous cochains

Mathlib computes the continuous cohomology of a topological representation X : TopRep R G as the homology of the homogeneous cochains TopRep.homogeneousCochains X: the m-cochains are the G-invariant elements of the (m + 1)-st term C(G, C(G, …, C(G, X.V))) of the coinduced resolution TopRep.resolutionX X, and the differential is the recursion (d F) g = F - d (F g) of TopRep.d. This file constructs the cup product of that complex.

A coefficient pairing TauCeti.TopPairing X Y Z is an R-bilinear map X.V →ₗ[R] Y.V →ₗ[R] Z.V that is jointly continuous and G-equivariant. Given one, the Alexander–Whitney formula

(a ⌣ b) (g₀, …, g_{m+n}) = μ (a (g₀, …, g_m)) (b (g_m, …, g_{m+n}))

pairs an m-cochain with an n-cochain. Read on the curried resolution it is the recursion (a ⌣ b) g = (a g) ⌣ b on the first argument, whose base case pairs the coefficient a g with every value of b g (TauCeti.TopPairing.pointwise). The pairing is first built as a jointly continuous map on the resolution with an explicit total degree (TauCeti.TopPairing.resolutionCup), whose two defining equations, TauCeti.TopPairing.resolutionCup_zero_apply and TauCeti.TopPairing.resolutionCup_succ_apply, hold by definition. It is bilinear, equivariant, and satisfies the Leibniz rule

d (a ⌣ b) = d a ⌣ b + (-1)^m (a ⌣ d b)

(TauCeti.TopPairing.resolutionCup_leibniz), so it descends to a bilinear map of homogeneous cochains TauCeti.TopPairing.cupCochain, with the Leibniz rule TauCeti.TopPairing.cupCochain_leibniz. Cocycles therefore cup to cocycles and coboundaries to coboundaries, which is what the cup product on continuous cohomology is built from.

Degrees

The total degree of a ⌣ b is m + n, but the recursion on m produces n + m, and the two are not definitionally equal. The resolution-level constructions therefore carry the total degree k as an explicit argument together with a proof k = n + m, so that every identity between them is stated without transport; TauCeti.TopPairing.resolutionCup_cast transports along an equality of degrees through Mathlib's HomologicalComplex.XIsoOfEq, whose evaluation rules are in TauCeti.RepresentationTheory.Homological.ContCohomology.DegreeCast. The bilinear maps TauCeti.TopPairing.resolutionCupPairing and TauCeti.TopPairing.cupCochain land in degree m + n; in their Leibniz rules the term d a ⌣ b lives in degree m + 1 + n and is transported.

Continuity

For fixed inputs a and b, the base case g ↦ (a g) ⌣ (b g) is the pointwise pairing composed with the continuous map g ↦ (a g, b g), and the successor step (a ⌣ b) g = (a g) ⌣ b is postcomposition with a fixed continuous map. The successor step, however, needs the base case to be jointly continuous in the pair (a, b) in order to be a well-defined continuous map, and joint continuity of (a, b) ↦ (g ↦ (a g, b g)) for the compact-open topologies is ContinuousMap.continuous_prodMk, which holds because a topological group is a regular space. No hypothesis beyond IsTopologicalGroup G is needed anywhere in the file.

Main definitions

• TauCeti.TopPairing: an equivariant jointly continuous bilinear pairing of topological representations, with TauCeti.ofDiscreteModulePairing for an equivariant biadditive map of discrete modules, TauCeti.TopPairing.flip for the opposite pairing (y, x) ↦ μ x y, and TauCeti.TopPairing.res for the restriction along a monoid homomorphism.
• TauCeti.TopPairing.pointwise: pairing a coefficient with every value of an iterated map.
• TauCeti.TopPairing.resolutionCup: the Alexander–Whitney pairing on the coinduced resolution, with explicit total degree.
• TauCeti.TopPairing.resolutionCupPairing: the same as a bilinear map into degree m + n, with TauCeti.TopPairing.resolutionCupPairing_zero_zero_apply and its five companions evaluating it in the bidegrees (m, n) with m + n ≤ 2.
• TauCeti.TopPairing.cupCochain: the cup product of homogeneous cochains.

Main results

• TauCeti.TopPairing.resolutionCup_ρ, TauCeti.TopPairing.continuous_resolutionCupPairing: the resolution pairing is equivariant and jointly continuous.
• TauCeti.TopPairing.resolutionCup_leibniz, TauCeti.TopPairing.resolutionCupPairing_leibniz, TauCeti.TopPairing.cupCochain_leibniz: the Leibniz rule.
• TauCeti.TopPairing.resolutionCupPairing_one_one_apply, TauCeti.TopPairing.cupCochain_one_one_apply: in bidegree (1, 1) the cup product is (a ⌣ b) g₀ g₁ g₂ = μ (a g₀ g₁) (b g₁ g₂), with no transport.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter V, §3, for the Alexander–Whitney formula on the standard resolution.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §4, (1.4.1), for the Leibniz rule.

Coefficient pairings

structure TauCeti.TopPairing {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Monoid G] (X Y Z : TopRep R G) : Type w

A coefficient pairing of topological representations: an R-bilinear map X.V →ₗ[R] Y.V →ₗ[R] Z.V that is jointly continuous and G-equivariant. Joint continuity is automatic for discrete coefficients and is not automatic in general, so it is carried as a field.

• bil : ↑X →ₗ[R] ↑Y →ₗ[R] ↑Z

  the underlying bilinear map

• cont : Continuous fun (p : ↑X × ↑Y) => (self.bil p.1) p.2

  joint continuity

• equivariant (g : G) (x : ↑X) (y : ↑Y) : (self.bil ((X.ρ g) x)) ((Y.ρ g) y) = (Z.ρ g) ((self.bil x) y)

  equivariance

theorem TauCeti.TopPairing.ext {R : Type u} {inst✝ : CommRing R} {inst✝¹ : TopologicalSpace R} {G : Type v} {inst✝² : Monoid G} {X Y Z : TopRep R G} {x y : TopPairing X Y Z} (bil : x.bil = y.bil) : x = y

theorem TauCeti.TopPairing.ext_iff {R : Type u} {inst✝ : CommRing R} {inst✝¹ : TopologicalSpace R} {G : Type v} {inst✝² : Monoid G} {X Y Z : TopRep R G} {x y : TopPairing X Y Z} : x = y ↔ x.bil = y.bil

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

The opposite pairing Y × X → Z, (y, x) ↦ μ x y, of a coefficient pairing μ : X × Y → Z.

Equations

• P.flip = { bil := P.bil.flip, cont := ⋯, equivariant := ⋯ }

@[simp]

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

@[simp]

theorem TauCeti.TopPairing.flip_flip {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Monoid G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) : P.flip.flip = P

theorem TauCeti.TopPairing.bil_transport {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Monoid G] {X Y Z : TopRep R G} (Q : TopPairing X Y Z) {X' Y' Z' : TopRep R G} (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (x : ↑X') (y : ↑Y') : ((cast ⋯ Q).bil x) y = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom hZ)) ((Q.bil ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) y))

Transport of a coefficient pairing along equalities of coefficient objects, read on carriers: the pairing cast along X = X', Y = Y' and Z = Z' is the original one conjugated by the transports of the carriers.

def TauCeti.ofDiscreteModulePairing {G : Type v} [Monoid G] {M N P : Type w} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) : TopPairing (ofDiscreteModule ℤ G M) (ofDiscreteModule ℤ G N) (ofDiscreteModule ℤ G P)

An equivariant biadditive map of discrete G-modules, μ (g • m) (g • n) = g • μ m n, as a coefficient pairing of the corresponding objects TauCeti.ofDiscreteModule ℤ G M. Joint continuity holds because the modules are discrete.

Equations

• TauCeti.ofDiscreteModulePairing μ hμ = { bil := μ.toIntLinearMap₂, cont := ⋯, equivariant := ⋯ }

@[simp]

theorem TauCeti.ofDiscreteModulePairing_bil_apply {G : Type v} [Monoid G] {M N P : Type w} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (m : M) (n : N) : ((ofDiscreteModulePairing μ hμ).bil m) n = (μ m) n

The restricted pairing

def TauCeti.TopPairing.res {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (φ : H →* G) : TopPairing (TopRep.res φ X) (TopRep.res φ Y) (TopRep.res φ Z)

The restriction of a coefficient pairing along a monoid homomorphism φ : H →* G: the same bilinear map, which is H-equivariant for the restricted actions.

Equations

• P.res φ = { bil := P.bil, cont := ⋯, equivariant := ⋯ }

@[simp]

theorem TauCeti.TopPairing.res_bil {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (φ : H →* G) : (P.res φ).bil = P.bil

The restricted pairing has the same underlying bilinear map.

Pairing a coefficient with every value of an iterated map

The n-th term of the coinduced resolution of Y is the iterated function space C(G, C(G, …, Y.V)). Pairing a fixed coefficient x : X.V with every value of such a function gives an element of the n-th term of the resolution of Z. The target degree k is an explicit argument with a proof k = n, so that the recursion below reduces definitionally in both the degree of the source and that of the target.

def TauCeti.TopPairing.pointwise {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) (n k : ℕ) : k = n → C(↑X × ↑(Y.resolutionX n), ↑(Z.resolutionX k))

Pairing a coefficient x : X.V with every value of an n-fold iterated continuous map F : C(G, C(G, …, Y.V)), as a jointly continuous map into the k-th term of the resolution of Z, for k = n.

Equations

• P.pointwise 0 0 x_3 = { toFun := fun (p : ↑X × ↑(Y.resolutionX 0)) => (P.bil p.1) p.2, continuous_toFun := ⋯ }
• P.pointwise n.succ k.succ hk = { toFun := fun (p : ↑X × ↑(Y.resolutionX (n + 1))) => (P.pointwise n k ⋯).comp ((ContinuousMap.const G p.1).prodMk p.2), continuous_toFun := ⋯ }
• P.pointwise 0 n.succ hk = absurd hk ⋯
• P.pointwise n.succ 0 hk = absurd hk ⋯

theorem TauCeti.TopPairing.pointwise_zero_apply {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) (hk : 0 = 0) (x : ↑X) (y : ↑Y) : (P.pointwise 0 0 hk) (x, y) = (P.bil x) y

@[simp]

theorem TauCeti.TopPairing.pointwise_succ_apply {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) {n k : ℕ} (hk : k + 1 = n + 1) (x : ↑X) (F : C(G, ↑(Y.resolutionX n))) (h : G) : ((P.pointwise (n + 1) (k + 1) hk) (x, F)) h = (P.pointwise n k ⋯) (x, F h)

theorem TauCeti.TopPairing.pointwise_cast {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) {n k k' : ℕ} (hk : k = n) (hk' : k' = n) (h : k = k') (p : ↑X × ↑(Y.resolutionX n)) : (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution h).hom) ((P.pointwise n k hk) p) = (P.pointwise n k' hk') p

Transport along an equality of degrees carries the pointwise pairing at one degree to the pointwise pairing at the other.

theorem TauCeti.TopPairing.pointwise_add_left {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) (n k : ℕ) (hk : k = n) (x x' : ↑X) (F : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (x + x', F) = (P.pointwise n k hk) (x, F) + (P.pointwise n k hk) (x', F)

theorem TauCeti.TopPairing.pointwise_sub_left {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) (n k : ℕ) (hk : k = n) (x x' : ↑X) (F : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (x - x', F) = (P.pointwise n k hk) (x, F) - (P.pointwise n k hk) (x', F)

theorem TauCeti.TopPairing.pointwise_smul_left {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) (n k : ℕ) (hk : k = n) (r : R) (x : ↑X) (F : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (r • x, F) = r • (P.pointwise n k hk) (x, F)

theorem TauCeti.TopPairing.pointwise_add_right {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) (n k : ℕ) (hk : k = n) (x : ↑X) (F F' : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (x, F + F') = (P.pointwise n k hk) (x, F) + (P.pointwise n k hk) (x, F')

theorem TauCeti.TopPairing.pointwise_sub_right {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) (n k : ℕ) (hk : k = n) (x : ↑X) (F F' : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (x, F - F') = (P.pointwise n k hk) (x, F) - (P.pointwise n k hk) (x, F')

theorem TauCeti.TopPairing.pointwise_smul_right {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) (n k : ℕ) (hk : k = n) (r : R) (x : ↑X) (F : ↑(Y.resolutionX n)) : (P.pointwise n k hk) (x, r • F) = r • (P.pointwise n k hk) (x, F)

theorem TauCeti.TopPairing.pointwise_ρ {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) (n k : ℕ) (hk : k = n) (g : G) (x : ↑X) (F : ↑(Y.resolutionX n)) : (P.pointwise n k hk) ((X.ρ g) x, ((Y.resolutionX n).ρ g) F) = ((Z.resolutionX k).ρ g) ((P.pointwise n k hk) (x, F))

The pointwise pairing is equivariant.

theorem TauCeti.TopPairing.d_pointwise {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) (n k : ℕ) (hk : k = n) (x : ↑X) (F : ↑(Y.resolutionX n)) : (TopRep.Hom.hom (Z.d k)) ((P.pointwise n k hk) (x, F)) = (P.pointwise (n + 1) (k + 1) ⋯) (x, (TopRep.Hom.hom (Y.d n)) F)

The pointwise pairing commutes with the differential of the resolution: the differential is natural in the coefficients, for a continuous linear map that need not be equivariant.

The Alexander–Whitney pairing on the resolution

def TauCeti.TopPairing.resolutionCup {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) (m n k : ℕ) : k = n + m → C(↑(X.resolutionX (m + 1)) × ↑(Y.resolutionX (n + 1)), ↑(Z.resolutionX (k + 1)))

The Alexander–Whitney pairing on the coinduced resolution, with explicit total degree: an element of the (m + 1)-st term of the resolution of X paired with an element of the (n + 1)-st term of the resolution of Y gives an element of the (k + 1)-st term of the resolution of Z, for k = n + m. The recursion is (a ⌣ b) g = (a g) ⌣ b, and the base case pairs the coefficient a g with every value of b g.

Equations

• One or more equations did not get rendered due to their size.
• P.resolutionCup n.succ x✝ 0 hk = absurd hk ⋯

@[simp]

theorem TauCeti.TopPairing.resolutionCup_zero_apply {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) {n k : ℕ} (hk : k = n + 0) (a : C(G, ↑X)) (b : C(G, ↑(Y.resolutionX n))) (g : G) : ((P.resolutionCup 0 n k hk) (a, b)) g = (P.pointwise n k hk) (a g, b g)

@[simp]

theorem TauCeti.TopPairing.resolutionCup_succ_apply {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) {m n k : ℕ} (hk : k + 1 = n + (m + 1)) (a : C(G, ↑(X.resolutionX (m + 1)))) (b : ↑(Y.resolutionX (n + 1))) (g : G) : ((P.resolutionCup (m + 1) n (k + 1) hk) (a, b)) g = (P.resolutionCup m n k ⋯) (a g, b)

theorem TauCeti.TopPairing.resolutionCup_cast {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) {m n k k' : ℕ} (hk : k = n + m) (hk' : k' = n + m) (h : k + 1 = k' + 1) (p : ↑(X.resolutionX (m + 1)) × ↑(Y.resolutionX (n + 1))) : (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution h).hom) ((P.resolutionCup m n k hk) p) = (P.resolutionCup m n k' hk') p

Transport along an equality of degrees carries the resolution pairing at one total degree to the resolution pairing at the other.

theorem TauCeti.TopPairing.resolutionCup_add_left {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) (m n k : ℕ) (hk : k = n + m) (a a' : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (a + a', b) = (P.resolutionCup m n k hk) (a, b) + (P.resolutionCup m n k hk) (a', b)

theorem TauCeti.TopPairing.resolutionCup_sub_left {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) (m n k : ℕ) (hk : k = n + m) (a a' : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (a - a', b) = (P.resolutionCup m n k hk) (a, b) - (P.resolutionCup m n k hk) (a', b)

theorem TauCeti.TopPairing.resolutionCup_smul_left {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) (m n k : ℕ) (hk : k = n + m) (r : R) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (r • a, b) = r • (P.resolutionCup m n k hk) (a, b)

theorem TauCeti.TopPairing.resolutionCup_add_right {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) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b b' : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (a, b + b') = (P.resolutionCup m n k hk) (a, b) + (P.resolutionCup m n k hk) (a, b')

theorem TauCeti.TopPairing.resolutionCup_smul_right {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) (m n k : ℕ) (hk : k = n + m) (r : R) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (a, r • b) = r • (P.resolutionCup m n k hk) (a, b)

theorem TauCeti.TopPairing.resolutionCup_sub_right {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) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b b' : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (a, b - b') = (P.resolutionCup m n k hk) (a, b) - (P.resolutionCup m n k hk) (a, b')

The Alexander--Whitney pairing preserves subtraction in its second argument.

theorem TauCeti.TopPairing.resolutionCup_ρ {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) (m n k : ℕ) (hk : k = n + m) (g : G) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup m n k hk) (((X.resolutionX (m + 1)).ρ g) a, ((Y.resolutionX (n + 1)).ρ g) b) = ((Z.resolutionX (k + 1)).ρ g) ((P.resolutionCup m n k hk) (a, b))

The resolution pairing is equivariant.

theorem TauCeti.TopPairing.resolutionCup_zero_d_zero {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) {n k : ℕ} (hk : k = n + 0) (x : ↑X) (b : ↑(Y.resolutionX (n + 1))) : (P.resolutionCup 0 n k hk) ((TopRep.Hom.hom (X.d 0)) x, b) = (P.pointwise (n + 1) (k + 1) ⋯) (x, b)

Pairing the constant map at x with b is the pointwise pairing of x with b.

theorem TauCeti.TopPairing.resolutionCup_leibniz {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) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (TopRep.Hom.hom (Z.d (k + 1))) ((P.resolutionCup m n k hk) (a, b)) = (P.resolutionCup (m + 1) n (k + 1) ⋯) ((TopRep.Hom.hom (X.d (m + 1))) a, b) + (-1) ^ m • (P.resolutionCup m (n + 1) (k + 1) ⋯) (a, (TopRep.Hom.hom (Y.d (n + 1))) b)

The Leibniz rule on the resolution, with the sign convention d (a ⌣ b) = d a ⌣ b + (-1)^m (a ⌣ d b) for a of degree m.

The pairing as a bilinear map into degree m + n

def TauCeti.TopPairing.resolutionCupPairing {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) (m n : ℕ) : ↑(X.resolution'X m) →ₗ[R] ↑(Y.resolution'X n) →ₗ[R] ↑(Z.resolution'X (m + n))

The Alexander–Whitney pairing on the resolution, as an R-bilinear map from the m-th and n-th terms of the shifted resolutions of X and Y to the (m + n)-th term of the shifted resolution of Z; the terms of the shifted resolution are the modules whose invariants are the homogeneous cochains.

Equations

• P.resolutionCupPairing m n = LinearMap.mk₂ R (fun (a : ↑(X.resolution'X m)) (b : ↑(Y.resolution'X n)) => (P.resolutionCup m n (m + n) ⋯) (a, b)) ⋯ ⋯ ⋯ ⋯

theorem TauCeti.TopPairing.resolutionCupPairing_apply {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) (m n : ℕ) (a : ↑(X.resolution'X m)) (b : ↑(Y.resolution'X n)) : ((P.resolutionCupPairing m n) a) b = (P.resolutionCup m n (m + n) ⋯) (a, b)

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_apply_zero {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) (n : ℕ) (a : ↑(X.resolution'X 0)) (b : ↑(Y.resolution'X n)) (g : G) : (((P.resolutionCupPairing 0 n) a) b) g = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution ⋯).hom) ((P.pointwise n n ⋯) (a g, b g))

The base case of the Alexander–Whitney recursion: a 0-cochain a cupped with b is the pointwise pairing of a g with every value of b g, transported from degree n to 0 + n.

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_apply_succ {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) (m n : ℕ) (a : ↑(X.resolution'X (m + 1))) (b : ↑(Y.resolution'X n)) (g : G) : (((P.resolutionCupPairing (m + 1) n) a) b) g = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution ⋯).hom) (((P.resolutionCupPairing m n) (a g)) b)

The successor case of the Alexander–Whitney recursion: (a ⌣ b) g = (a g) ⌣ b, transported from degree m + n + 1 to m + 1 + n.

The Alexander–Whitney pairing evaluated in low bidegrees

In each bidegree (m, n) with m + n ≤ 2 the recursion unfolds to the Alexander–Whitney formula (a ⌣ b) (g₀, …, g_{m+n}) = μ (a (g₀, …, g_m)) (b (g_m, …, g_{m+n})). The transports along the degree equalities 0 + n = n and m + n + 1 = m + 1 + n are between the same numeral, so HomologicalComplex.XIsoOfEq_rfl turns each into the identity morphism, which TopRep.hom_id and ContIntertwiningMap.id_apply remove.

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_zero_zero_apply {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 : ↑(X.resolution'X 0)) (b : ↑(Y.resolution'X 0)) (g : G) : (((P.resolutionCupPairing 0 0) a) b) g = (P.bil (a g)) (b g)

The Alexander–Whitney pairing of two degree-zero elements of the resolution, evaluated: (a ⌣ b) g = μ (a g) (b g).

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_zero_one_apply {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 : ↑(X.resolution'X 0)) (b : ↑(Y.resolution'X 1)) (g₀ g₁ : G) : ((((P.resolutionCupPairing 0 1) a) b) g₀) g₁ = (P.bil (a g₀)) ((b g₀) g₁)

The Alexander–Whitney pairing of a degree-zero and a degree-one element of the resolution, evaluated: (a ⌣ b) g₀ g₁ = μ (a g₀) (b g₀ g₁).

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_zero_two_apply {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 : ↑(X.resolution'X 0)) (b : ↑(Y.resolution'X 2)) (g₀ g₁ g₂ : G) : (((((P.resolutionCupPairing 0 2) a) b) g₀) g₁) g₂ = (P.bil (a g₀)) (((b g₀) g₁) g₂)

The Alexander–Whitney pairing of a degree-zero and a degree-two element of the resolution, evaluated: (a ⌣ b) g₀ g₁ g₂ = μ (a g₀) (b g₀ g₁ g₂).

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_one_zero_apply {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 : ↑(X.resolution'X 1)) (b : ↑(Y.resolution'X 0)) (g₀ g₁ : G) : ((((P.resolutionCupPairing 1 0) a) b) g₀) g₁ = (P.bil ((a g₀) g₁)) (b g₁)

The Alexander–Whitney pairing of a degree-one and a degree-zero element of the resolution, evaluated: (a ⌣ b) g₀ g₁ = μ (a g₀ g₁) (b g₁).

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_two_zero_apply {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 : ↑(X.resolution'X 2)) (b : ↑(Y.resolution'X 0)) (g₀ g₁ g₂ : G) : (((((P.resolutionCupPairing 2 0) a) b) g₀) g₁) g₂ = (P.bil (((a g₀) g₁) g₂)) (b g₂)

The Alexander–Whitney pairing of a degree-two and a degree-zero element of the resolution, evaluated: (a ⌣ b) g₀ g₁ g₂ = μ (a g₀ g₁ g₂) (b g₂).

@[simp]

theorem TauCeti.TopPairing.resolutionCupPairing_one_one_apply {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 : ↑(X.resolution'X 1)) (b : ↑(Y.resolution'X 1)) (g₀ g₁ g₂ : G) : (((((P.resolutionCupPairing 1 1) a) b) g₀) g₁) g₂ = (P.bil ((a g₀) g₁)) ((b g₁) g₂)

The Alexander–Whitney pairing of two degree-one elements of the resolution, evaluated: (a ⌣ b) g₀ g₁ g₂ = μ (a g₀ g₁) (b g₁ g₂).

theorem TauCeti.TopPairing.continuous_resolutionCupPairing {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) (m n : ℕ) : Continuous fun (p : ↑(X.resolution'X m) × ↑(Y.resolution'X n)) => ((P.resolutionCupPairing m n) p.1) p.2

The resolution pairing is jointly continuous.

theorem TauCeti.TopPairing.resolutionCupPairing_ρ {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) (m n : ℕ) (g : G) (a : ↑(X.resolution'X m)) (b : ↑(Y.resolution'X n)) : ((P.resolutionCupPairing m n) (((X.resolution'X m).ρ g) a)) (((Y.resolution'X n).ρ g) b) = ((Z.resolution'X (m + n)).ρ g) (((P.resolutionCupPairing m n) a) b)

The resolution pairing is equivariant.

theorem TauCeti.TopPairing.resolutionCupPairing_leibniz {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) (m n : ℕ) (a : ↑(X.resolution'X m)) (b : ↑(Y.resolution'X n)) : (TopRep.Hom.hom (Z.d (m + n + 1))) (((P.resolutionCupPairing m n) a) b) = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution ⋯).hom) (((P.resolutionCupPairing (m + 1) n) ((TopRep.Hom.hom (X.d (m + 1))) a)) b) + (-1) ^ m • ((P.resolutionCupPairing m (n + 1)) a) ((TopRep.Hom.hom (Y.d (n + 1))) b)

The Leibniz rule on the resolution, in degree m + n: the term d a ⌣ b lives in degree m + 1 + n and is transported to m + n + 1.

The cup product of homogeneous cochains

def TauCeti.TopPairing.cupCochain {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) (m n : ℕ) : ↑(X.homogeneousCochains.X m).toModuleCat →ₗ[R] ↑(Y.homogeneousCochains.X n).toModuleCat →ₗ[R] ↑(Z.homogeneousCochains.X (m + n)).toModuleCat

The cup product of homogeneous cochains: the Alexander–Whitney pairing restricted to the G-invariant elements, which it preserves by equivariance.

Equations

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

theorem TauCeti.TopPairing.coe_cupCochain {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) (m n : ℕ) (a : ↑(X.homogeneousCochains.X m).toModuleCat) (b : ↑(Y.homogeneousCochains.X n).toModuleCat) : ↑(((P.cupCochain m n) a) b) = ((P.resolutionCupPairing m n) ↑a) ↑b

The underlying resolution element of a cup product of homogeneous cochains is the Alexander–Whitney pairing of the underlying elements.

theorem TauCeti.TopPairing.cupCochain_one_one_apply {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 : ↑(X.homogeneousCochains.X 1).toModuleCat) (b : ↑(Y.homogeneousCochains.X 1).toModuleCat) (g₀ g₁ g₂ : G) : ((↑(((P.cupCochain 1 1) a) b) g₀) g₁) g₂ = (P.bil ((↑a g₀) g₁)) ((↑b g₁) g₂)

The cup product of two homogeneous one-cochains, evaluated: (a ⌣ b) g₀ g₁ g₂ = μ (a g₀ g₁) (b g₁ g₂).

theorem TauCeti.TopPairing.cupCochain_leibniz {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) (m n : ℕ) (a : ↑(X.homogeneousCochains.X m).toModuleCat) (b : ↑(Y.homogeneousCochains.X n).toModuleCat) : (TopModuleCat.Hom.hom (Z.homogeneousCochains.d (m + n) (m + n + 1))) (((P.cupCochain m n) a) b) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq Z.homogeneousCochains ⋯).hom) (((P.cupCochain (m + 1) n) ((TopModuleCat.Hom.hom (X.homogeneousCochains.d m (m + 1))) a)) b) + (-1) ^ m • ((P.cupCochain m (n + 1)) a) ((TopModuleCat.Hom.hom (Y.homogeneousCochains.d n (n + 1))) b)

The Leibniz rule for the cup product of homogeneous cochains, d (a ⌣ b) = d a ⌣ b + (-1)^m (a ⌣ d b), where the term d a ⌣ b lives in degree m + 1 + n and is transported to m + n + 1.