NYLL
Module

SolvableQuotients.lean

Nyll.ProCGroups.FreeProC.SolvableQuotients
6 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Free pro-C / Solvable Quotients

This module transports free pro-\(C\) data to finite-step solvable quotients and their derived-series constructions.

Imports2
Imported by1

Declarations

def

collapseToFinsetQuot

L32 ↗
ProCGroups.FreeProC.collapseToFinsetQuot
Documentation

The endomorphism induced by collapseToFinset on a maximal solvable quotient.

Source context 9 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
def collapseToFinsetQuot
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    (S : Finset ι) (m : ℕ) :
    MaxSolvQuot F m →ₜ* MaxSolvQuot F m
theorem

comp_collapseToFinsetQuot_eq_of_eq_one_outside

L45 ↗
ProCGroups.FreeProC.comp_collapseToFinsetQuot_eq_of_eq_one_outside
Documentation

On the quotient, composing with \(\mathrm{collapseToFinsetQuot}\) leaves a map that is trivial outside \(S\) unchanged.

Source context 10 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)] in
Lean source · statement
theorem comp_collapseToFinsetQuot_eq_of_eq_one_outside
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    {H : Type w} [TopologicalSpace H] [Group H] [T2Space H]
    (S : Finset ι) (m : ℕ) (φ : MaxSolvQuot F m →ₜ* H)
    (hφ : ∀ j, j ∉ S → φ (continuousToMaxSolvQuot F m (X j)) = 1) :
    φ.comp (collapseToFinsetQuot X hFree S m) = φ
def

finsetSupportRangeQuot

L69 ↗
ProCGroups.FreeProC.finsetSupportRangeQuot
Documentation

The map from the original maximal solvable quotient to the maximal solvable quotient of the finite-support retract.

Source context 9 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
def finsetSupportRangeQuot
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    (S : Finset ι) (m : ℕ) :
    MaxSolvQuot F m →ₜ* MaxSolvQuot (hFree.FinsetSupportRetract S) m
def

finsetSupportInclusionQuot

L81 ↗
ProCGroups.FreeProC.finsetSupportInclusionQuot
Documentation

The map from the maximal solvable quotient of the finite-support retract to the original maximal solvable quotient.

Source context 9 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
def finsetSupportInclusionQuot
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    (S : Finset ι) (m : ℕ) :
    MaxSolvQuot (hFree.FinsetSupportRetract S) m →ₜ* MaxSolvQuot F m
theorem

finsetSupportRangeQuot_apply

L94 ↗
ProCGroups.FreeProC.finsetSupportRangeQuot_apply
Documentation

The quotient map induced by the finite-support retraction sends the class of x to the class of its collapsed finite-support image.

Source context 10 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)] in
Lean source · statement
theorem finsetSupportRangeQuot_apply
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    (S : Finset ι) (m : ℕ) (x : F) :
    finsetSupportRangeQuot X hFree S m (continuousToMaxSolvQuot F m x) =
      continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m
        (hFree.collapseToFinsetRange S x)
theorem

finsetSupportInclusionQuot_apply

L120 ↗
ProCGroups.FreeProC.finsetSupportInclusionQuot_apply
Documentation

The quotient map induced by inclusion of the finite-support retract sends the class of x to the class of its image in the original free pro-\(C\) group.

Source context 10 commands

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

open scoped Topology
namespace ProCGroups.FreeProC
open ProCGroups.FiniteStepSolvableQuotients
universe u v w
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)] in
Lean source · statement
theorem finsetSupportInclusionQuot_apply
    {ι : Type v} [DecidableEq ι] (X : ι → F)
    (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) ι F X)
    (S : Finset ι) (m : ℕ) (x : hFree.FinsetSupportRetract S) :
    finsetSupportInclusionQuot X hFree S m
        (continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m x) =
      continuousToMaxSolvQuot F m (hFree.collapseToFinsetInclusion S x)

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