Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.TrivialF2.Basic

The coefficient pairing of trivial ๐”ฝโ‚‚ coefficients #

Multiplication in ๐”ฝโ‚‚ is a G-equivariant biadditive map of the lifted carrier of the trivial ๐”ฝโ‚‚ coefficient object (TauCeti.trivialF2Pairing). This file reads it as a coefficient pairing TauCeti.TopPairing of TauCeti.trivialF2 itself, which is what the ๐”ฝโ‚‚-valued cup products of continuous cohomology are formed from. It is the โ„ค-coefficient counterpart of TauCeti.fpPairing, whose coefficient object TauCeti.trivialFp is a ZMod p-module.

Main definitions #

Main results #

source
noncomputable def TauCeti.trivialF2TopPairing (G : Type u) [Monoid G] :
TopPairing (trivialF2 G) (trivialF2 G) (trivialF2 G)

Multiplication on the trivial ๐”ฝโ‚‚ coefficient object, as a continuous equivariant pairing over โ„ค. It is the generic discrete-module pairing TauCeti.ofDiscreteModulePairing of TauCeti.trivialF2Pairing, read on the coefficient object itself along TauCeti.ofDiscreteModule_trivialF2. This is the coefficient pairing used by the mod-two Kummer cup.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.trivialF2TopPairing_bil_apply (G : Type u) [Monoid G] (x y : โ†‘(trivialF2 G)) :
    ((trivialF2TopPairing G).bil x) y = (trivialF2Equiv G).symm ((trivialF2Equiv G) x * (trivialF2Equiv G) y)

    The coefficient pairing multiplies the underlying values in ZMod 2.

    source
    theorem TauCeti.trivialF2TopPairing_bil_comm (G : Type u) [Monoid G] (x y : โ†‘(trivialF2 G)) :
    ((trivialF2TopPairing G).bil x) y = ((trivialF2TopPairing G).bil y) x

    Multiplication on the trivial ๐”ฝโ‚‚ coefficient object is symmetric.

    source
    theorem TauCeti.trivialF2TopPairing_bil_one_left (G : Type u) [Monoid G] (x : โ†‘(trivialF2 G)) :
    ((trivialF2TopPairing G).bil ((trivialF2Equiv G).symm 1)) x = x

    The lift of 1 is a left unit for multiplication on the trivial ๐”ฝโ‚‚ coefficient object.

    source
    theorem TauCeti.trivialF2TopPairing_bil_one_right (G : Type u) [Monoid G] (x : โ†‘(trivialF2 G)) :
    ((trivialF2TopPairing G).bil x) ((trivialF2Equiv G).symm 1) = x

    The lift of 1 is a right unit for multiplication on the trivial ๐”ฝโ‚‚ coefficient object.

    source
    theorem TauCeti.trivialF2TopPairing_bil_assoc (G : Type u) [Monoid G] (x y z : โ†‘(trivialF2 G)) :
    ((trivialF2TopPairing G).bil (((trivialF2TopPairing G).bil x) y)) z = ((trivialF2TopPairing G).bil x) (((trivialF2TopPairing G).bil y) z)

    Multiplication on the trivial ๐”ฝโ‚‚ coefficient object is associative.

    source
    @[simp]
    theorem TauCeti.trivialF2TopPairing_flip (G : Type u) [Monoid G] :
    (trivialF2TopPairing G).flip = trivialF2TopPairing G

    The opposite of the multiplication pairing is itself, because multiplication in ZMod 2 is commutative.

    source
    @[simp]
    theorem TauCeti.trivialF2Map_cup {G H : Type u} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] [IsTopologicalGroup H] (ฯ† : H โ†’โ‚œ* G) (m n : โ„•) (x : โ†‘(continuousCohomology m (trivialF2 G)).toModuleCat) (y : โ†‘(continuousCohomology n (trivialF2 G)).toModuleCat) :
    (CategoryTheory.ConcreteCategory.hom (trivialF2Map ฯ† (m + n))) ((((trivialF2TopPairing G).cup m n) x) y) = (((trivialF2TopPairing H).cup m n) ((CategoryTheory.ConcreteCategory.hom (trivialF2Map ฯ† m)) x)) ((CategoryTheory.ConcreteCategory.hom (trivialF2Map ฯ† n)) y)

    Pullback with trivial ๐”ฝโ‚‚ coefficients preserves the cup product in every bidegree.

    source
    theorem TauCeti.trivialF2TopPairing_cup_comm (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m n : โ„•) (x : cohomF2 G m) (y : cohomF2 G n) :
    (((trivialF2TopPairing G).cup m n) x) y = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.degreeCast (trivialF2 G) โ‹ฏ).hom) ((((trivialF2TopPairing G).cup n m) y) x)

    The mod-two cup product is commutative in every bidegree: the Koszul sign of TauCeti.TopPairing.cup_gradedComm acts trivially because every class is killed by 2.

    source
    noncomputable def TauCeti.cohomF2.one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    cohomF2 G 0

    The unit class of continuous cohomology with trivial ๐”ฝโ‚‚ coefficients: the degree-zero class of the lift of 1, a two-sided unit for the cup product along TauCeti.trivialF2TopPairing.

    Equations
    Instances For
      source
      theorem TauCeti.cohomF2.one_def (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
      one G = ContinuousCohomology.degreeZeroClass (trivialF2 G) ((trivialF2Equiv G).symm 1) โ‹ฏ

      The unit class is the degree-zero class of the lift of 1.

      The cup product on explicit cocycles #

      source
      theorem TauCeti.instContinuousSMulVIntTrivialF2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
      ContinuousSMul G โ†‘(trivialF2 G)

      The trivial ๐”ฝโ‚‚ coefficients are a discrete module.

      source
      theorem TauCeti.trivialF2TopPairing_cup_one_one_explicitH1_subgroup (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) [LocallyCompactSpace โ†ฅS] (x y : ContCohomology.H1 โ†ฅS โ†‘(trivialF2 G)) :
      (((trivialF2TopPairing โ†ฅS).cup 1 1) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH1AddEquivContinuousCohomology โ†ฅS โ†‘(trivialF2 G)) x))) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH1AddEquivContinuousCohomology โ†ฅS โ†‘(trivialF2 G)) y)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH2AddEquivContinuousCohomology โ†ฅS โ†‘(trivialF2 G)) (((ContCohomology.explicitCup11 (โ†ฅS) (โ†‘(trivialF2 G)) (โ†‘(trivialF2 G)) (โ†‘(trivialF2 G)) (trivialF2Pairing G) โ‹ฏ โ‹ฏ) x) y))

      The cup product of two classes of Hยน(S, ๐”ฝโ‚‚) on explicit cocycles, for a subgroup S. For explicit classes x and y of S valued in the carrier of the ambient trivial ๐”ฝโ‚‚ object, read in Hยน(S, ๐”ฝโ‚‚) through the comparison with continuous cohomology and the transport ofDiscreteModule_subgroup_trivialF2, their cup product along trivialF2TopPairing is the explicit (1, 1) cup product of multiplication in ๐”ฝโ‚‚, read in Hยฒ(S, ๐”ฝโ‚‚) the same way.

      source
      theorem TauCeti.trivialF2TopPairing_cup_one_one_explicitH1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (x y : ContCohomology.H1 G โ†‘(trivialF2 G)) :
      (((trivialF2TopPairing G).cup 1 1) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH1AddEquivContinuousCohomology G โ†‘(trivialF2 G)) x))) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH1AddEquivContinuousCohomology G โ†‘(trivialF2 G)) y)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom โ‹ฏ)) ((ContCohomology.explicitH2AddEquivContinuousCohomology G โ†‘(trivialF2 G)) (((ContCohomology.explicitCup11 G (โ†‘(trivialF2 G)) (โ†‘(trivialF2 G)) (โ†‘(trivialF2 G)) (trivialF2Pairing G) โ‹ฏ โ‹ฏ) x) y))

      The cup product of two classes of Hยน(G, ๐”ฝโ‚‚) on explicit cocycles. For explicit classes x and y, read in Hยน(G, ๐”ฝโ‚‚) through the comparison with continuous cohomology and the transport ofDiscreteModule_trivialF2, their cup product along trivialF2TopPairing is the explicit (1, 1) cup product of multiplication in ๐”ฝโ‚‚, (a โŒฃ b) (g, h) = a g * b h, read in Hยฒ(G, ๐”ฝโ‚‚) the same way.

      source
      theorem TauCeti.trivialF2CorMap_cup_one_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] (S : Subgroup G) (hS : IsOpen โ†‘S) [S.FiniteIndex] (x : โ†‘(continuousCohomology 1 (trivialF2 G)).toModuleCat) (y : โ†‘(continuousCohomology 1 (trivialF2 โ†ฅS)).toModuleCat) :
      (CategoryTheory.ConcreteCategory.hom (trivialF2CorMap G S hS 2)) ((((trivialF2TopPairing โ†ฅS).cup 1 1) ((CategoryTheory.ConcreteCategory.hom (trivialF2ResMap G S 1)) x)) y) = (((trivialF2TopPairing G).cup 1 1) x) ((CategoryTheory.ConcreteCategory.hom (trivialF2CorMap G S hS 1)) y)

      The (1,1) projection formula with trivial ๐”ฝโ‚‚ coefficients: degree-two corestriction of the cup of a restricted ambient class with a subgroup class is the cup of the ambient class with its degree-one corestriction.