NYLL
Module

PrimeOrderTest.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.PrimeOrderTest
2 declarations indexed from sourceView source ↗

Module documentation

The prime-order test for ab-faithfulness

A nonfaithful finite quotient action has a prime-order subgroup in its kernel. Pulling that subgroup back gives an open layer with prime-order quotient and trivial action on the topological abelianization of its kernel.

Imports6
Imported by4

Declarations

theorem

exists_prime_quotient_trivial_action_of_not_injective

L33 ↗
ProCGroups.FiniteStepSolvableQuotients.exists_prime_quotient_trivial_action_of_not_injective
Documentation

A nonfaithful open layer yields an open layer with prime-order quotient and trivial action. The new open subgroup is constructed in the original ambient group, so the result requires no additional inheritance assumption on the prime-order test.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem exists_prime_quotient_trivial_action_of_not_injective
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G]
    (H : OpenSubgroup G) (N : OpenNormalSubgroup ↥(H : Subgroup G))
    (hρ : ¬ Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))))) :
    ∃ J : OpenSubgroup G, ∃ M : OpenNormalSubgroup ↥(J : Subgroup G),
      Nat.Prime (Nat.card (↥(J : Subgroup G) ⧸ (M : Subgroup ↥(J : Subgroup G)))) ∧
      quotientConjugationTopologicalAbelianizationMap
        (G := ↥(J : Subgroup G)) (N := (M : Subgroup ↥(J : Subgroup G))) = 1
theorem

isAbFaithful_iff_prime_order_test

L158 ↗
ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_iff_prime_order_test
Documentation

A compact topological group is ab-faithful if and only if every open layer with prime-order quotient acts nontrivially on the topological abelianization of its kernel.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem isAbFaithful_iff_prime_order_test
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] :
    IsAbFaithful G ↔
      ∀ H : OpenSubgroup G, ∀ N : OpenNormalSubgroup ↥(H : Subgroup G),
        Nat.Prime (Nat.card (↥(H : Subgroup G) ⧸ (N : Subgroup ↥(H : Subgroup G)))) →
        quotientConjugationTopologicalAbelianizationMap
          (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))) ≠ 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.