Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.TrivialFp.Basic

The cup product with trivial ZMod p coefficients #

Multiplication in ZMod p gives a continuous equivariant pairing of the trivial coefficient representations. Its cup product in degrees (1, 1) is the bilinear pairing on continuous cohomology used to define and study Demushkin groups. The coefficient representation is lifted to the universe of the group, as required by the continuous cohomology complex. When p is prime, ZMod p is the field ๐”ฝ_p.

Because multiplication is commutative the opposite pairing of fpPairing p G is itself, and graded commutativity of the cup product in bidegree (1, 1) reads cupFp p G a b = - cupFp p G b a (TauCeti.cupFp_gradedComm). Consequently a โŒฃ b vanishes exactly when b โŒฃ a does, and at an odd prime every cup square a โŒฃ a vanishes, since 2 is then invertible in ๐”ฝ_p.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.fpPairing (p : โ„•) (G : Type u) [Monoid G] :
TopPairing (trivialFp p G) (trivialFp p G) (trivialFp p G)

Multiplication of trivial ZMod p coefficients as a continuous equivariant bilinear pairing.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.fpPairing_bil_apply (p : โ„•) (G : Type u) [Monoid G] (x y : โ†‘(trivialFp p G)) :
    ((fpPairing p G).bil x) y = (trivialFpEquiv p G).symm ((trivialFpEquiv p G) x * (trivialFpEquiv p G) y)

    The coefficient pairing is multiplication in ZMod p, under the universe lift.

    source
    theorem TauCeti.fpPairing_bil_comm (p : โ„•) (G : Type u) [Monoid G] (x y : โ†‘(trivialFp p G)) :
    ((fpPairing p G).bil x) y = ((fpPairing p G).bil y) x

    Multiplication on the trivial coefficient representation is symmetric.

    source
    @[simp]
    theorem TauCeti.fpPairing_flip (p : โ„•) (G : Type u) [Monoid G] :
    (fpPairing p G).flip = fpPairing p G

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

    source
    theorem TauCeti.eqToHom_res_fpPairing_bil (p : โ„•) (G : Type u) [Group G] (S : Subgroup G) (x y : โ†‘(TopRep.res S.subtype (trivialFp p G))) :
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom โ‹ฏ)) ((((fpPairing p G).res S.subtype).bil x) y) = ((fpPairing p โ†ฅS).bil ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom โ‹ฏ)) x)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom โ‹ฏ)) y)

    Transport along res_trivialFp intertwines the restricted multiplication pairing of G with the multiplication pairing of S.

    source
    noncomputable def TauCeti.cupFp (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    โ†‘(cohomFp p G 1).toModuleCat โ†’โ‚—[ZMod p] โ†‘(cohomFp p G 1).toModuleCat โ†’โ‚—[ZMod p] โ†‘(cohomFp p G 2).toModuleCat

    The degree-(1,1) cup product on continuous cohomology with trivial ZMod p coefficients.

    Equations
    Instances For
      source
      theorem TauCeti.cupFp_def (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
      cupFp p G = (fpPairing p G).cup 1 1

      The specialized cup product is the general cup product of the multiplication pairing. This equation lets general cup-product results apply to arbitrary cohomology classes.

      source
      @[simp]
      theorem TauCeti.cupFp_ฯ€ (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a b : โ†‘(ContinuousCohomology.cocycles (trivialFp p G) 1).toModuleCat) :
      ((cupFp p G) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.ฯ€ (trivialFp p G) 1)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.ฯ€ (trivialFp p G) 1)) b) = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.ฯ€ (trivialFp p G) 2)) ((((fpPairing p G).cupCocycles 1 1) a) b)

      On classes of cocycles, cupFp is the class of their cochain cup product.

      source
      @[simp]
      theorem TauCeti.cupFp_map (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (ฯ† : H โ†’โ‚œ* G) (a b : โ†‘(cohomFp p G 1).toModuleCat) :
      (CategoryTheory.ConcreteCategory.hom (cohomFpMap p ฯ† 2)) (((cupFp p G) a) b) = ((cupFp p H) ((CategoryTheory.ConcreteCategory.hom (cohomFpMap p ฯ† 1)) a)) ((CategoryTheory.ConcreteCategory.hom (cohomFpMap p ฯ† 1)) b)

      A continuous group homomorphism preserves the cup product with trivial ZMod p coefficients.

      source
      theorem TauCeti.cupFp_bijective_iff_of_bijective (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (ฯ† : H โ†’โ‚œ* G) (hโ‚ : Function.Bijective โ‡‘(CategoryTheory.ConcreteCategory.hom (cohomFpMap p ฯ† 1))) (hโ‚‚ : Function.Bijective โ‡‘(CategoryTheory.ConcreteCategory.hom (cohomFpMap p ฯ† 2))) :
      Function.Bijective โ‡‘(cupFp p G) โ†” Function.Bijective โ‡‘(cupFp p H)

      Perfectness of the cup square transfers along a continuous homomorphism ฯ† : H โ†’โ‚œ* G inducing isomorphisms on Hยน(-, ZMod p) and Hยฒ(-, ZMod p): cupFp p G is a bijection onto the linear maps Hยน(G, ZMod p) โ†’โ‚— Hยฒ(G, ZMod p) exactly when cupFp p H is.

      source
      theorem TauCeti.cupFp_bijective_congr (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G โ‰ƒโ‚œ* H) :
      Function.Bijective โ‡‘(cupFp p G) โ†” Function.Bijective โ‡‘(cupFp p H)

      Perfectness of the cup square is invariant under topological group isomorphism: cupFp p G is a bijection onto the linear maps Hยน(G, ZMod p) โ†’โ‚— Hยฒ(G, ZMod p) exactly when cupFp p H is, for G โ‰ƒโ‚œ* H.

      source
      @[simp]
      theorem TauCeti.cupFp_res (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (a b : โ†‘(cohomFp p G 1).toModuleCat) :
      (CategoryTheory.ConcreteCategory.hom (trivialFpResMap p G S 2)) (((cupFp p G) a) b) = ((cupFp p โ†ฅS) ((CategoryTheory.ConcreteCategory.hom (trivialFpResMap p G S 1)) a)) ((CategoryTheory.ConcreteCategory.hom (trivialFpResMap p G S 1)) b)

      Restriction preserves the cup product with trivial ZMod p coefficients: res (a โŒฃ b) = res a โŒฃ res b for the named restriction trivialFpResMap.

      source
      theorem TauCeti.cupFp_gradedComm (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a b : โ†‘(cohomFp p G 1).toModuleCat) :
      ((cupFp p G) a) b = -((cupFp p G) b) a

      Graded commutativity of the cup square, cupFp a b = - cupFp b a: the bidegree-(1, 1) graded commutativity of the cup product at the multiplication pairing, whose opposite pairing is itself.

      source
      theorem TauCeti.cupFp_eq_zero_comm (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a b : โ†‘(cohomFp p G 1).toModuleCat) :
      ((cupFp p G) a) b = 0 โ†” ((cupFp p G) b) a = 0

      a โŒฃ b vanishes exactly when b โŒฃ a does, by graded commutativity.

      source
      theorem TauCeti.cupFp_self_eq_zero_of_ne_two (p : โ„•) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (hp : p โ‰  2) (a : โ†‘(cohomFp p G 1).toModuleCat) :
      ((cupFp p G) a) a = 0

      At an odd prime every cup square vanishes: a โŒฃ a = -(a โŒฃ a) and 2 is invertible.