Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Unit

The unit of the cup product on continuous cohomology #

Let u be a G-invariant vector of a topological representation Y, and let P be a coefficient pairing for which u is a unit. The degree-zero class of u (TauCeti.ContinuousCohomology.degreeZeroClass) is then a unit for the cup product TauCeti.TopPairing.cup on continuous cohomology:

a ⌣ [u] = a   if  P.bil x u = x  for all x   (P : TopPairing X Y X),
[u] ⌣ a = a   if  P.bil u x = x  for all x   (P : TopPairing Y X X).

The main application is a discrete G-ring with its multiplication as the pairing and u = 1, where these are the unit laws 1 ⌣ a = a = a ⌣ 1 of the cohomology ring.

The class of u is represented by the constant 0-cocycle g ↦ u (TauCeti.ContinuousCohomology.degreeZeroCocycle), and on it both identities already hold at the level of homogeneous cochains: the Alexander–Whitney formula (a ⌣ b) (g₀, …, g_{m+n}) = μ (a (g₀, …, g_m)) (b (g_m, …, g_{m+n})) pairs every value of a with u, or u with every value of a. On the right the total degree m + 0 is m by definition. On the left the total degree 0 + n is only propositionally n, so the cochain-level identity carries the transport HomologicalComplex.XIsoOfEq and the class-level identity carries the transport TauCeti.ContinuousCohomology.degreeCast along n = 0 + n.

Main results #

References #

The unit on the right #

source
theorem TauCeti.TopPairing.cupCochain_degreeZeroCocycle_right {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (P : TopPairing X Y X) (u : ↑Y) (hu : ∀ (x : ↑X), (P.bil x) u = x) (hinv : ∀ (g : G), (Y.ρ g) u = u) (m : ℕ) (a : ↑(X.homogeneousCochains.X m).toModuleCat) :
((P.cupCochain m 0) a) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Y.homogeneousCochains 0)) (ContinuousCohomology.degreeZeroCocycle Y u hinv)) = a

The right unit law for the cup product of homogeneous cochains: cupping with the constant 0-cocycle of a right unit u is the identity.

source
@[simp]
theorem TauCeti.TopPairing.cup_one_right {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (P : TopPairing X Y X) (u : ↑Y) (hu : ∀ (x : ↑X), (P.bil x) u = x) (hinv : ∀ (g : G), (Y.ρ g) u = u) (m : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) :
((P.cup m 0) a) (ContinuousCohomology.degreeZeroClass Y u hinv) = a

The right unit law for the cup product on continuous cohomology: if u is an invariant vector with P.bil x u = x for every x, then a ⌣ [u] = a for every class a. For a discrete G-ring and its multiplication this is a ⌣ 1 = a.

The unit on the left #

source
theorem TauCeti.TopPairing.cupCochain_degreeZeroCocycle_left {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (P : TopPairing Y X X) (u : ↑Y) (hu : ∀ (x : ↑X), (P.bil u) x = x) (hinv : ∀ (g : G), (Y.ρ g) u = u) (n : ℕ) (a : ↑(X.homogeneousCochains.X n).toModuleCat) :
((P.cupCochain 0 n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Y.homogeneousCochains 0)) (ContinuousCohomology.degreeZeroCocycle Y u hinv))) a = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq X.homogeneousCochains ⋯).hom) a

The left unit law for the cup product of homogeneous cochains: cupping the constant 0-cocycle of a left unit u with a is a, transported from degree n to 0 + n.

source
@[simp]
theorem TauCeti.TopPairing.cup_one_left {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (P : TopPairing Y X X) (u : ↑Y) (hu : ∀ (x : ↑X), (P.bil u) x = x) (hinv : ∀ (g : G), (Y.ρ g) u = u) (n : ℕ) (a : ↑(continuousCohomology n X).toModuleCat) :
((P.cup 0 n) (ContinuousCohomology.degreeZeroClass Y u hinv)) a = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.degreeCast X ⋯).hom) a

The left unit law for the cup product on continuous cohomology: if u is an invariant vector with P.bil u x = x for every x, then [u] ⌣ a = a for every class a, where the right-hand side is transported from degree n to the degree 0 + n of the cup product. For a discrete G-ring and its multiplication this is 1 ⌣ a = a.