theorem
L33 ↗sigma_properties_1_3
Yamaguchi26AbfaithfulGalois.sigma_properties_1_3
Allowing all primes recovers ordinary ab-faithfulness. Enlarging Σ preserves Σ-ab-faithfulness, and the maximal pro-Σ quotient inherits it. For a singleton set of primes, both the original group and its maximal pro-ℓ quotient are ordinarily ab-faithful.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
universe uLean source · full declaration
theorem sigma_properties_1_3
{sigma : Set ℕ} (G : ProfiniteGrp.{u}) :
(IsSigmaAbFaithful Set.univ G ↔ IsAbFaithful G) ∧
(IsSigmaAbFaithful sigma G →
let Q := G ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G
letI : TotallyDisconnectedSpace Q :=
totallyDisconnectedSpace_quotient_closedNormal
(proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G)
(proCResidualCore_isClosed (FiniteGroupClass.sigmaGroup sigma) G)
(∀ tau : Set ℕ, sigma ⊆ tau → IsSigmaAbFaithful tau G) ∧
IsSigmaAbFaithful sigma Q ∧
(∀ ell : ℕ, sigma = {ell} →
IsAbFaithful G ∧ IsAbFaithful Q)) := by
refine ⟨isSigmaAbFaithful_univ_iff (G := G), ?_⟩
intro hG
let Q := G ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G
let : TotallyDisconnectedSpace Q :=
totallyDisconnectedSpace_quotient_closedNormal
(proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G)
(proCResidualCore_isClosed (FiniteGroupClass.sigmaGroup sigma) G)
change (∀ tau : Set ℕ, sigma ⊆ tau → IsSigmaAbFaithful tau G) ∧
IsSigmaAbFaithful sigma Q ∧
(∀ ell : ℕ, sigma = {ell} → IsAbFaithful G ∧ IsAbFaithful Q)
have hQ : IsAbFaithful Q := hG.isAbFaithful_residualQuotient
refine ⟨?_, ?_, ?_⟩
· intro tau hsub
exact IsSigmaAbFaithful.mono hsub hG
· exact (isSigmaAbFaithful_iff_isAbFaithful_of_proSigma
(G := Q) (sigma := sigma)
(proCResidualCoreQuotient_hasOpenNormalBasisInClass
(G := G) (FiniteGroupClass.sigmaGroup_formation sigma))).2 hQ
· intro ell _
exact ⟨hG.isAbFaithful, hQ⟩