Module

SigmaFixedPoints.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.SigmaFixedPoints

2 declarations indexed from sourceView source ↗

Module documentation

Fixed primary classes in sigma quotients

Centralizing classes in sigma-residual quotients project to fixed primary classes for primes in sigma. Vanishing of those fixed classes forces the centralizing quotient class to be trivial.

Imports2

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.SigmaKernel
Mathlib.GroupTheory.Subgroup.Centralizer

Imported by2

theorem

primaryProjection_mem_fixed_of_sigmaQuotient_centralizes

L23 ↗

Yamaguchi26AbfaithfulGalois.primaryProjection_mem_fixed_of_sigmaQuotient_centralizes

Source context 4 commands

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

open scoped commutatorElement
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.Abelian ProCGroups.ProC
universe u

Lean source · statement

theorem primaryProjection_mem_fixed_of_sigmaQuotient_centralizes {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (sigma : Set ℕ) (D : ClosedSubgroup G) [(D : Subgroup G).Normal]
    (H : Subgroup G) (d : (D : Subgroup G))
    (hd : QuotientGroup.mk' (sigmaResidualKernel sigma D) (d : G) ∈
      Subgroup.centralizer (H.map (QuotientGroup.mk' (sigmaResidualKernel sigma D)) :
        Set (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) ∈
          primaryFixedSubgroup p (D : Subgroup G) D.isClosed' H

theorem

sigmaQuotient_eq_one_of_primaryFixed_eq_bot

L47 ↗

Yamaguchi26AbfaithfulGalois.sigmaQuotient_eq_one_of_primaryFixed_eq_bot