Yamaguchi26AbfaithfulGalois.relative_centerfree_and_slim_criterion
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
universe uLean source · statement
theorem relative_centerfree_and_slim_criterion
(G : ProfiniteGrp.{u})
(D : Subgroup G) [D.Normal]
(hDclosed : IsClosed (D : Set G)) (hDderived : D ≤ topDerivedTop G 1)
(hFaithful : ∀ N : OpenNormalSubgroup G,
D ≤ (N : Subgroup G) →
Function.Injective
(quotientConjugationTopologicalAbelianizationMap
(G := G) (N := (N : Subgroup G))))
(hOrient : ∀ (ℓ : ℕ) [Fact ℓ.Prime],
Nontrivial (PrimaryAbelianization ℓ D) →
∃ θ : Orientation ℓ G, RelativeFormalHilbert90 D θ) :
Subgroup.center (RelativeDerivedQuotient D) = ⊥ ∧
((∀ (ℓ : ℕ) [Fact ℓ.Prime],
Nontrivial (PrimaryAbelianization ℓ D) →
∃ θ : Orientation ℓ G,
RelativeFormalHilbert90 D θ ∧ Set.Infinite (Set.range θ)) →
IsSlim (RelativeDerivedQuotient D))