Module

Theorem6Dot5GroupCriterion.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot5GroupCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Finite-step solvable quotients of an ab-faithful group

Yamaguchi, arXiv:2610.05634v1, Corollary 6.5. Each orientation satisfies formal Hilbert 90 on every open subgroup.

Imports5

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.RelativeDerivedCriterion
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.Faithful
Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
Nyll.ProCGroups.Topologies.OpenSubgroup
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Imported by3

theorem

finiteStepSolvable_centerfree_and_slim_of_formalHilbert90

L26 ↗

Yamaguchi26AbfaithfulGalois.finiteStepSolvable_centerfree_and_slim_of_formalHilbert90

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem finiteStepSolvable_centerfree_and_slim_of_formalHilbert90
    (G : ProfiniteGrp.{u})
    (hG : IsAbFaithful G)
    (hOrient : ∀ (ℓ : ℕ) [Fact ℓ.Prime],
      ∃ θ : Orientation ℓ G, FormalHilbert90 θ) :
    (∀ m : ℕ, 2 ≤ m → Subgroup.center (MaxSolvQuot G m) = ⊥) ∧
      ((∀ (ℓ : ℕ) [Fact ℓ.Prime],
        ∃ θ : Orientation ℓ G,
          FormalHilbert90 θ ∧ Set.Infinite (Set.range θ)) →
        ∀ m : ℕ, 2 ≤ m → IsSlim (MaxSolvQuot G m))

Module documentation

Finite-step solvable quotients of an ab-faithful group

Declarations

finiteStepSolvable_centerfree_and_slim_of_formalHilbert90