Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.TrivialFp.Form

The cup form of a linear functional on Hยฒ(G, ๐”ฝ_p) #

Composing the cup square cupFp p G : Hยน(G, ๐”ฝ_p) ร— Hยน(G, ๐”ฝ_p) โ†’ Hยฒ(G, ๐”ฝ_p) with a linear functional ฯ† : Hยฒ(G, ๐”ฝ_p) โ†’โ‚— ๐”ฝ_p gives an ๐”ฝ_p-bilinear form (a, b) โ†ฆ ฯ† (a โŒฃ b) on Hยน(G, ๐”ฝ_p), the cup form ฯ†.cupForm. It is the object through which Mathlib's theory of bilinear forms โ€” alternation, symmetry, nondegeneracy, matrices with respect to a basis โ€” applies to the cup product; a Demushkin group is a pro-p group whose cup form, for an isomorphism ฯ† : Hยฒ(G, ๐”ฝ_p) โ‰… ๐”ฝ_p, is nondegenerate.

Graded commutativity of the cup square makes the cup form skew-symmetric, hence reflexive; at an odd prime every cup square a โŒฃ a vanishes (TauCeti.cupFp_self_eq_zero_of_ne_two) and the form is alternating, while at p = 2 it is symmetric. When ฯ† is injective the form is alternating exactly when every cup square vanishes and nondegenerate exactly when the cup square separates points, so neither property depends on the choice of ฯ†: replacing ฯ† by a nonzero multiple rescales the form and changes nothing below.

Main definitions #

Main results #

References #

The cup form #

The form is a construction on the linear functional ฯ†, so it and its lemmas live in the LinearMap namespace: ฯ†.cupForm.

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

The cup form of a linear functional ฯ† : Hยฒ(G, ๐”ฝ_p) โ†’โ‚— ๐”ฝ_p: the ๐”ฝ_p-bilinear form (a, b) โ†ฆ ฯ† (a โŒฃ b) on Hยน(G, ๐”ฝ_p). For a Demushkin group, where Hยฒ(G, ๐”ฝ_p) is one-dimensional, an isomorphism ฯ† : Hยฒ(G, ๐”ฝ_p) โ‰… ๐”ฝ_p turns the cup square into the nondegenerate bilinear form of Labute's definition.

Equations
Instances For
    source
    @[simp]
    theorem LinearMap.cupForm_apply {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) (a b : โ†‘(TauCeti.cohomFp p G 1).toModuleCat) :
    (ฯ†.cupForm a) b = ฯ† (((TauCeti.cupFp p G) a) b)
    source
    @[simp]
    theorem LinearMap.cupForm_smul {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (c : ZMod p) (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) :
    (c โ€ข ฯ†).cupForm = c โ€ข ฯ†.cupForm

    Rescaling the functional rescales the cup form.

    source
    theorem LinearMap.cupForm_gradedComm {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) (a b : โ†‘(TauCeti.cohomFp p G 1).toModuleCat) :
    (ฯ†.cupForm a) b = -(ฯ†.cupForm b) a

    The cup form is skew-symmetric, by graded commutativity of the cup square.

    source
    theorem LinearMap.isRefl_cupForm {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) :
    ฯ†.cupForm.IsRefl

    The cup form is reflexive: ฯ† (a โŒฃ b) = 0 implies ฯ† (b โŒฃ a) = 0.

    source
    theorem LinearMap.isAlt_cupForm_iff {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) :
    ฯ†.cupForm.IsAlt โ†” โˆ€ (a : โ†‘(TauCeti.cohomFp p G 1).toModuleCat), ฯ† (((TauCeti.cupFp p G) a) a) = 0

    The cup form is alternating exactly when ฯ† kills every cup square.

    source
    theorem LinearMap.isAlt_cupForm_iff_of_injective {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) (hฯ† : Function.Injective โ‡‘ฯ†) :
    ฯ†.cupForm.IsAlt โ†” โˆ€ (a : โ†‘(TauCeti.cohomFp p G 1).toModuleCat), ((TauCeti.cupFp p G) a) a = 0

    For injective ฯ†, the cup form is alternating exactly when every cup square a โŒฃ a vanishes; in particular alternation does not depend on the choice of ฯ†.

    source
    theorem LinearMap.isAlt_cupForm_of_ne_two {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) (hp : p โ‰  2) :
    ฯ†.cupForm.IsAlt

    At an odd prime the cup form is alternating.

    source
    theorem LinearMap.isSymm_cupForm_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp 2 G 2).toModuleCat โ†’โ‚—[ZMod 2] ZMod 2) :
    ฯ†.cupForm.IsSymm

    At p = 2 the cup form is symmetric: skew-symmetry is symmetry in characteristic two.

    source
    theorem LinearMap.nondegenerate_cupForm_iff_of_injective {p : โ„•} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ฯ† : โ†‘(TauCeti.cohomFp p G 2).toModuleCat โ†’โ‚—[ZMod p] ZMod p) (hฯ† : Function.Injective โ‡‘ฯ†) :
    ฯ†.cupForm.Nondegenerate โ†” โˆ€ (a : โ†‘(TauCeti.cohomFp p G 1).toModuleCat), a โ‰  0 โ†’ โˆƒ (b : โ†‘(TauCeti.cohomFp p G 1).toModuleCat), ((TauCeti.cupFp p G) a) b โ‰  0

    For injective ฯ†, the cup form is nondegenerate exactly when the cup square separates points on the left: every nonzero class a has some b with a โŒฃ b โ‰  0. By reflexivity the right-separating condition is automatic, and nondegeneracy does not depend on the choice of ฯ†.