Module

Abelianization.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.Abelianization

11 declarations indexed from sourceView source ↗

Module documentation

Abelianizations inside finite-step solvable quotients

This module studies the last closed-derived subgroup of a maximal solvable quotient and formulates torsion-freeness and containment conditions using abelianizations of its open subgroups.

Imports3

Imported by4

def

lastDerivedSubgroup

L27 ↗

ProCGroups.FiniteStepSolvableQuotients.lastDerivedSubgroup

Documentation

The last nontrivial closed derived term inside the maximal \(m\)-step solvable quotient.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

def lastDerivedSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) : Subgroup (MaxSolvQuot G m)

def

aboveLastDerived

L33 ↗

ProCGroups.FiniteStepSolvableQuotients.aboveLastDerived

Documentation

An open subgroup of the maximal \(m\)-step solvable quotient contains the last derived term.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

def aboveLastDerived
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ) (H : OpenSubgroup (MaxSolvQuot G m)) : Prop

def

containsLastDerived

L42 ↗

ProCGroups.FiniteStepSolvableQuotients.containsLastDerived

Documentation

An open normal subgroup inside an open subgroup of the maximal \(m\)-step solvable quotient contains the last derived term.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

def containsLastDerived
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (m : ℕ)
    (H : OpenSubgroup (MaxSolvQuot G m))
    (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))) : Prop

theorem

containsLastDerived_iff_lastDerivedSubgroup_le_map_subtype

L54 ↗

ProCGroups.FiniteStepSolvableQuotients.containsLastDerived_iff_lastDerivedSubgroup_le_map_subtype

Documentation

\(\mathrm{ContainsLastDerived}\) is the intrinsic form of saying that the ambient image of \(N\) contains the last derived subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem containsLastDerived_iff_lastDerivedSubgroup_le_map_subtype
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ}
    {H : OpenSubgroup (MaxSolvQuot G m)}
    {N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))} :
    containsLastDerived (G := G) m H N ↔
      lastDerivedSubgroup (G := G) m ≤
        (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
          ((H : Subgroup (MaxSolvQuot G m)).subtype)

theorem

containsLastDerived_of_lastDerivedSubgroup_le_map_subtype

L84 ↗

ProCGroups.FiniteStepSolvableQuotients.containsLastDerived_of_lastDerivedSubgroup_le_map_subtype

Documentation

The quotient contains the last derived subgroup under the stated map-subtype containment hypothesis.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem containsLastDerived_of_lastDerivedSubgroup_le_map_subtype
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {m : ℕ}
    {H : OpenSubgroup (MaxSolvQuot G m)}
    {N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m))}
    (hN :
      lastDerivedSubgroup (G := G) m ≤
        (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
          ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
    containsLastDerived (G := G) m H N

theorem

injective_topologicalAbelianizationMk_of_topologicalCommutator_eq_bot

L102 ↗

ProCGroups.FiniteStepSolvableQuotients.injective_topologicalAbelianizationMk_of_topologicalCommutator_eq_bot

Documentation

Trivial closed commutator subgroup makes the natural map to topological abelianization injective.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem injective_topologicalAbelianizationMk_of_topologicalCommutator_eq_bot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hcomm : topologicalCommutator G = ⊥) :
    Function.Injective (TopologicalAbelianization.mk G)

theorem

injective_topologicalAbelianizationMk_of_topDerivedTop_one_eq_bot

L113 ↗

ProCGroups.FiniteStepSolvableQuotients.injective_topologicalAbelianizationMk_of_topDerivedTop_one_eq_bot

Documentation

Trivial first closed derived subgroup makes the natural map to topological abelianization injective.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem injective_topologicalAbelianizationMk_of_topDerivedTop_one_eq_bot
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hder : topDerivedTop G 1 = ⊥) :
    Function.Injective (TopologicalAbelianization.mk G)

theorem

topDerivedTop_one_eq_bot_of_closedDerivedSeries_eq_bot

L124 ↗

ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_one_eq_bot_of_closedDerivedSeries_eq_bot

Documentation

If the first closed derived subgroup of a closed subgroup vanishes in the ambient group, then the subgroup has trivial first closed derived subgroup internally as well.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem topDerivedTop_one_eq_bot_of_closedDerivedSeries_eq_bot
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q))
    (hstep : closedDerivedSeries (G := Q) K 1 = ⊥) :
    topDerivedTop K 1 = ⊥

theorem

topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one

L161 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one

Documentation

The kernel of the canonical topological abelianization map is the first closed derived subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    ProCGroups.ProC.ProfiniteKernelSubgroup
        (TopologicalAbelianization.mkₜ G) =
      topDerivedTop G 1

theorem

topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two

L176 ↗

ProCGroups.FiniteStepSolvableQuotients.topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two

Documentation

Mapping the first closed derived subgroup of the topological abelianization kernel back into the ambient group gives the second closed derived subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · full declaration

theorem topologicalAbelianization_kernel_closedDerivedSeries_one_map_subtype_eq_topDerivedTop_two
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    let N : Subgroup G :=
      ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
    (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
      topDerivedTop G 2 := by
  let N : Subgroup G :=
    ProCGroups.ProC.ProfiniteKernelSubgroup (TopologicalAbelianization.mkₜ G)
  have hN_eq : N = topDerivedTop G 1 :=
    topologicalAbelianization_profiniteKernelSubgroup_eq_topDerivedTop_one G
  have hNmap : (⊤ : Subgroup N).map N.subtype = topDerivedTop G 1 := by
    ext y
    constructor
    · rintro ⟨z, -, rfl⟩
      change (z : G) ∈ topDerivedTop G 1
      exact hN_eq ▸ z.2
    · intro hy
      refine ⟨⟨y, hN_eq.symm ▸ hy⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
  have hmap :
      (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
        closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := by
    exact
      topDerived_one_map_subtype_eq_of_isClosed_subgroup
        (G := G) (H := N) (K := (⊤ : Subgroup N))
        (by
          simpa [N] using
            ProCGroups.ProC.isClosed_profiniteKernelSubgroup
              (TopologicalAbelianization.mkₜ G))
  calc
    (closedDerivedSeries (G := N) (⊤ : Subgroup N) 1).map N.subtype =
        closedDerivedSeries (G := G) ((⊤ : Subgroup N).map N.subtype) 1 := hmap
    _ = closedDerivedSeries (G := G) (topDerivedTop G 1) 1 := by rw [hNmap]
    _ = topDerivedTop G 2 := by
      change closedDerivedSeries (G := G) (topDerivedTop G 1) 1 = topDerivedTop G (1 + 1)
      exact topDerived_add (G := G) (m := 1) (n := 1)

theorem

mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel

L216 ↗

ProCGroups.FiniteStepSolvableQuotients.mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel

Documentation

Membership in the second closed derived subgroup is equivalent to membership in the closed commutator of the canonical topological abelianization kernel.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u

Lean source · statement

theorem mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {a : G}
    (haψ : TopologicalAbelianization.mkₜ G a = 1) :
    a ∈ topDerivedTop G 2 ↔
      (⟨a, haψ⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup
        (TopologicalAbelianization.mkₜ G)) ∈
        Subgroup.closedCommutator
          (ProCGroups.ProC.ProfiniteKernelSubgroup
            (TopologicalAbelianization.mkₜ G))

Module documentation

Abelianizations inside finite-step solvable quotients

Declarations