Documentation

TauCeti.NumberTheory.ClassFieldTheory.Formation.TrivialLayer

Trivial layers and class formations #

For a finite normal layer V ◁ U with equal top and ground subgroups, the relative subgroup is all of U, so its Galois group U / V is trivial and its degree is one. The norm is therefore the identity after identifying the two levels. In particular, its image is the whole ground level and the norm quotient is trivial.

For a class formation, Artin reciprocity identifies this norm quotient with the additive abelianization of the Galois group. Consequently the Artin map of the layer is the unique additive homomorphism into a trivial group. This gives the trivial-layer direction check without comparing cardinalities.

If the ambient profinite group itself is a subsingleton, every layer is trivial. In that case every positive-degree cohomology group of a layer vanishes, so every formation has a canonical class formation whose invariant maps are zero. This is the class formation used at a complex place.

Main statements #

References #

source
theorem TauCeti.ClassFieldTheory.NormalLayer.top_eq_ground_of_subsingleton {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) [Subsingleton G] :
L.top = L.ground

Every layer over a subsingleton group is trivial.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_gal_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (hL : L.top = L.ground) :
Subsingleton L.Gal

The Galois group of a layer whose top and ground subgroups agree is trivial.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.degree_eq_one_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (hL : L.top = L.ground) :
L.degree = 1

A layer whose top and ground subgroups agree has degree one.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_H_succ_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (hL : L.top = L.ground) (n : ℕ) :
Subsingleton ↑(L.H F (n + 1))

The positive-degree cohomology of a layer whose top and ground subgroups agree vanishes.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.norm_apply_coe_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (hL : L.top = L.ground) (x : ↥(F.level L.top)) :
↑((L.norm F) x) = ↑x

The norm of a trivial layer is the identity after reading both levels in the ambient representation.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.norm_surjective_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (hL : L.top = L.ground) :
Function.Surjective ⇑(L.norm F)

The norm of a layer whose top and ground subgroups agree is surjective.

source
@[simp]
theorem TauCeti.ClassFieldTheory.NormalLayer.normSubgroup_eq_top_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (hL : L.top = L.ground) :
L.normSubgroup F = ⊤

The norm subgroup of a trivial layer is the whole ground level.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_normQuotient_of_top_eq_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (hL : L.top = L.ground) :
Subsingleton (L.NormQuotient F)

The norm quotient of a trivial layer is a subsingleton.

source
noncomputable def TauCeti.ClassFieldTheory.ClassFormation.ofSubsingleton {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) [Subsingleton G] :
ClassFormation F

The canonical class formation on a formation over a subsingleton profinite group. Every layer is trivial, its positive-degree cohomology vanishes, and its invariant map is consequently zero.

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.ClassFormation.ofSubsingleton_inv_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Subsingleton G] (F : Formation G) (L : NormalLayer G) (x : ↑(L.H F 2)) :
    ((ofSubsingleton F).inv L) x = 0

    The invariant maps of the canonical class formation over a subsingleton group are zero.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.ClassFormation.artinMap_trivialLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (hL : L.top = L.ground) :
    cf.artinMap L = 0

    The Artin map of a layer whose top and ground subgroups agree is the zero homomorphism.