Module

SigmaKernel.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.SigmaKernel

11 declarations indexed from sourceView source ↗

Module documentation

The kernel of the maximal abelian pro-Σ quotient inside an ambient group

Imports3

Imported by3

def

sigmaAbelianizationProjection

L22 ↗

Yamaguchi26AbfaithfulGalois.sigmaAbelianizationProjection

Documentation

The actual composite A → A^Σ → (A^Σ)ᵃᵇ.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

def sigmaAbelianizationProjection (sigma : Set ℕ)
    (A : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A] :
    A →ₜ* TopologicalAbelianization (A ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) A)

theorem

sigmaAbelianizationProjection_apply

L28 ↗

Yamaguchi26AbfaithfulGalois.sigmaAbelianizationProjection_apply

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem sigmaAbelianizationProjection_apply (sigma : Set ℕ)
    (A : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A] (a : A) :
    sigmaAbelianizationProjection sigma A a =
      TopologicalAbelianization.mk _
        (QuotientGroup.mk' (proCResidualCore (FiniteGroupClass.sigmaGroup sigma) A) a)

def

sigmaResidualKernel

L35 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel

Documentation

The manuscript's R_Σ(D), viewed as a subgroup of the ambient group.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

def sigmaResidualKernel {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) : Subgroup G

theorem

sigmaResidualKernel_le

L40 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel_le

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem sigmaResidualKernel_le {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) : sigmaResidualKernel sigma D ≤ (D : Subgroup G)

theorem

mem_sigmaResidualKernel_iff

L46 ↗

Yamaguchi26AbfaithfulGalois.mem_sigmaResidualKernel_iff

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem mem_sigmaResidualKernel_iff {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) (d : (D : Subgroup G)) :
    (d : G) ∈ sigmaResidualKernel sigma D ↔
      sigmaAbelianizationProjection sigma (D : Subgroup G) d = 1

instance

sigmaResidualKernel_normal

L58 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel_normal

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

instance sigmaResidualKernel_normal {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) [(D : Subgroup G).Normal] :
    (sigmaResidualKernel sigma D).Normal

theorem

sigmaResidualKernel_isClosed

L78 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel_isClosed

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem sigmaResidualKernel_isClosed {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) : IsClosed (sigmaResidualKernel sigma D : Set G)

theorem

sigmaResidualKernel_mono

L87 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel_mono

Documentation

The intrinsic residual kernel is functorial for inclusions of closed subgroups.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem sigmaResidualKernel_mono {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (sigma : Set ℕ) (D E : ClosedSubgroup G) (hDE : (D : Subgroup G) ≤ (E : Subgroup G)) :
    sigmaResidualKernel sigma D ≤ sigmaResidualKernel sigma E

theorem

sigmaResidualKernel_iff_primePower_roots

L111 ↗

Yamaguchi26AbfaithfulGalois.sigmaResidualKernel_iff_primePower_roots

Documentation

Elements killed by D → (D^Σ)ᵃᵇ have arbitrarily deep allowed prime-power roots in the topological abelianization of D.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem sigmaResidualKernel_iff_primePower_roots {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) (d : (D : Subgroup G)) :
    (d : G) ∈ sigmaResidualKernel sigma D ↔
      ∀ p : ℕ, p ∈ sigma → p.Prime → ∀ n : ℕ, 0 < n →
        ∃ b : TopologicalAbelianization (D : Subgroup G),
          b ^ (p ^ n) = TopologicalAbelianization.mk (D : Subgroup G) d

theorem

primaryProjection_eq_one_of_mem_sigmaResidualKernel

L129 ↗

Yamaguchi26AbfaithfulGalois.primaryProjection_eq_one_of_mem_sigmaResidualKernel

Documentation

The residual kernel is killed by each allowed primary projection.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem primaryProjection_eq_one_of_mem_sigmaResidualKernel {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) (d : (D : Subgroup G))
    (hd : (d : G) ∈ sigmaResidualKernel sigma D)
    (p : ℕ) [Fact p.Prime] (hp : p ∈ sigma) :
    QuotientGroup.mk' (proCResidualCore (FiniteGroupClass.pGroup p)
      (TopologicalAbelianization (D : Subgroup G)))
        (TopologicalAbelianization.mk (D : Subgroup G) d) = 1

theorem

mem_sigmaResidualKernel_of_primaryProjections

L159 ↗

Yamaguchi26AbfaithfulGalois.mem_sigmaResidualKernel_of_primaryProjections

Documentation

Vanishing of all allowed primary components detects the residual kernel.

Source context 4 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u

Lean source · statement

theorem mem_sigmaResidualKernel_of_primaryProjections {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) (d : (D : Subgroup G))
    (hd : ∀ (p : ℕ) [Fact p.Prime], p ∈ sigma →
      QuotientGroup.mk' (proCResidualCore (FiniteGroupClass.pGroup p)
        (TopologicalAbelianization (D : Subgroup G)))
          (TopologicalAbelianization.mk (D : Subgroup G) d) = 1) :
    (d : G) ∈ sigmaResidualKernel sigma D

Module documentation

The kernel of the maximal abelian pro-Σ quotient inside an ambient group

Declarations