The connecting maps and the explicit low-degree cup products

The Leibniz rule δ (x ⌣ y) = δ x ⌣ y + (-1)^p (x ⌣ δ y) is not a statement until one says which short exact sequences of coefficients the two connecting maps belong to, and how the pairing relates them. Cupping with a fixed class in the second variable and cupping with a fixed class in the first variable are two different constructions, each attached to a short exact sequence in its own variable, so this file proves two families of identities rather than one sum rule.

In the first variable the input is a short exact sequence 0 → A' → A → A'' → 0 of discrete G-modules, a topological G-module B, a short exact sequence 0 → C' → C → C'' → 0, and three G-equivariant biadditive pairings

μ  : A  →+ B →+ C,      μ' : A' →+ B →+ C',      μ'' : A'' →+ B →+ C''

with μ (incl a') b = incl (μ' a' b) and μ'' (proj a) b = proj (μ a b), that is a map of short exact sequences after pairing with B. For x ∈ H^p(G, A'') and y ∈ H^q(G, B) the identity is

δ (x ⌣ y) = δ x ⌣ y     in H^{p+q+1}(G, C').

In the second variable the sequence is 0 → B' → B → B'' → 0, the fixed module is A, the pairings are μ : A →+ B →+ C, μ' : A →+ B' →+ C' and μ'' : A →+ B'' →+ C'', and for x ∈ H^p(G, A) and y ∈ H^q(G, B'') the identity carries the sign of the degree it moves past:

δ (x ⌣ y) = (-1)^p (x ⌣ δ y)   in H^{p+q+1}(G, C').

Six instances have all three of p, q and p + q + 1 at most 2, so six theorems exhaust what the low-degree model can state.

The third family moves a connecting map from one variable to the other. Its input is a pair of short exact sequences 0 → A₁ → A → A₂ → 0 and 0 → B₂ → B → B₁ → 0 of discrete G-modules, compatibly paired into one topological G-module C by μ : A →+ B →+ C, μ₁ : A₁ →+ B₁ →+ C and μ₂ : A₂ →+ B₂ →+ C with

μ (incl a₁) b = μ₁ a₁ (proj b),      μ a (incl b₂) = μ₂ (proj a) b₂,

so that the sub-object A₁ is orthogonal to the sub-object B₂ and pairs with the quotient B₁, while the quotient A₂ pairs with the sub-object B₂. No nondegeneracy is assumed; the motivating instance is a short exact sequence and its dual sequence under an evaluation pairing. For x ∈ H^p(G, A₂) and y ∈ H^q(G, B₁) the two connecting maps are adjoint up to the Leibniz sign:

δ x ⌣ y = (-1)^(p+1) (x ⌣ δ y)   in H^{p+q+1}(G, C),

because δ x ⌣ y + (-1)^p (x ⌣ δ y) is the coboundary of the cup of lifts. Three bidegrees have p + q + 1 ≤ 2, so three theorems exhaust this family too. These are the identities that make the duality maps H^i(G, M) → H^{2-i}(G, M')^∨ of a Demushkin group commute with the long exact sequences, the step of Tate's argument that Serre records.

Main statements

• TauCeti.ContCohomology.explicitDelta0_explicitCup00_left, explicitDelta1_explicitCup01_left and explicitDelta1_explicitCup10_left: the three first-variable identities, in bidegrees (0,0), (0,1) and (1,0).
• TauCeti.ContCohomology.explicitDelta0_explicitCup00_right, explicitDelta1_explicitCup01_right and explicitDelta1_explicitCup10_right: the three second-variable identities, in bidegrees (0,0), (0,1) and (1,0), the last with its sign.
• TauCeti.ContCohomology.explicitCup10_explicitDelta0_eq_neg_explicitCup01_explicitDelta0, explicitCup11_explicitDelta0_eq_neg_explicitCup02_explicitDelta1 and explicitCup20_explicitDelta1_eq_explicitCup11_explicitDelta0: the three adjointness identities for a pair of compatibly paired short exact sequences, in bidegrees (0,0), (0,1) and (1,0).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.4.3) and (1.4.5): the compatibility of the cup product with the connecting homomorphisms.
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I §0, the cup-product properties (0.1.1)-(0.1.6), stated with the same sign conventions.
• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.1: Tate's duality argument, which uses the adjointness identities to compare the long exact sequences of a finite module and of its dual.

theorem TauCeti.ContCohomology.explicitDelta0_explicitCup00_left {G : Type u_1} [Group G] [TopologicalSpace G] {A' : Type u_2} [AddCommGroup A'] [TopologicalSpace A'] [DiscreteTopology A'] [DistribMulAction G A'] [ContinuousSMul G A'] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {A'' : Type u_4} [AddCommGroup A''] [TopologicalSpace A''] [DiscreteTopology A''] [DistribMulAction G A''] {B : Type u_5} [AddCommGroup B] [TopologicalSpace B] [DistribMulAction G B] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] (SA : DiscreteShortExact G A' A A'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A' →+ B →+ C') (μ'' : A'' →+ B →+ C'') (hμ' : Continuous fun (p : A' × B) => (μ' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A') (b : B), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A'') (b : B), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A') (b : B), (μ (SA.incl a)) b = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' (SA.proj a)) b = SC.proj ((μ a) b)) (x : ↥(H0 G A'')) (y : ↥(H0 G B)) : SC.explicitDelta0 (((explicitCup00 G A'' B C'' μ'' hequiv'') x) y) = ((explicitCup10 G A' B C' μ' hμ' hequiv') (SA.explicitDelta0 x)) y

δ⁰ passes through the (0,0) cup in the first variable. For an invariant x of A'' and an invariant y of B, the class δ⁰ (x ⌣ y) ∈ H¹(G, C') is δ⁰ x ⌣ y, the (1,0) cup against the pairing μ' of the sub-objects.

theorem TauCeti.ContCohomology.explicitDelta1_explicitCup01_left {G : Type u_1} [Group G] [TopologicalSpace G] {A' : Type u_2} [AddCommGroup A'] [TopologicalSpace A'] [DiscreteTopology A'] [DistribMulAction G A'] [ContinuousSMul G A'] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {A'' : Type u_4} [AddCommGroup A''] [TopologicalSpace A''] [DiscreteTopology A''] [DistribMulAction G A''] {B : Type u_5} [AddCommGroup B] [TopologicalSpace B] [IsTopologicalAddGroup B] [DistribMulAction G B] [ContinuousSMul G B] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] [ContinuousSMul G C''] (SA : DiscreteShortExact G A' A A'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A' →+ B →+ C') (μ'' : A'' →+ B →+ C'') (hμ : Continuous fun (p : A × B) => (μ p.1) p.2) (hμ' : Continuous fun (p : A' × B) => (μ' p.1) p.2) (hμ'' : Continuous fun (p : A'' × B) => (μ'' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A') (b : B), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A'') (b : B), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A') (b : B), (μ (SA.incl a)) b = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' (SA.proj a)) b = SC.proj ((μ a) b)) [ContinuousMul G] (x : ↥(H0 G A'')) (y : H1 G B) : SC.explicitDelta1 (((explicitCup01 G A'' B C'' μ'' hμ'' hequiv'') x) y) = ((explicitCup11 G A' B C' μ' hμ' hequiv') (SA.explicitDelta0 x)) y

δ¹ passes through the (0,1) cup in the first variable. For an invariant x of A'' and a class y ∈ H¹(G, B), the class δ¹ (x ⌣ y) ∈ H²(G, C') is the (1,1) cup δ⁰ x ⌣ y.

theorem TauCeti.ContCohomology.explicitDelta1_explicitCup10_left {G : Type u_1} [Group G] [TopologicalSpace G] {A' : Type u_2} [AddCommGroup A'] [TopologicalSpace A'] [DiscreteTopology A'] [DistribMulAction G A'] [ContinuousSMul G A'] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] [ContinuousSMul G A] {A'' : Type u_4} [AddCommGroup A''] [TopologicalSpace A''] [DiscreteTopology A''] [DistribMulAction G A''] [ContinuousSMul G A''] {B : Type u_5} [AddCommGroup B] [TopologicalSpace B] [DistribMulAction G B] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] [ContinuousSMul G C''] (SA : DiscreteShortExact G A' A A'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A' →+ B →+ C') (μ'' : A'' →+ B →+ C'') (hμ' : Continuous fun (p : A' × B) => (μ' p.1) p.2) (hμ'' : Continuous fun (p : A'' × B) => (μ'' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A') (b : B), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A'') (b : B), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A') (b : B), (μ (SA.incl a)) b = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' (SA.proj a)) b = SC.proj ((μ a) b)) [ContinuousMul G] (x : H1 G A'') (y : ↥(H0 G B)) : SC.explicitDelta1 (((explicitCup10 G A'' B C'' μ'' hμ'' hequiv'') x) y) = ((explicitCup20 G A' B C' μ' hμ' hequiv') (SA.explicitDelta1 x)) y

δ¹ passes through the (1,0) cup in the first variable. For a class x ∈ H¹(G, A'') and an invariant y of B, the class δ¹ (x ⌣ y) ∈ H²(G, C') is the (2,0) cup δ¹ x ⌣ y.

theorem TauCeti.ContCohomology.explicitDelta0_explicitCup00_right {G : Type u_1} [Group G] [TopologicalSpace G] {A : Type u_2} [AddCommGroup A] [TopologicalSpace A] [DistribMulAction G A] {B' : Type u_3} [AddCommGroup B'] [TopologicalSpace B'] [DiscreteTopology B'] [DistribMulAction G B'] [ContinuousSMul G B'] {B : Type u_4} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {B'' : Type u_5} [AddCommGroup B''] [TopologicalSpace B''] [DiscreteTopology B''] [DistribMulAction G B''] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] (SB : DiscreteShortExact G B' B B'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A →+ B' →+ C') (μ'' : A →+ B'' →+ C'') (hμ' : Continuous fun (p : A × B') => (μ' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A) (b : B'), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A) (b : B''), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A) (b : B'), (μ a) (SB.incl b) = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' a) (SB.proj b) = SC.proj ((μ a) b)) (x : ↥(H0 G A)) (y : ↥(H0 G B'')) : SC.explicitDelta0 (((explicitCup00 G A B'' C'' μ'' hequiv'') x) y) = ((explicitCup01 G A B' C' μ' hμ' hequiv') x) (SB.explicitDelta0 y)

δ⁰ passes through the (0,0) cup in the second variable. For an invariant x of A and an invariant y of B'', the class δ⁰ (x ⌣ y) ∈ H¹(G, C') is the (0,1) cup x ⌣ δ⁰ y; the sign (-1)^p is 1 because x has degree 0.

theorem TauCeti.ContCohomology.explicitDelta1_explicitCup01_right {G : Type u_1} [Group G] [TopologicalSpace G] {A : Type u_2} [AddCommGroup A] [TopologicalSpace A] [DistribMulAction G A] {B' : Type u_3} [AddCommGroup B'] [TopologicalSpace B'] [DiscreteTopology B'] [DistribMulAction G B'] [ContinuousSMul G B'] {B : Type u_4} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {B'' : Type u_5} [AddCommGroup B''] [TopologicalSpace B''] [DiscreteTopology B''] [DistribMulAction G B''] [ContinuousSMul G B''] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] [ContinuousSMul G C''] (SB : DiscreteShortExact G B' B B'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A →+ B' →+ C') (μ'' : A →+ B'' →+ C'') (hμ' : Continuous fun (p : A × B') => (μ' p.1) p.2) (hμ'' : Continuous fun (p : A × B'') => (μ'' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A) (b : B'), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A) (b : B''), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A) (b : B'), (μ a) (SB.incl b) = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' a) (SB.proj b) = SC.proj ((μ a) b)) [ContinuousMul G] (x : ↥(H0 G A)) (y : H1 G B'') : SC.explicitDelta1 (((explicitCup01 G A B'' C'' μ'' hμ'' hequiv'') x) y) = ((explicitCup02 G A B' C' μ' hμ' hequiv') x) (SB.explicitDelta1 y)

δ¹ passes through the (0,1) cup in the second variable. For an invariant x of A and a class y ∈ H¹(G, B''), the class δ¹ (x ⌣ y) ∈ H²(G, C') is the (0,2) cup x ⌣ δ¹ y.

theorem TauCeti.ContCohomology.explicitDelta1_explicitCup10_right {G : Type u_1} [Group G] [TopologicalSpace G] {A : Type u_2} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] {B' : Type u_3} [AddCommGroup B'] [TopologicalSpace B'] [DiscreteTopology B'] [DistribMulAction G B'] [ContinuousSMul G B'] {B : Type u_4} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {B'' : Type u_5} [AddCommGroup B''] [TopologicalSpace B''] [DiscreteTopology B''] [DistribMulAction G B''] {C' : Type u_6} [AddCommGroup C'] [TopologicalSpace C'] [DiscreteTopology C'] [DistribMulAction G C'] [ContinuousSMul G C'] {C : Type u_7} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] {C'' : Type u_8} [AddCommGroup C''] [TopologicalSpace C''] [DiscreteTopology C''] [DistribMulAction G C''] [ContinuousSMul G C''] (SB : DiscreteShortExact G B' B B'') (SC : DiscreteShortExact G C' C C'') (μ : A →+ B →+ C) (μ' : A →+ B' →+ C') (μ'' : A →+ B'' →+ C'') (hμ : Continuous fun (p : A × B) => (μ p.1) p.2) (hμ' : Continuous fun (p : A × B') => (μ' p.1) p.2) (hμ'' : Continuous fun (p : A × B'') => (μ'' p.1) p.2) (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (hequiv' : ∀ (g : G) (a : A) (b : B'), (μ' (g • a)) (g • b) = g • (μ' a) b) (hequiv'' : ∀ (g : G) (a : A) (b : B''), (μ'' (g • a)) (g • b) = g • (μ'' a) b) (hincl : ∀ (a : A) (b : B'), (μ a) (SB.incl b) = SC.incl ((μ' a) b)) (hproj : ∀ (a : A) (b : B), (μ'' a) (SB.proj b) = SC.proj ((μ a) b)) [ContinuousMul G] (x : H1 G A) (y : ↥(H0 G B'')) : SC.explicitDelta1 (((explicitCup10 G A B'' C'' μ'' hμ'' hequiv'') x) y) = -((explicitCup11 G A B' C' μ' hμ' hequiv') x) (SB.explicitDelta0 y)

δ¹ passes through the (1,0) cup in the second variable, with a sign. For a class x ∈ H¹(G, A) and an invariant y of B'', the class δ¹ (x ⌣ y) ∈ H²(G, C') is -(x ⌣ δ⁰ y), the sign (-1)^p at p = 1.

A pair of compatibly paired short exact sequences

The connecting maps of 0 → A₁ → A → A₂ → 0 and of 0 → B₂ → B → B₁ → 0 are adjoint under pairings that make A₁ orthogonal to B₂. Every coefficient module of the two sequences is discrete here, so the joint continuity of each pairing is automatic and is not taken as a hypothesis, and the equivariance of μ₁ and μ₂ follows from that of μ through the two compatibilities, so only μ is assumed equivariant; the common target C is any topological G-module.

theorem TauCeti.ContCohomology.equivariant_of_incl {G : Type u_1} [Group G] {A₁ : Type u_2} [AddCommGroup A₁] [TopologicalSpace A₁] [DiscreteTopology A₁] [DistribMulAction G A₁] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {A₂ : Type u_4} [AddCommGroup A₂] [TopologicalSpace A₂] [DiscreteTopology A₂] [DistribMulAction G A₂] {B₂ : Type u_5} [AddCommGroup B₂] [TopologicalSpace B₂] [DiscreteTopology B₂] [DistribMulAction G B₂] {B : Type u_6} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {B₁ : Type u_7} [AddCommGroup B₁] [TopologicalSpace B₁] [DiscreteTopology B₁] [DistribMulAction G B₁] {C : Type u_8} [AddCommGroup C] (SA : DiscreteShortExact G A₁ A A₂) (SB : DiscreteShortExact G B₂ B B₁) (μ : A →+ B →+ C) (μ₁ : A₁ →+ B₁ →+ C) (hincl : ∀ (a : A₁) (b : B), (μ (SA.incl a)) b = (μ₁ a) (SB.proj b)) [DistribMulAction G C] (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (g : G) (a : A₁) (b : B₁) : (μ₁ (g • a)) (g • b) = g • (μ₁ a) b

The pairing of the sub-object A₁ with the quotient B₁ is equivariant. Lift b to B and read μ₁ through μ on SA.incl a.

theorem TauCeti.ContCohomology.equivariant_of_proj {G : Type u_1} [Group G] {A₁ : Type u_2} [AddCommGroup A₁] [TopologicalSpace A₁] [DiscreteTopology A₁] [DistribMulAction G A₁] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {A₂ : Type u_4} [AddCommGroup A₂] [TopologicalSpace A₂] [DiscreteTopology A₂] [DistribMulAction G A₂] {B₂ : Type u_5} [AddCommGroup B₂] [TopologicalSpace B₂] [DiscreteTopology B₂] [DistribMulAction G B₂] {B : Type u_6} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {B₁ : Type u_7} [AddCommGroup B₁] [TopologicalSpace B₁] [DiscreteTopology B₁] [DistribMulAction G B₁] {C : Type u_8} [AddCommGroup C] (SA : DiscreteShortExact G A₁ A A₂) (SB : DiscreteShortExact G B₂ B B₁) (μ : A →+ B →+ C) (μ₂ : A₂ →+ B₂ →+ C) (hproj : ∀ (a : A) (b : B₂), (μ a) (SB.incl b) = (μ₂ (SA.proj a)) b) [DistribMulAction G C] (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) (g : G) (a : A₂) (b : B₂) : (μ₂ (g • a)) (g • b) = g • (μ₂ a) b

The pairing of the quotient A₂ with the sub-object B₂ is equivariant. Lift a to A and read μ₂ through μ on SB.incl b.

theorem TauCeti.ContCohomology.explicitCup10_explicitDelta0_eq_neg_explicitCup01_explicitDelta0 {G : Type u_1} [Group G] {A₁ : Type u_2} [AddCommGroup A₁] [TopologicalSpace A₁] [DiscreteTopology A₁] [DistribMulAction G A₁] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {A₂ : Type u_4} [AddCommGroup A₂] [TopologicalSpace A₂] [DiscreteTopology A₂] [DistribMulAction G A₂] {B₂ : Type u_5} [AddCommGroup B₂] [TopologicalSpace B₂] [DiscreteTopology B₂] [DistribMulAction G B₂] {B : Type u_6} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {B₁ : Type u_7} [AddCommGroup B₁] [TopologicalSpace B₁] [DiscreteTopology B₁] [DistribMulAction G B₁] {C : Type u_8} [AddCommGroup C] (SA : DiscreteShortExact G A₁ A A₂) (SB : DiscreteShortExact G B₂ B B₁) (μ : A →+ B →+ C) (μ₁ : A₁ →+ B₁ →+ C) (μ₂ : A₂ →+ B₂ →+ C) (hincl : ∀ (a : A₁) (b : B), (μ (SA.incl a)) b = (μ₁ a) (SB.proj b)) (hproj : ∀ (a : A) (b : B₂), (μ a) (SB.incl b) = (μ₂ (SA.proj a)) b) [DistribMulAction G C] (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) [TopologicalSpace G] [ContinuousSMul G A₁] [ContinuousSMul G A] [ContinuousSMul G B₂] [ContinuousSMul G B] [TopologicalSpace C] [IsTopologicalAddGroup C] [ContinuousSMul G C] (x : ↥(H0 G A₂)) (y : ↥(H0 G B₁)) : ((explicitCup10 G A₁ B₁ C μ₁ ⋯ ⋯) (SA.explicitDelta0 x)) y = -((explicitCup01 G A₂ B₂ C μ₂ ⋯ ⋯) x) (SB.explicitDelta0 y)

The two δ⁰ are anti-adjoint under the (1,0) and (0,1) cups. For invariants x of A₂ and y of B₁, the class δ⁰ x ⌣ y ∈ H¹(G, C) is -(x ⌣ δ⁰ y).

theorem TauCeti.ContCohomology.explicitCup11_explicitDelta0_eq_neg_explicitCup02_explicitDelta1 {G : Type u_1} [Group G] {A₁ : Type u_2} [AddCommGroup A₁] [TopologicalSpace A₁] [DiscreteTopology A₁] [DistribMulAction G A₁] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {A₂ : Type u_4} [AddCommGroup A₂] [TopologicalSpace A₂] [DiscreteTopology A₂] [DistribMulAction G A₂] {B₂ : Type u_5} [AddCommGroup B₂] [TopologicalSpace B₂] [DiscreteTopology B₂] [DistribMulAction G B₂] {B : Type u_6} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {B₁ : Type u_7} [AddCommGroup B₁] [TopologicalSpace B₁] [DiscreteTopology B₁] [DistribMulAction G B₁] {C : Type u_8} [AddCommGroup C] (SA : DiscreteShortExact G A₁ A A₂) (SB : DiscreteShortExact G B₂ B B₁) (μ : A →+ B →+ C) (μ₁ : A₁ →+ B₁ →+ C) (μ₂ : A₂ →+ B₂ →+ C) (hincl : ∀ (a : A₁) (b : B), (μ (SA.incl a)) b = (μ₁ a) (SB.proj b)) (hproj : ∀ (a : A) (b : B₂), (μ a) (SB.incl b) = (μ₂ (SA.proj a)) b) [DistribMulAction G C] (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) [TopologicalSpace G] [ContinuousSMul G A₁] [ContinuousSMul G A] [ContinuousSMul G B₂] [ContinuousSMul G B] [ContinuousSMul G B₁] [TopologicalSpace C] [IsTopologicalAddGroup C] [ContinuousSMul G C] [ContinuousMul G] (x : ↥(H0 G A₂)) (y : H1 G B₁) : ((explicitCup11 G A₁ B₁ C μ₁ ⋯ ⋯) (SA.explicitDelta0 x)) y = -((explicitCup02 G A₂ B₂ C μ₂ ⋯ ⋯) x) (SB.explicitDelta1 y)

δ⁰ and δ¹ are anti-adjoint under the (1,1) and (0,2) cups. For an invariant x of A₂ and a class y ∈ H¹(G, B₁), the class δ⁰ x ⌣ y ∈ H²(G, C) is -(x ⌣ δ¹ y).

theorem TauCeti.ContCohomology.explicitCup20_explicitDelta1_eq_explicitCup11_explicitDelta0 {G : Type u_1} [Group G] {A₁ : Type u_2} [AddCommGroup A₁] [TopologicalSpace A₁] [DiscreteTopology A₁] [DistribMulAction G A₁] {A : Type u_3} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {A₂ : Type u_4} [AddCommGroup A₂] [TopologicalSpace A₂] [DiscreteTopology A₂] [DistribMulAction G A₂] {B₂ : Type u_5} [AddCommGroup B₂] [TopologicalSpace B₂] [DiscreteTopology B₂] [DistribMulAction G B₂] {B : Type u_6} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {B₁ : Type u_7} [AddCommGroup B₁] [TopologicalSpace B₁] [DiscreteTopology B₁] [DistribMulAction G B₁] {C : Type u_8} [AddCommGroup C] (SA : DiscreteShortExact G A₁ A A₂) (SB : DiscreteShortExact G B₂ B B₁) (μ : A →+ B →+ C) (μ₁ : A₁ →+ B₁ →+ C) (μ₂ : A₂ →+ B₂ →+ C) (hincl : ∀ (a : A₁) (b : B), (μ (SA.incl a)) b = (μ₁ a) (SB.proj b)) (hproj : ∀ (a : A) (b : B₂), (μ a) (SB.incl b) = (μ₂ (SA.proj a)) b) [DistribMulAction G C] (hequiv : ∀ (g : G) (a : A) (b : B), (μ (g • a)) (g • b) = g • (μ a) b) [TopologicalSpace G] [ContinuousSMul G A₁] [ContinuousSMul G A] [ContinuousSMul G A₂] [ContinuousSMul G B₂] [ContinuousSMul G B] [TopologicalSpace C] [IsTopologicalAddGroup C] [ContinuousSMul G C] [ContinuousMul G] (x : H1 G A₂) (y : ↥(H0 G B₁)) : ((explicitCup20 G A₁ B₁ C μ₁ ⋯ ⋯) (SA.explicitDelta1 x)) y = ((explicitCup11 G A₂ B₂ C μ₂ ⋯ ⋯) x) (SB.explicitDelta0 y)

δ¹ and δ⁰ are adjoint under the (2,0) and (1,1) cups. For a class x ∈ H¹(G, A₂) and an invariant y of B₁, the class δ¹ x ⌣ y ∈ H²(G, C) is x ⌣ δ⁰ y; the sign (-1)^(p+1) is 1 because x has degree 1.