theorem
L26 ↗integral_invariants_6_2
Yamaguchi26AbfaithfulGalois.integral_invariants_6_2
Under formal Hilbert 90 the primary abelianization of a closed normal subgroup of the closed derived group has no global invariants. An infinite orientation also excludes invariants under every open subgroup.
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 integral_invariants_6_2
{ℓ : ℕ} [Fact ℓ.Prime] (G : ProfiniteGrp.{u})
(D : Subgroup G) [D.Normal] (hDclosed : IsClosed (D : Set G))
(hDderived : D ≤ topDerivedTop G 1)
(θ : Orientation ℓ G) (hθ : FormalHilbert90 θ) :
primaryFixedSubgroup ℓ D hDclosed (⊤ : Subgroup G) = ⊥ ∧
(Set.Infinite (Set.range θ) → ∀ H : OpenSubgroup G,
primaryFixedSubgroup ℓ D hDclosed (H : Subgroup G) = ⊥)