Cup products in continuous cohomology (degrees ≤ 2) #
Cup products relative to a G-equivariant biadditive pairing μ : M →+ N →+ P, in the three
shapes needed by the literature axioms (B3 Demushkin, B6 local Tate duality):
cup11 : H¹(G,M) →+ H¹(G,N) →+ H²(G,P)— the(1,1)cup,(a ∪ b)(g,h) = μ (a g) (g • b h);cup02 : H⁰(G,M) →+ H²(G,N) →+ H²(G,P)—(a ∪ b)(g,h) = μ a (b (g,h));cup20 : H²(G,M) →+ H⁰(G,N) →+ H²(G,P)—(a ∪ b)(g,h) = μ (a (g,h)) ((g·h) • b).
Design. Coefficient modules M, N are taken discrete (the finite discrete setting of the
axioms), which makes every cup cochain continuous with no continuity hypothesis on μ. The maps
are built by descending explicit cochain formulas through cohomology; the bundling into
→+ →+ makes them bilinear by construction (acceptance criterion), and ∪ 0 = 0 / 0 ∪ = 0
are then map_zero. Coefficient naturality is cup11_mapCoeff_right etc.
The (1,1) cup is the one B3 needs (nondegeneracy of H¹ × H¹ → H²); (0,2)/(2,0) feed B6's
H^i × H^{2-i} → H² pairing. Everything is proved from the explicit mem_Z1_iff/mem_Z2_iff
cocycle identities of GQ2/Cohomology.lean; #print axioms stays the standard three.
The (1,1) cup product #
def
GQ2.ContCoh.cup11Fun
{G : Type u_1}
[Group G]
{M : Type u_2}
[AddCommGroup M]
{N : Type u_3}
[AddCommGroup N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
(μ : M →+ N →+ P)
(a : G → M)
(b : G → N)
:
G × G → P
The (1,1)-cup cochain (a ∪ b)(g,h) = μ (a g) (g • b h).
Equations
- GQ2.ContCoh.cup11Fun μ a b p = (μ (a p.1)) (p.1 • b p.2)
Instances For
theorem
GQ2.ContCoh.continuous_pairing
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
(μ : M →+ N →+ P)
{α : Type u_5}
[TopologicalSpace α]
{u : α → M}
{v : α → N}
(hu : Continuous u)
(hv : Continuous v)
:
Continuous fun (x : α) => (μ (u x)) (v x)
A product-of-values map into P out of two continuous maps into the discrete modules
M, N is continuous (the pairing is automatically continuous since M × N is discrete).
theorem
GQ2.ContCoh.cup11_mem_Z2
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(a : ↥(Z1 G M))
(b : ↥(Z1 G N))
:
Cup of cocycles is a cocycle: the key 2-cocycle identity for (1,1).
def
GQ2.ContCoh.cup11ZH
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (1,1) cup, bundled biadditively at the cocycle level and post-composed with the class
map Z² → H².
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
GQ2.ContCoh.cup11_bcobound
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(a : ↥(Z1 G M))
{c : G → N}
(hc : c ∈ B1 G N)
:
Descent, right variable: if the N-cocycle is a coboundary, the cup is a coboundary
(uses that the M-argument is a cocycle).
theorem
GQ2.ContCoh.cup11_acobound
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
{c : G → M}
(hc : c ∈ B1 G M)
(b : ↥(Z1 G N))
:
Descent, left variable: if the M-cocycle is a coboundary, the cup is a coboundary
(uses that the N-argument is a cocycle).
noncomputable def
GQ2.ContCoh.cup11
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (1,1) cup product H¹(G,M) →+ H¹(G,N) →+ H²(G,P), bilinear by construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
GQ2.ContCoh.cup11_mk_mk
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(a : ↥(Z1 G M))
(b : ↥(Z1 G N))
:
@[simp]
theorem
GQ2.ContCoh.cup11_zero_left
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(y : H1 G N)
:
((cup11 μ hμ) 0) y = 0
The (0,2) cup product #
def
GQ2.ContCoh.cup02Fun
{G : Type u_1}
{M : Type u_2}
[AddCommGroup M]
{N : Type u_3}
[AddCommGroup N]
{P : Type u_4}
[AddCommGroup P]
(μ : M →+ N →+ P)
(m : M)
(b : G × G → N)
:
G × G → P
The (0,2)-cup cochain (a ∪ b)(g,h) = μ a (b (g,h)).
Equations
- GQ2.ContCoh.cup02Fun μ m b p = (μ m) (b p)
Instances For
theorem
GQ2.ContCoh.cup02_mem_Z2
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(m : ↥(H0 G M))
(b : ↥(Z2 G N))
:
Cup of an invariant with a 2-cocycle is a 2-cocycle.
theorem
GQ2.ContCoh.cup02_bcobound
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(m : ↥(H0 G M))
{c : G × G → N}
(hc : c ∈ B2 G N)
:
Descent for (0,2): cup with a coboundary is a coboundary.
def
GQ2.ContCoh.cup02FlipZH
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (0,2) cup, bundled biadditively at the cocycle level (Z²-slot first, so that it can be
descended with a single QuotientAddGroup.lift; the final order is fixed by flip).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
GQ2.ContCoh.cup02
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (0,2) cup product H⁰(G,M) →+ H²(G,N) →+ H²(G,P).
Equations
- GQ2.ContCoh.cup02 μ hμ = (QuotientAddGroup.lift ((GQ2.ContCoh.B2 G N).addSubgroupOf (GQ2.ContCoh.Z2 G N)) (GQ2.ContCoh.cup02FlipZH μ hμ) ⋯).flip
Instances For
The (2,0) cup product #
def
GQ2.ContCoh.cup20Fun
{G : Type u_1}
[Group G]
{M : Type u_2}
[AddCommGroup M]
{N : Type u_3}
[AddCommGroup N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
(μ : M →+ N →+ P)
(a : G × G → M)
(n : N)
:
G × G → P
The (2,0)-cup cochain (a ∪ b)(g,h) = μ (a (g,h)) ((g·h) • b).
Equations
- GQ2.ContCoh.cup20Fun μ a n p = (μ (a p)) ((p.1 * p.2) • n)
Instances For
theorem
GQ2.ContCoh.cup20_mem_Z2
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
(a : ↥(Z2 G M))
(n : ↥(H0 G N))
:
Cup of a 2-cocycle with an invariant is a 2-cocycle.
theorem
GQ2.ContCoh.cup20_acobound
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
[DistribMulAction G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
{c : G × G → M}
(hc : c ∈ B2 G M)
(n : ↥(H0 G N))
:
Descent for (2,0): cup of a coboundary with an invariant is a coboundary.
def
GQ2.ContCoh.cup20ZH
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (2,0) cup, bundled biadditively at the cocycle level.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
GQ2.ContCoh.cup20
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{M : Type u_2}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
[DiscreteTopology M]
[DistribMulAction G M]
{N : Type u_3}
[AddCommGroup N]
[TopologicalSpace N]
[DiscreteTopology N]
[DistribMulAction G N]
[ContinuousSMul G N]
{P : Type u_4}
[AddCommGroup P]
[TopologicalSpace P]
[IsTopologicalAddGroup P]
[DistribMulAction G P]
(μ : M →+ N →+ P)
(hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n)
:
The (2,0) cup product H²(G,M) →+ H⁰(G,N) →+ H²(G,P).
Equations
- GQ2.ContCoh.cup20 μ hμ = QuotientAddGroup.lift ((GQ2.ContCoh.B2 G M).addSubgroupOf (GQ2.ContCoh.Z2 G M)) (GQ2.ContCoh.cup20ZH μ hμ) ⋯
Instances For
Coefficient naturality #
The cup product is natural in the pairing's target: post-composing μ with a continuous
G-equivariant fP : P →+ P' and cupping equals cupping and then applying the coefficient map
mapCoeff2 fP. (Stated for the (1,1) cup; the same holds in the other shapes.)
def
GQ2.ContCoh.postPairing
{M : Type u_2}
[AddCommGroup M]
{N : Type u_3}
[AddCommGroup N]
{P : Type u_4}
[AddCommGroup P]
(μ : M →+ N →+ P)
{P' : Type u_5}
[AddCommGroup P']
(fP : P →+ P')
:
M →+ N →+ P'
The pairing μ post-composed with a target map fP, as a biadditive pairing into P'.
Equations
- GQ2.ContCoh.postPairing μ fP = (AddMonoidHom.compHom fP).comp μ