Cup product with a class of a finite normal layer

The cup product with a class in ordinary degree two gives a homomorphism from Tate cohomology with trivial integral coefficients to Tate cohomology with formation coefficients. The ordinary class is first transported to Tate degree two, and the tensor product with the trivial representation is removed using the left unitor. For a class formation, the chosen class is its fundamental class. This is the map whose invertibility is asserted by Tate's theorem.

The construction uses the Tate cup product of TauCeti.RepresentationTheory.Homological.TateCohomology.Cup.Product, following the cup product formulation in Artin and Tate, Class Field Theory, Chapter XIV, §4.

noncomputable def TauCeti.ClassFieldTheory.cupClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (r : ℤ) : ↑(L.TrivialTateH r) →+ ↑(L.TateH F (r + 2))

Cup product with a class in H²(U/V, A^V), viewed in Tate degree two, followed by the tensor-unit isomorphism ℤ ⊗ A^V ≅ A^V.

theorem TauCeti.ClassFieldTheory.cupClass_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (r : ℤ) (x : ↑(L.TrivialTateH r)) : (cupClass F L u r) x = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor (r + 2)).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor (L.rep F)).hom)) (((TateCohomology.cup (Rep.trivial ℤ L.Gal ℤ) (L.rep F) r 2 (r + 2) ⋯) x) ((CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).inv) u))

The map cupClass evaluates by taking the Tate cup product with the degree-two image of u, then applying the left unitor to the coefficient representation.

@[simp]

theorem TauCeti.ClassFieldTheory.cupClass_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (r : ℤ) : cupClass F L 0 r = 0

Cup product with the zero class is zero.

@[simp]

theorem TauCeti.ClassFieldTheory.cupClass_add {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u v : ↑(L.H F 2)) (r : ℤ) : cupClass F L (u + v) r = cupClass F L u r + cupClass F L v r

Cup product is additive in the chosen degree-two class.

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (r : ℤ) : ↑(L.TrivialTateH r) →+ ↑(L.TateH F (r + 2))

Cup product with the fundamental class of a finite normal layer.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClass_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (r : ℤ) (x : ↑(L.TrivialTateH r)) : (cf.cupFundamentalClass L r) x = (cupClass F L (cf.fundamentalClass L) r) x

The map cupFundamentalClass evaluates as cupClass at the fundamental class.