Yamaguchi26AbfaithfulGalois.relative_centerfree_and_slim_criterion_6_4
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe uLean source · statement
theorem relative_centerfree_and_slim_criterion_6_4
(sigma : Set ℕ) (G : ProfiniteGrp.{u}) (hG : IsSigmaAbFaithful sigma G)
(D : ClosedSubgroup G) [(D : Subgroup G).Normal]
(hDderived : (D : Subgroup G) ≤ topDerivedTop G 1)
(hOrient : ∀ (p : ℕ) [Fact p.Prime], p ∈ sigma →
Nontrivial (PrimaryAbelianization p (D : Subgroup G)) →
∃ θ : Orientation p G, FormalHilbert90 θ) :
Subgroup.center (G ⧸ sigmaResidualKernel sigma D) = ⊥ ∧
((∀ (p : ℕ) [Fact p.Prime], p ∈ sigma →
Nontrivial (PrimaryAbelianization p (D : Subgroup G)) →
∃ θ : Orientation p G, FormalHilbert90 θ ∧ Set.Infinite (Set.range θ)) →
IsSlim (G ⧸ sigmaResidualKernel sigma D))