Module

CharacterDetection.lean

Nyll.ProCGroups.Abelian.CharacterDetection

4 declarations indexed from sourceView source ↗

Module documentation

Finite characters detect conjugation on topological abelianization

Distinct classes in the topological abelianization of a profinite group are separated by a continuous homomorphism to an actual finite discrete abelian quotient. Applied to a normal subgroup, this identifies trivial conjugation on its abelianization with invariance of all its finite continuous characters.

Imports3

Imported by2

theorem

exists_finite_character_of_mk_ne

L31 ↗

ProCGroups.Abelian.TopologicalAbelianization.exists_finite_character_of_mk_ne

Documentation

A finite discrete abelian quotient separates two distinct abelianization classes. The character is the composite of abelianization with an open-normal quotient, so its finiteness and continuity are supplied by the construction.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Abelian
universe u v
namespace TopologicalAbelianization

Lean source · statement

theorem exists_finite_character_of_mk_ne
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {x y : G} (hxy : mk G x ≠ mk G y) :
    ∃ (A : Type u) (_ : CommGroup A) (_ : TopologicalSpace A)
      (_ : Finite A) (_ : DiscreteTopology A),
      ∃ χ : G →ₜ* A, χ x ≠ χ y

theorem

mk_eq_iff_finite_characters_eq

L62 ↗

ProCGroups.Abelian.TopologicalAbelianization.mk_eq_iff_finite_characters_eq

Documentation

Equality of abelianization classes is equivalent to equality under all continuous characters with finite discrete abelian targets.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Abelian
universe u v
namespace TopologicalAbelianization

Lean source · statement

theorem mk_eq_iff_finite_characters_eq
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {x y : G} :
    mk G x = mk G y ↔
      ∀ (A : Type u) [CommGroup A] [TopologicalSpace A]
        [Finite A] [DiscreteTopology A],
        ∀ χ : G →ₜ* A, χ x = χ y

theorem

quotientConjugationTopologicalAbelianizationMap_ne_one_of_character_ne

L87 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_ne_one_of_character_ne

Documentation

A character changed by conjugation detects a nontrivial automorphism of the normal subgroup's topological abelianization. This direction needs only a T₁ commutative target, so it also applies to finite characters.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Abelian
universe u v

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_ne_one_of_character_ne
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {N : Subgroup G} [N.Normal]
    {A : Type v} [CommGroup A] [TopologicalSpace A] [T1Space A]
    (χ : N →ₜ* A) {g : G} {n : N}
    (hχ : χ (MulAut.conjNormal g n) ≠ χ n) :
    quotientConjugationTopologicalAbelianizationMap (G := G) N
      (QuotientGroup.mk' N g) ≠ 1

theorem

quotientConjugationTopologicalAbelianizationMap_eq_one_iff_finite_characters_fixed

L117 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_eq_one_iff_finite_characters_fixed

Documentation

If the normal subgroup is profinite, a quotient element acts trivially on its topological abelianization exactly when it fixes every finite continuous character. Profinite hypotheses are needed only on the subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ProCGroups.Abelian
universe u v

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_eq_one_iff_finite_characters_fixed
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {N : Subgroup G} [N.Normal]
    [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
    {g : G} :
    quotientConjugationTopologicalAbelianizationMap (G := G) N
        (QuotientGroup.mk' N g) = 1 ↔
      ∀ (A : Type u) [CommGroup A] [TopologicalSpace A]
        [Finite A] [DiscreteTopology A],
        ∀ (χ : N →ₜ* A) (n : N), χ (MulAut.conjNormal g n) = χ n

Module documentation

Finite characters detect conjugation on topological abelianization

Declarations

exists_finite_character_of_mk_ne

mk_eq_iff_finite_characters_eq

quotientConjugationTopologicalAbelianizationMap_ne_one_of_character_ne

quotientConjugationTopologicalAbelianizationMap_eq_one_iff_finite_characters_fixed