Module

RelativeFixedPoints.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.RelativeFixedPoints

4 declarations indexed from sourceView source ↗

Module documentation

Relative derived quotients and fixed primary classes

Centralizing classes in relative derived quotients yield fixed primary abelianization classes. Vanishing of these fixed classes forces the centralizing quotient class to be trivial.

Imports4

Imported by2

theorem

relativeDerived_mem_iff

L25 ↗

Yamaguchi26AbfaithfulGalois.relativeDerived_mem_iff

Source context 4 commands

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

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

Lean source · statement

theorem relativeDerived_mem_iff
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) (hD : IsClosed (D : Set G)) (d : D) :
    (d : G) ∈ relativeDerived D ↔ TopologicalAbelianization.mk D d = 1

theorem

relativeDerived_quotient_mem_openNormal_of_centralizes

L39 ↗

Yamaguchi26AbfaithfulGalois.relativeDerived_quotient_mem_openNormal_of_centralizes

Source context 4 commands

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

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

Lean source · statement

theorem relativeDerived_quotient_mem_openNormal_of_centralizes
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) [D.Normal]
    (N : OpenNormalSubgroup G) (hDN : D ≤ (N : Subgroup G))
    (hN : Function.Injective
      (quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G))))
    (x : G)
    (hx : QuotientGroup.mk' (relativeDerived D) x ∈
      Subgroup.centralizer (((N : Subgroup G).map
        (QuotientGroup.mk' (relativeDerived D))) : Set (RelativeDerivedQuotient D))) :
    x ∈ (N : Subgroup G)

theorem

primaryAbelianization_mk_mem_fixed_of_quotient_centralizes

L70 ↗

Yamaguchi26AbfaithfulGalois.primaryAbelianization_mk_mem_fixed_of_quotient_centralizes

Source context 4 commands

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

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

Lean source · statement

theorem primaryAbelianization_mk_mem_fixed_of_quotient_centralizes
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
    (H : Subgroup G) (d : D)
    (hd : QuotientGroup.mk' (relativeDerived D) (d : G) ∈
      Subgroup.centralizer (H.map (QuotientGroup.mk' (relativeDerived D)) :
        Set (RelativeDerivedQuotient D)))
    (p : ℕ) [Fact p.Prime] :
    QuotientGroup.mk' (proCResidualCore (ProCGroups.FiniteGroupClass.pGroup p)
      (TopologicalAbelianization D)) (TopologicalAbelianization.mk D d) ∈
      primaryFixedSubgroup p D hD H

theorem

relativeDerived_quotient_eq_one_of_primaryFixed_eq_bot

L97 ↗

Yamaguchi26AbfaithfulGalois.relativeDerived_quotient_eq_one_of_primaryFixed_eq_bot

Source context 4 commands

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

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

Lean source · statement

theorem relativeDerived_quotient_eq_one_of_primaryFixed_eq_bot
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
    (H : Subgroup G)
    (hfixed : ∀ (p : ℕ) [Fact p.Prime],
      Nontrivial (PrimaryAbelianization p D) → primaryFixedSubgroup p D hD H = ⊥)
    (d : D)
    (hd : QuotientGroup.mk' (relativeDerived D) (d : G) ∈
      Subgroup.centralizer (H.map (QuotientGroup.mk' (relativeDerived D)) :
        Set (RelativeDerivedQuotient D))) :
    QuotientGroup.mk' (relativeDerived D) (d : G) = 1

Module documentation

Relative derived quotients and fixed primary classes

Declarations

relativeDerived_mem_iff

relativeDerived_quotient_mem_openNormal_of_centralizes

primaryAbelianization_mk_mem_fixed_of_quotient_centralizes

relativeDerived_quotient_eq_one_of_primaryFixed_eq_bot