Documentation

TauCeti.NumberTheory.ClassFieldTheory.Formation.Tate.Conjugation

Conjugation and the Tate isomorphism of a class formation #

An element g of the ambient group carries a finite normal layer V ◁ U to its conjugate gVg⁻¹ ◁ gUg⁻¹ (NormalLayer.conjugate), with an isomorphism of Galois groups (NormalLayer.conjugateGalEquiv) and the action of g on the coefficient modules. Conjugation of Tate cohomology with formation coefficients is NormalLayer.conjugateTateIso. This file adds the same conjugation on Tate cohomology with trivial integral coefficients (NormalLayer.conjugateTrivialTateIso), which in degree -2 is the induced isomorphism of abelianized Galois groups, and proves that cup product with a degree-two class is equivariant: conjugating x ∪ u gives the cup product of the conjugates (cupClass_conj).

Since conjugation carries the fundamental class of a layer of a class formation to the fundamental class of the conjugate layer (ClassFormation.fundamentalClass_conj), Tate's isomorphism H^r(U/V, ℤ) ≃ H^{r+2}(U/V, A^V) commutes with conjugation in every degree (ClassFormation.tateIso_conj). In degree -2 this is the conjugation compatibility of the Artin map.

Main definitions #

Main statements #

References #

source
noncomputable def TauCeti.ClassFieldTheory.NormalLayer.conjugateTrivialTateIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (r : ℤ) :
L.TrivialTateH r ≅ (L.conjugate g).TrivialTateH r

Conjugation on Tate cohomology with trivial integral coefficients: the isomorphism H^r(U/V, ℤ) ≅ H^r(gUg⁻¹/gVg⁻¹, ℤ) induced by the isomorphism of Galois groups.

Instances For
    source
    theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTrivialTateIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (r : ℤ) :
    (L.conjugateTrivialTateIso g r).hom = TateCohomology.map ⋯ r

    Conjugation with trivial integral coefficients is the Tate map of the compatible pair formed by the isomorphism of Galois groups and the identity of ℤ.

    source
    theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTrivialTateIso_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (r : ℤ) :
    L.conjugateTrivialTateIso 1 r = CategoryTheory.eqToIso ⋯

    Conjugation by 1 is the identity on Tate cohomology with trivial integral coefficients, up to transport along conjugate_one.

    source
    theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTrivialTateIso_trans_conjugateTrivialTateIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g h : G) (r : ℤ) :
    L.conjugateTrivialTateIso h r ≪≫ (L.conjugate h).conjugateTrivialTateIso g r = L.conjugateTrivialTateIso (g * h) r ≪≫ CategoryTheory.eqToIso ⋯

    Conjugation by h and then by g on Tate cohomology with trivial integral coefficients is conjugation by g * h, up to transport along conjugate_conjugate.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.NormalLayer.tateHMinusTwoEquivAbelianization_conjugateTrivialTateIso_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (x : ↑(L.TrivialTateH (-2))) :
    (L.conjugate g).tateHMinusTwoEquivAbelianization ((CategoryTheory.ConcreteCategory.hom (L.conjugateTrivialTateIso g (-2)).hom) x) = (MulEquiv.toAdditive (L.conjugateGalEquiv g).abelianizationCongr) (L.tateHMinusTwoEquivAbelianization x)

    In degree -2, conjugation is conjugation of abelianized Galois groups: under the identifications H^{-2}(U/V, ℤ) ≃ (U/V)^ab, it is the isomorphism induced by conjugateGalEquiv.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.cupClass_conj {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (g : G) (u : ↑(L.H F 2)) (r : ℤ) (x : ↑(L.TrivialTateH r)) :
    (CategoryTheory.ConcreteCategory.hom (L.conjugateTateIso F g (r + 2)).hom) ((cupClass F L u r) x) = (cupClass F (L.conjugate g) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) u) r) ((CategoryTheory.ConcreteCategory.hom (L.conjugateTrivialTateIso g r).hom) x)

    Cup product with a degree-two class commutes with conjugation: conjugating x ∪ u by g gives the cup product of the conjugate of x with the conjugate of u, in every degree.

    source
    theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_conj {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (g : G) (r : ℤ) (x : ↑(L.TrivialTateH r)) :
    (CategoryTheory.ConcreteCategory.hom (L.conjugateTateIso F g (r + 2)).hom) ((cf.tateIso L r) x) = (cf.tateIso (L.conjugate g) r) ((CategoryTheory.ConcreteCategory.hom (L.conjugateTrivialTateIso g r).hom) x)

    Tate's isomorphism of a class formation commutes with conjugation: conjugating x ∪ u_{U/V} by g gives the cup product of the conjugate of x with the fundamental class of the conjugate layer.