Module

SigmaFaithful.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaFaithful

1 declaration indexed from sourceView source ↗

Module documentation

Sigma-abelianization-faithfulness

The quantifiers range over all open subgroups and all their open normal subgroups, without restricting the prime divisors of the relative index. The action is the existing conjugation action on the actual residual quotient.

Imports6

Imported by16

theorem

mono

L29 ↗

ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.mono

Documentation

Enlarging the permitted set of primes preserves Sigma-abelianization-faithfulness.

Source context 3 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC
universe u

Lean source · statement

theorem IsSigmaAbFaithful.mono {sigma tau : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (h : sigma ⊆ tau) (hG : IsSigmaAbFaithful sigma G) :
    IsSigmaAbFaithful tau G

Module documentation

Sigma-abelianization-faithfulness

Declarations

mono