Documentation

TauCeti.NumberTheory.ClassFieldTheory.Formation.Character

Character classes for the Artin map of a finite normal layer #

Let Γ = U ⧸ V be the Galois group of a finite normal layer. A character χ : Γ^ab → ℚ/ℤ is a homomorphism Γ → ℚ/ℤ, which is a class in H¹(Γ, ℚ/ℤ) for the trivial action. The connecting map of the sequence 0 → ℤ → ℚ → ℚ/ℤ → 0 of trivial Γ-modules sends it to a class δχ ∈ H²(Γ, ℤ), which is read in the Tate group of degree 2. This is the class through which Artin and Tate characterize the Artin map: χ(artinMap a) is the invariant of the cup product of the degree-zero class of a with δχ.

As elsewhere in this development, ℚ/ℤ is the rational circle AddCircle (1 : ℚ).

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
↑(L.TrivialTateH 2)

The connecting class δχ ∈ H²(Γ, ℤ) of a character χ : Γ^ab → ℚ/ℤ of the Galois group Γ of a finite normal layer, in the Tate group of degree 2: the image of χ, as a class in H¹(Γ, ℚ/ℤ) for the trivial action, under the connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0. This is TauCeti.TateCohomology.characterConnectingClass for the finite group Γ.

Instances For
    source
    theorem TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
    L.characterConnectingClass χ = (TateCohomology.characterConnectingClass L.Gal) χ

    The connecting class of a character of a layer is the connecting class of the character of its Galois group.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass_add {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (χ₁ χ₂ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
    L.characterConnectingClass (χ₁ + χ₂) = L.characterConnectingClass χ₁ + L.characterConnectingClass χ₂

    The connecting class is additive in the character.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) :
    L.characterConnectingClass 0 = 0

    The connecting class of the trivial character vanishes.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass_neg {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
    L.characterConnectingClass (-χ) = -L.characterConnectingClass χ

    The connecting class of the negated character is the negated class.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.NormalLayer.characterConnectingClass_sub {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (χ₁ χ₂ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
    L.characterConnectingClass (χ₁ - χ₂) = L.characterConnectingClass χ₁ - L.characterConnectingClass χ₂

    The connecting class of a difference of characters is the difference of their classes.

    source
    noncomputable def TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) :
    ↥(F.level L.ground) →+ (Additive (Abelianization L.Gal) →+ AddCircle 1) →+ ↑(L.H F 2)

    The class a₀ ∪ δχ ∈ H²(Γ, A^V) used in the character formula for the Artin map, where a₀ is the degree-zero Tate class of a and δχ is the connecting class of the character χ. The cup product lands in the cohomology of A^V ⊗ ℤ; the right unitor identifies this coefficient representation with A^V, and positive Tate cohomology is then identified with ordinary group cohomology.

    Instances For
      source
      theorem TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (a : ↥(F.level L.ground)) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
      ((L.artinCharacterCup F) a) χ = (CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).hom) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 2).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor (L.rep F)).hom)) (((TateCohomology.cup (L.rep F) (Rep.trivial ℤ L.Gal ℤ) 0 2 2 ⋯) ((L.zeroTateClass F) a)) (L.characterConnectingClass χ)))

      The Artin character cup evaluates as the Tate cup product of a₀ with δχ, transported through the right unitor and the comparison between positive Tate and ordinary cohomology.

      source
      theorem TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup_groundLevelEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(L.rep F).ρ.invariants) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
      ((L.artinCharacterCup F) ((L.groundLevelEquiv F) x)) χ = (CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).hom) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 2).map (CategoryTheory.CategoryStruct.comp ((Rep.trivial ℤ L.Gal ℤ).tensorInvariant x) (CategoryTheory.CategoryStruct.comp (β_ (Rep.trivial ℤ L.Gal ℤ) (L.rep F)).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (L.rep F)).hom)))) (L.characterConnectingClass χ))

      For the ground-level element attached to an invariant x ∈ (A^V)^{U/V}, the Artin character cup a₀ ∪ δχ is the image of δχ under the map of coefficients ℤ → A^V, n ↦ n • x, written as n ↦ n ⊗ x ↦ x ⊗ n ↦ n • x.

      source
      theorem TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup_groundLevelEquiv_eq_H2π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(L.rep F).ρ.invariants) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) :
      ((L.artinCharacterCup F) ((L.groundLevelEquiv F) x)) χ = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (L.rep F))) (groupCohomology.characterCarryCocycles₂ (χ.comp (MonoidHom.toAdditive Abelianization.of)) (L.rep F) x)

      The Artin character cup is the carry class. For an invariant x of the coefficient module of the layer and a character χ of its abelianized Galois group, the class a₀ ∪ δχ of the character formula, for the ground-level element a corresponding to x, is the class of the carry cocycle (g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • x.

      source
      theorem TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup_eq_zero_of_mem_normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (a : ↥(F.level L.ground)) (χ : Additive (Abelianization L.Gal) →+ AddCircle 1) (ha : a ∈ L.normSubgroup F) :
      ((L.artinCharacterCup F) a) χ = 0

      The Artin character cup vanishes on the norm subgroup.

      source
      theorem TauCeti.ClassFieldTheory.NormalLayer.characterCarry_galOfOpenNormalEquiv_symm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) (χ : Additive (Abelianization (ofOpenNormal V).Gal) →+ AddCircle 1) (ψ : Additive G →+ AddCircle 1) (hχψ : ∀ (g : G), ψ (Additive.ofMul g) = χ (Additive.ofMul (Abelianization.of ((galOfOpenNormalEquiv V).symm ↑g)))) (g h : G) :
      ContCohomology.characterCarry (χ.comp (MonoidHom.toAdditive Abelianization.of)) ((galOfOpenNormalEquiv V).symm ↑g) ((galOfOpenNormalEquiv V).symm ↑h) = ContCohomology.characterCarry ψ g h

      The carry of a character of the layer V ◁ G, read on G. If ψ : G → ℚ/ℤ reads a character χ of the abelianized Galois group of the layer V ◁ G through the projection G → G ⧸ V, then the carry of χ at the images of g, h ∈ G is the carry of ψ at g, h.