ModuleAbFaithfulness.lean
Nyll.ProCGroups.FiniteStepSolvableQuotients.AbFaithfulness
2 declarations indexed from sourceView source ↗ Module documentation
Abelianization faithfulness
Every open subgroup acts faithfully on the topological abelianization of each open normal subgroup. The relative pro-Σ version uses the same quotient-conjugation action on the maximal pro-Σ quotient.
Declarations
ProCGroups.FiniteStepSolvableQuotients.IsAbFaithful
DocumentationEvery open subgroup acts faithfully on the topological abelianization of each open normal subgroup.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful
DocumentationDefinition in Section 1: every finite relative quotient acts faithfully on the abelianized maximal pro-Σ quotient of its open normal subgroup.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u