NYLL
Module

ResidualPowerDetection.lean

Nyll.ProCGroups.ProC.MaximalQuotients.ResidualPowerDetection
3 declarations indexed from sourceView source ↗

Module documentation

Detection of the pro-Sigma residual core by powers

Finite groups annihilated by a Sigma-number lie in the finite Sigma class. Conversely, an element admitting an n-th root for every positive Sigma-number vanishes in every finite Sigma quotient of every pro-Sigma quotient, hence belongs to the actual residual core.

Imports4
Imported by2

Declarations

theorem

sigmaGroup_of_pow_eq_one

L27 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_of_pow_eq_one
Documentation

Cauchy's theorem detects every prime divisor of a finite group's order among the prime divisors of an annihilating exponent.

Source context 2 commands

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

namespace ProCGroups
universe u v
Lean source · statement
theorem FiniteGroupClass.sigmaGroup_of_pow_eq_one
    {H : Type u} [Group H] [Finite H] (sigma : Set ℕ) (n : ℕ)
    (hn : FiniteGroupClass.IsSigmaNumber sigma n) (hpow : ∀ x : H, x ^ n = 1) :
    FiniteGroupClass.sigmaGroup sigma H
theorem

proCResidualCore_le_ker_of_finite_exponent

L43 ↗
ProCGroups.ProC.proCResidualCore_le_ker_of_finite_exponent
Documentation

The residual core is killed by any continuous finite target whose exponent is a Sigma-number, even when source and target have different universes.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace ProC
Lean source · statement
theorem proCResidualCore_le_ker_of_finite_exponent
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H] [Finite H]
    (sigma : Set ℕ) (phi : G →ₜ* H) (n : ℕ)
    (hn : FiniteGroupClass.IsSigmaNumber sigma n) (hpow : ∀ x : H, x ^ n = 1) :
    proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G ≤ phi.toMonoidHom.ker
theorem

mem_proCResidualCore_of_forall_sigmaPower

L67 ↗
ProCGroups.ProC.mem_proCResidualCore_of_forall_sigmaPower
Documentation

An element having all positive Sigma-number roots lies in the actual pro-Sigma residual core. No comparison of quotients is an extra hypothesis.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace ProC
Lean source · statement
theorem mem_proCResidualCore_of_forall_sigmaPower
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
    (sigma : Set ℕ) (g : G)
    (hg : ∀ n : ℕ, 0 < n → FiniteGroupClass.IsSigmaNumber sigma n →
      ∃ a : G, a ^ n = g) :
    g ∈ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G

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