Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.Character.Basic

The canonical character of a Demushkin group #

A Demushkin group G has exactly one continuous character χ : G → ℤ_pˣ with Labute's prescription property (TauCeti.HasPrescriptionProperty): every reduction H¹(G, I(χ)/pⁱ) → H¹(G, I(χ)/p) of the twisted coefficients is surjective (Labute, Theorem 4). This file proves that theorem and defines the character, TauCeti.demushkinCharacter, the canonical character or orientation of G, whose image is the second invariant of the classification of Demushkin groups.

Write G = ⟨x₁, …, x_n ∣ r⟩ with r ∈ Φ(F) in the free pro-p group F. A continuous character χ of G is determined by its values u_i = χ(x_i), which are principal units 1 + pℤ_p, and by the relator criterion (TauCeti.presentedProP.hasPrescriptionProperty_iff_forall_isCrossedHom_eq_zero) it has the prescription property exactly when every continuous crossed homomorphism F → ℤ_p for the induced character of F vanishes at r. The existence and uniqueness theorem holds for every one-relator pro-p group whose relator has nondegenerate degree-one form (TauCeti.freeProP.degreeOneForm), a condition every Demushkin group satisfies (TauCeti.IsDemushkin.nondegenerate_degreeOneForm); it needs no normal form of the relator and is uniform in p.

Main definitions #

Main results #

References #

source
theorem TauCeti.existsUnique_hasPrescriptionProperty_presentedProP_of_nondegenerate {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] {r : freeProP p X} (hr : r ∈ proPFrattini p (freeProP p X)) (hnd : (freeProP.degreeOneForm (gradedMk p (freeProP p X) 1 ⟨r, ⋯⟩)).Nondegenerate) :
∃! χ : presentedProP p X {r} →ₜ* ℤ_[p]ˣ, HasPrescriptionProperty χ

A one-relator pro-p group whose relator has nondegenerate degree-one form has exactly one continuous character with the prescription property (Labute, Theorem 4, without normal forms). Let F be the free pro-p group on a finite type X and r ∈ Φ(F) a relator whose class in gr_1(F) has nondegenerate degree-one form. Then the presented group ⟨X ∣ r⟩ has exactly one continuous character χ : ⟨X ∣ r⟩ → ℤ_pˣ with the prescription property, that is, exactly one continuous character for which every continuous crossed homomorphism F → ℤ_p for the induced character of F vanishes at r (the relator criterion, TauCeti.presentedProP.hasPrescriptionProperty_iff_forall_isCrossedHom_eq_zero).

source
theorem TauCeti.IsDemushkin.existsUnique_hasPrescriptionProperty {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
∃! χ : G →ₜ* ℤ_[p]ˣ, HasPrescriptionProperty χ

Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property.

source
noncomputable def TauCeti.demushkinCharacter {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
G →ₜ* ℤ_[p]ˣ

The canonical character (orientation) of a Demushkin group: the unique continuous character χ : G → ℤ_pˣ with the prescription property (Labute, Theorem 4). Its image is the invariant that, together with the rank, classifies Demushkin groups.

Equations
Instances For
    source
    theorem TauCeti.hasPrescriptionProperty_demushkinCharacter {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
    HasPrescriptionProperty (demushkinCharacter hG)

    The canonical character has the prescription property.

    source
    theorem TauCeti.HasPrescriptionProperty.eq_demushkinCharacter {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) :
    χ = demushkinCharacter hG

    The canonical character is the only continuous character with the prescription property. This is the uniqueness half of Labute's Theorem 4 and the normalization consumed by the marked classification.

    source
    @[simp]
    theorem TauCeti.hasPrescriptionProperty_iff_eq_demushkinCharacter {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (χ : G →ₜ* ℤ_[p]ˣ) :
    HasPrescriptionProperty χ ↔ χ = demushkinCharacter hG

    A continuous character of a Demushkin group has the prescription property exactly when it is the canonical character.

    source
    theorem TauCeti.demushkinCharacter_apply_mem_unitsPrincipal_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (g : G) :
    (demushkinCharacter hG) g ∈ unitsPrincipal p 1

    The canonical character takes values in the principal units 1 + pℤ_p.

    source
    theorem TauCeti.isClosed_range_demushkinCharacter {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
    IsClosed ↑(demushkinCharacter hG).range

    The image of the canonical character is closed: it is the image of a compact group under a continuous map.

    source
    theorem TauCeti.range_demushkinCharacter_comp_equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {H : Type w} [Group H] [TopologicalSpace H] (e : H ≃ₜ* G) :
    ((demushkinCharacter hG).comp ↑e).range = (demushkinCharacter hG).range

    Pulling the canonical character back along a topological group isomorphism e : H ≃ₜ* G does not change its image. The group H may live in any universe and need not be known to be Demushkin.

    source
    theorem TauCeti.range_demushkinCharacter_eq_of_equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {H : Type w} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) {A : Subgroup ℤ_[p]ˣ} (hA : ∀ (χ : H →ₜ* ℤ_[p]ˣ), HasPrescriptionProperty χ → χ.range = A) :
    (demushkinCharacter hG).range = A

    The image of the canonical character, read through an isomorphism: if e : G ≃ₜ* H and every continuous character of H with the prescription property has image A, then the canonical character of G has image A. This is how the image table of the normal forms, stated for any character with the prescription property of the presented group, is read on the canonical character of a Demushkin group isomorphic to that presented group.

    source
    theorem TauCeti.demushkinCharacter_of_equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {H : Type w} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsDemushkin p H) (e : G ≃ₜ* H) :
    demushkinCharacter hH = (demushkinCharacter hG).comp ↑e.symm

    The canonical character is invariant under topological isomorphism: along e : G ≃ₜ* H, the canonical character of H is the canonical character of G pulled back along e⁻¹. The two groups may live in different universes.

    source
    theorem TauCeti.range_demushkinCharacter_of_equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {H : Type w} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsDemushkin p H) (e : G ≃ₜ* H) :
    (demushkinCharacter hH).range = (demushkinCharacter hG).range

    The image of the canonical character is invariant under topological isomorphism.