NYLL
Module

DerivedSeriesAndQuotients.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
44 declarations indexed from sourceView source ↗

Module documentation

Closed derived series and solvable quotients

This module defines the closed derived series of a topological group and its maximal finite-step solvable quotients. It also records functoriality, closedness, and normality properties used to compare these quotients under continuous homomorphisms.

Imports6
Imported by11

Declarations

lemma

restrictPreimage_isClosedMap_of_isClosedMap

L30 ↗
TopologicalGroup.restrictPreimage_isClosedMap_of_isClosedMap
Documentation

Closed-map properties descend to the restriction to a subgroup preimage.

Source context 2 commands

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

universe u v
namespace TopologicalGroup
Lean source · statement
lemma restrictPreimage_isClosedMap_of_isClosedMap
    {G : Type u} [TopologicalSpace G] [Group G]
    {Q : Type v} [TopologicalSpace Q] [Group Q]
    (π : G →ₜ* Q) (Q₁ : Subgroup Q)
    (hπ : IsClosedMap π)
    (hQ₁ : IsClosed (Q₁ : Set Q)) :
    IsClosedMap (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁)
lemma

map_closure_le_of_map_le

L65 ↗
TopologicalGroup.map_closure_le_of_map_le
Documentation

If the image of a subgroup is contained in a closed subgroup, then the image of its closure is contained there as well.

Source context 2 commands

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

universe u v
namespace TopologicalGroup
Lean source · statement
lemma map_closure_le_of_map_le
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q]
    {G₁ : Subgroup G} {Q₁ : Subgroup Q} {f : G →ₜ* Q}
    (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
    (hclosed : IsClosed (Q₁ : Set Q)) :
    (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁
lemma

map_closure_le_closure

L82 ↗
TopologicalGroup.map_closure_le_closure
Documentation

The image of a closure is contained in the closure of the image.

Source context 2 commands

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

universe u v
namespace TopologicalGroup
Lean source · statement
lemma map_closure_le_closure
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {G₁ : Subgroup G} {Q₁ : Subgroup Q} (f : G →ₜ* Q)
    (h₁ : G₁.map (f : G →* Q) ≤ Q₁) :
    (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁.topologicalClosure
lemma

isClosed_map_of_isClosedMap

L94 ↗
TopologicalGroup.isClosed_map_of_isClosedMap
Documentation

Closed maps send closed subgroups to closed images.

Source context 2 commands

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

universe u v
namespace TopologicalGroup
Lean source · statement
lemma isClosed_map_of_isClosedMap
    {G : Type u} [TopologicalSpace G] [Group G]
    {H : Type v} [TopologicalSpace H] [Group H]
    (f : G →ₜ* H) (hclosed : IsClosedMap f)
    (K : Subgroup G) (hK : IsClosed (K : Set G)) :
    IsClosed (((K.map (f : G →* H) : Subgroup H) : Set H))
lemma

ker_map_eq_bot_of_comap_eq

L108 ↗
TopologicalGroup.ker_map_eq_bot_of_comap_eq
Documentation

The kernel of the induced map is trivial under the stated comap equality hypothesis.

Source context 2 commands

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

universe u v
namespace TopologicalGroup
Lean source · statement
lemma ker_map_eq_bot_of_comap_eq
    {G : Type u} [Group G]
    {H : Type v} [Group H]
    {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (f : G →* H) (h : N ≤ M.comap f) (hcomap : M.comap f = N) :
    (QuotientGroup.map (N := N) (M := M) (f := f) h).ker = ⊥
theorem

isMulTorsionFree

L129 ↗
MulEquiv.isMulTorsionFree
Documentation

Multiplicative equivalences transport torsion-freeness.

Source context 2 commands

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

universe u v
namespace MulEquiv
Lean source · statement
theorem isMulTorsionFree
    {M : Type u} [Monoid M]
    {N : Type v} [Monoid N]
    (e : M ≃* N) [IsMulTorsionFree M] :
    IsMulTorsionFree N
abbrev

closedCommutator

L141 ↗
ProCGroups.FiniteStepSolvableQuotients.closedCommutator
Documentation

The closed commutator subgroup of a topological group.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev closedCommutator
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (H K : Subgroup G) : Subgroup G
def

closedDerivedSeries

L147 ↗
ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries
Documentation

The closed derived series starting from a subgroup.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · full declaration
def closedDerivedSeries
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (K : Subgroup G) : ℕ → Subgroup G
  | 0 => K
  | n + 1 => closedCommutator (closedDerivedSeries K n) (closedDerivedSeries K n)
abbrev

topDerivedTop

L154 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop
Documentation

The mth closed derived subgroup of the whole topological group G.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev topDerivedTop
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) : Subgroup G
instance

topDerivedTop_isClosedInst

L160 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_isClosedInst
Documentation

Every term in the closed derived series of G is a closed subgroup.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
instance topDerivedTop_isClosedInst
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ} :
    IsClosed (topDerivedTop G m : Set G)
instance

topDerivedTop_normalInst

L173 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_normalInst
Documentation

Every term in the closed derived series of G is a normal subgroup.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
instance topDerivedTop_normalInst
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ} :
    (topDerivedTop G m).Normal
abbrev

MaxSolvQuot

L186 ↗
ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot
Documentation

The quotient by the mth closed derived subgroup.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev MaxSolvQuot
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) : Type u
abbrev

toMaxSolvQuot

L192 ↗
ProCGroups.FiniteStepSolvableQuotients.toMaxSolvQuot
Documentation

The natural quotient map to the maximal \(m\)-step solvable quotient.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev toMaxSolvQuot
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) :
    G →* MaxSolvQuot G m
abbrev

continuousToMaxSolvQuot

L199 ↗
ProCGroups.FiniteStepSolvableQuotients.continuousToMaxSolvQuot
Documentation

The natural quotient map as a continuous homomorphism.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev continuousToMaxSolvQuot
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) :
    G →ₜ* MaxSolvQuot G m
abbrev

preimageOpenSubgroup

L207 ↗
ProCGroups.FiniteStepSolvableQuotients.preimageOpenSubgroup
Documentation

The preimage open subgroup induced by a continuous homomorphism.

Source context 2 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
abbrev preimageOpenSubgroup
    {G : Type u} [TopologicalSpace G] [Group G]
    {Q : Type v} [TopologicalSpace Q] [Group Q]
    (f : G →ₜ* Q) (H : OpenSubgroup Q) : OpenSubgroup G
lemma

closedDerivedSeries_zero

L223 ↗
ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries_zero
Documentation

The zeroth closed derived subgroup is the whole topological group.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma closedDerivedSeries_zero
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (K : Subgroup G) :
    closedDerivedSeries (G := G) K 0 = K
lemma

closedDerivedSeries_succ

L232 ↗
ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries_succ
Documentation

The successor closed derived subgroup is the closed commutator subgroup of the previous derived stage.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma closedDerivedSeries_succ
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (K : Subgroup G) (n : ℕ) :
    closedDerivedSeries (G := G) K (n + 1) =
      ⁅closedDerivedSeries (G := G) K n, closedDerivedSeries (G := G) K n⁆ₜ
lemma

topDerivedTop_zero

L239 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_zero
Documentation

The zeroth term of the ambient closed derived series is the whole ambient group.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma topDerivedTop_zero
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    G⟦0⟧ₜ = (⊤ : Subgroup G)
lemma

topDerivedTop_succ

L247 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_succ
Documentation

The successor term of the ambient closed derived series is the closed commutator subgroup of the previous term.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma topDerivedTop_succ
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (n : ℕ) :
    G⟦n + 1⟧ₜ = ⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ
theorem

closedCommutator_map_mono

L253 ↗
ProCGroups.FiniteStepSolvableQuotients.closedCommutator_map_mono
Documentation

Closed commutators map monotonically under continuous homomorphisms.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem closedCommutator_map_mono
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
    (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
    (h₂ : G₂.map (f : G →* Q) ≤ Q₂) :
    (⁅G₁, G₂⁆ₜ).map (f : G →* Q) ≤ ⁅Q₁, Q₂⁆ₜ
lemma

commutator_le_map_closedCommutator

L273 ↗
ProCGroups.FiniteStepSolvableQuotients.commutator_le_map_closedCommutator
Documentation

If target subgroups lie in the corresponding images, then their commutator lies in the image of the source closed commutator.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma commutator_le_map_closedCommutator
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [Group Q]
    (φ : G →* Q)
    {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q}
    (h₁ : Q₁ ≤ G₁.map φ) (h₂ : Q₂ ≤ G₂.map φ) :
    ⁅Q₁, Q₂⁆ ≤ (⁅G₁, G₂⁆ₜ).map φ
theorem

map_closedCommutator_eq_of_map_eq

L294 ↗
ProCGroups.FiniteStepSolvableQuotients.map_closedCommutator_eq_of_map_eq
Documentation

The map carries the closed commutator subgroup to the corresponding closed commutator subgroup under the stated equality hypothesis.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem map_closedCommutator_eq_of_map_eq
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
    (h₁ : G₁.map (f : G →* Q) = Q₁)
    (h₂ : G₂.map (f : G →* Q) = Q₂)
    (hclosed : IsClosed (((⁅G₁,G₂⁆ₜ).map (f : G →* Q) : Subgroup Q) : Set Q)) :
    (⁅G₁, G₂⁆ₜ).map (f : G →* Q) = ⁅Q₁, Q₂⁆ₜ
theorem

closedCommutator_topologicallyCharacteristic

L322 ↗
ProCGroups.FiniteStepSolvableQuotients.closedCommutator_topologicallyCharacteristic
Documentation

Closed commutators of topologically characteristic subgroups are again topologically characteristic.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem closedCommutator_topologicallyCharacteristic
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (G₁ G₂ : Subgroup G)
    (h₁ : G₁.TopologicallyCharacteristic)
    (h₂ : G₂.TopologicallyCharacteristic) :
    (⁅G₁, G₂⁆ₜ).TopologicallyCharacteristic
lemma

topDerived_add

L335 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerived_add
Documentation

Restarting the ambient closed derived series adds indices.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma topDerived_add
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m n : ℕ) :
    closedDerivedSeries (G := G) (G⟦m⟧ₜ) n = G⟦m + n⟧ₜ
theorem

topDerivedTop_antitone

L348 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_antitone
Documentation

The ambient closed derived series is antitone.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerivedTop_antitone
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    Antitone (topDerivedTop G)
instance

topDerivedTop_topologicallyCharacteristicInst

L362 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_topologicallyCharacteristicInst
Documentation

Every stage of the ambient closed derived series is topologically characteristic.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
instance topDerivedTop_topologicallyCharacteristicInst
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ} :
    (topDerivedTop G m).TopologicallyCharacteristic
theorem

topDerived_map_le

L378 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerived_map_le
Documentation

The closed derived series is monotone under continuous homomorphisms.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerived_map_le
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) (m : ℕ) :
    (G⟦m⟧ₜ).map (f : G →* Q) ≤ Q⟦m⟧ₜ
lemma

topDerivedTop_le_comap

L402 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_le_comap
Documentation

The ambient closed derived series pulls back along continuous homomorphisms.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma topDerivedTop_le_comap
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) (m : ℕ) :
    G⟦m⟧ₜ ≤ (Q⟦m⟧ₜ).comap (f : G →* Q)
theorem

mem_topDerived_one_of_mem_topDerived_of_le

L413 ↗
ProCGroups.FiniteStepSolvableQuotients.mem_topDerived_one_of_mem_topDerived_of_le
Documentation

A point in the ambient \(m\)-th derived subgroup lies in the first derived subgroup of any larger subgroup containing the \((m-1)\)-st derived term.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem mem_topDerived_one_of_mem_topDerived_of_le
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {K : Subgroup G} {m : ℕ} (hm : 1 ≤ m)
    (hK : G⟦m - 1⟧ₜ ≤ K)
    {x : G} (hx : x ∈ G⟦m⟧ₜ) :
    x ∈ closedDerivedSeries (G := G) K 1
theorem

topDerived_one_map_subtype_eq_of_isClosed_subgroup

L437 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerived_one_map_subtype_eq_of_isClosed_subgroup
Documentation

The first derived subgroup of a closed subgroup maps back to the corresponding subgroup of the ambient group.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerived_one_map_subtype_eq_of_isClosed_subgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Subgroup G} {K : Subgroup H} (hH : IsClosed (H : Set G)) :
    (closedDerivedSeries (G := H) K 1).map H.subtype =
      closedDerivedSeries (G := G) (K.map H.subtype) 1
theorem

topDerived_map_eq_of_surj

L466 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerived_map_eq_of_surj
Documentation

Surjective maps identify the stagewise closed derived subgroups once the commutator images are closed.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerived_map_eq_of_surj
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) (hf : Function.Surjective f)
    (hclosed_comm :
      ∀ n : ℕ,
        IsClosed (((⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H) : Subgroup H) : Set H))
    (n : ℕ) :
    (G⟦n⟧ₜ).map (f : G →* H) = H⟦n⟧ₜ
theorem

closedCommutator_topDerived_map_isClosed_of_compact

L509 ↗
ProCGroups.FiniteStepSolvableQuotients.closedCommutator_topDerived_map_isClosed_of_compact
Documentation

Images of closed commutators of derived terms are closed when the source is compact and the target is Hausdorff.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem closedCommutator_topDerived_map_isClosed_of_compact
    {G H : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TopologicalSpace H] [Group H] [T2Space H]
    (f : G →ₜ* H) (n : ℕ) :
    IsClosed
      (((closedCommutator (topDerivedTop G n) (topDerivedTop G n)).map
        (f : G →* H) : Subgroup H) : Set H)
theorem

closedDerivedSeries_mono

L526 ↗
ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries_mono
Documentation

The closed derived series is monotone in the initial subgroup.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem closedDerivedSeries_mono
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {K L : Subgroup G} (hKL : K ≤ L) (n : ℕ) :
    closedDerivedSeries (G := G) K n ≤ closedDerivedSeries (G := G) L n
theorem

topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup

L554 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup
Documentation

The internal derived series of a closed subgroup maps to the corresponding ambient derived series.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Subgroup G} (hH : IsClosed (H : Set G)) (n : ℕ) :
    (topDerivedTop H n).map H.subtype =
      closedDerivedSeries (G := G) H n
theorem

topDerivedTop_le_openSubgroup_pred_map_of_first_le

L594 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_le_openSubgroup_pred_map_of_first_le
Documentation

Higher ambient derived terms lie in the corresponding derived term of any open subgroup containing the first derived term.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerivedTop_le_openSubgroup_pred_map_of_first_le
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (H : OpenSubgroup G) {m : ℕ} (hm : 1 ≤ m)
    (hfirst : topDerivedTop G 1 ≤ (H : Subgroup G)) :
    topDerivedTop G m ≤
      (topDerivedTop ↥(H : Subgroup G) (m - 1)).map
        (Subgroup.subtype (H : Subgroup G))
theorem

eq_one_of_mem_all_openNormalSubgroup_derived

L627 ↗
ProCGroups.FiniteStepSolvableQuotients.eq_one_of_mem_all_openNormalSubgroup_derived
Documentation

If a profinite element projects into all open-normal derived lifts and the corresponding ambient derived term is trivial, then the element is trivial.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem eq_one_of_mem_all_openNormalSubgroup_derived
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    {m : ℕ} (hm : 3 ≤ m)
    (hQm : topDerivedTop Q m = ⊥)
    {d : Q}
    (hproj :
      ∀ H : OpenNormalSubgroup Q,
        topDerivedTop Q 1 ≤ (H : Subgroup Q) →
        d ∈ (topDerivedTop ↥(H : Subgroup Q) (m - 1)).map
          (Subgroup.subtype (H : Subgroup Q))) :
    d = 1
theorem

topDerivedTop_one_eq_bot_of_topologicallyGenerates_singleton

L779 ↗
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_one_eq_bot_of_topologicallyGenerates_singleton
Documentation

Topological cyclic generation forces the first derived term to be trivial.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem topDerivedTop_one_eq_bot_of_topologicallyGenerates_singleton
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [T2Space Q] (x : Q)
    (hgen : ProCGroups.Generation.TopologicallyGenerates (G := Q) ({x} : Set Q)) :
    topDerivedTop Q 1 = ⊥
def

topMaxSolvQuotMap

L834 ↗
ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap
Documentation

The induced map on maximal finite-step solvable quotients.

Source context 6 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
def topMaxSolvQuotMap
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) (m : ℕ) :
    (G^ₘ m) →ₜ* (Q^ₘ m)
def

restrictPreimage_topMaxSolvQuot_mulEquiv

L850 ↗
ProCGroups.FiniteStepSolvableQuotients.TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
Documentation

The induced map on finite-step solvable quotients is an equivalence under surjectivity and the required kernel containment for the subgroup preimage.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
def TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {π : G →ₜ* Q} {Q₁ : Subgroup Q} {m : ℕ}
    (hπ : Function.Surjective π)
    (hclosed : IsClosedMap (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁))
    (hker :
      (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁).ker ≤
        topDerivedTop ↥(Q₁.comap (π : G →* Q)) m) :
    MaxSolvQuot (Q₁.comap (π : G →* Q)) m ≃* MaxSolvQuot Q₁ m
lemma

continuousToMaxSolvQuot_surjective

L928 ↗
ProCGroups.FiniteStepSolvableQuotients.continuousToMaxSolvQuot_surjective
Documentation

The quotient map to the maximal \(m\)-step solvable quotient is surjective.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
lemma continuousToMaxSolvQuot_surjective
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) :
    Function.Surjective (continuousToMaxSolvQuot G m)
theorem

continuousToMaxSolvQuot_eq_one_iff

L936 ↗
ProCGroups.FiniteStepSolvableQuotients.continuousToMaxSolvQuot_eq_one_iff
Documentation

The quotient map kills exactly the \(m\)-th closed derived subgroup.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem continuousToMaxSolvQuot_eq_one_iff
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ} {x : G} :
    continuousToMaxSolvQuot G m x = 1 ↔ x ∈ topDerivedTop G m
theorem

continuousToMaxSolvQuot_ker_le_topDerived_one_map_subtype_of_le

L947 ↗
ProCGroups.FiniteStepSolvableQuotients.continuousToMaxSolvQuot_ker_le_topDerived_one_map_subtype_of_le
Documentation

The kernel of the ambient quotient map lands in the first closed derived subgroup of any preimage open subgroup containing the previous derived term.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem continuousToMaxSolvQuot_ker_le_topDerived_one_map_subtype_of_le
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ} (hm : 1 ≤ m)
    (H : OpenSubgroup (MaxSolvQuot G m))
    (hH :
      topDerivedTop G (m - 1) ≤
        ((H : Subgroup (MaxSolvQuot G m)).comap
          (continuousToMaxSolvQuot G m : G →* MaxSolvQuot G m))) :
    (continuousToMaxSolvQuot G m : G →* MaxSolvQuot G m).ker ≤
      (topDerivedTop
          ↥((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
            Subgroup G) 1).map
        (Subgroup.subtype
          ((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
            Subgroup G))
theorem

isMulTorsionFree_maxSolvQuot_one_of_isMulTorsionFree_topologicalAbelianization

L1006 ↗
ProCGroups.FiniteStepSolvableQuotients.isMulTorsionFree_maxSolvQuot_one_of_isMulTorsionFree_topologicalAbelianization
Documentation

The first maximal solvable quotient is the topological abelianization.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem isMulTorsionFree_maxSolvQuot_one_of_isMulTorsionFree_topologicalAbelianization
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hG : IsMulTorsionFree (TopologicalAbelianization G)) :
    IsMulTorsionFree (MaxSolvQuot G 1)
theorem

preimageOpenSubgroup_maxSolvQuot_mulEquiv_of_ker_le

L1017 ↗
ProCGroups.FiniteStepSolvableQuotients.preimageOpenSubgroup_maxSolvQuot_mulEquiv_of_ker_le
Documentation

The induced map between maximal finite-step solvable quotients of a subgroup preimage and the target subgroup is an isomorphism under the expected kernel bound.

Source context 8 commands

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

universe u v
namespace ProCGroups.FiniteStepSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.closedCommutator H K
scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
  ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G m
scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
  ProCGroups.FiniteStepSolvableQuotients.MaxSolvQuot G m
open scoped ProCGroupsSolvableQuotients
scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
  ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap f m
open scoped ProCGroupsSolvableQuotients
Lean source · statement
theorem preimageOpenSubgroup_maxSolvQuot_mulEquiv_of_ker_le
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (f : G →ₜ* Q) (hf : Function.Surjective f) (H : OpenSubgroup Q)
    (hclosed : IsClosedMap (ProCGroups.ContinuousMonoidHom.restrictPreimage f (H : Subgroup Q)))
    (n : ℕ)
    (hker :
      f.ker ≤
        (topDerivedTop
          ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n).map
            (Subgroup.subtype
              ((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G))) :
    Nonempty
      (MaxSolvQuot ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n ≃*
        MaxSolvQuot ↥(H : Subgroup Q) n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.