NYLL
Module

ResidualSelfCentralizingQuotient.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualSelfCentralizingQuotient
5 declarations indexed from sourceView source ↗

Module documentation

Self-centralizing quotients with residual image in the formation

A faithful finite invariant quotient of the residual abelianization gives an open normal ambient kernel. Its subgroup image is abelian and self-centralizing. The first isomorphism theorem identifies that actual image with the constructed finite quotient, so the image belongs to the formation without imposing a condition on the entire ambient quotient.

Imports7
Imported by2

Declarations

theorem

invariantResidualAbelianQuotientKernel_mk_eq_iff

L45 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientKernel_mk_eq_iff
Documentation

On the original subgroup, equality in the ambient quotient is precisely equality in the constructed finite invariant residual quotient.

Source context 10 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (hC : FiniteGroupClass.FullFormation C) (N : OpenNormalSubgroup H)
local notation "Res" => (N : Subgroup H) ⧸ proCResidualCore C (N : Subgroup H)
local notation "Ab" => TopologicalAbelianization Res
local notation "ρ" => residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
local notation "hρ" => continuous_residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
Lean source · statement
theorem invariantResidualAbelianQuotientKernel_mk_eq_iff
    (U : OpenNormalSubgroup Ab) (n m : (N : Subgroup H)) :
    QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H)
        (n : H) =
      QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H)
        (m : H) ↔
      invariantResidualAbelianQuotientMap hC N U n =
        invariantResidualAbelianQuotientMap hC N U m
theorem

invariantResidualAbelianQuotientKernel_commute

L61 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientKernel_commute
Documentation

The original subgroup has abelian image in the constructed ambient quotient.

Source context 10 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (hC : FiniteGroupClass.FullFormation C) (N : OpenNormalSubgroup H)
local notation "Res" => (N : Subgroup H) ⧸ proCResidualCore C (N : Subgroup H)
local notation "Ab" => TopologicalAbelianization Res
local notation "ρ" => residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
local notation "hρ" => continuous_residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
Lean source · statement
theorem invariantResidualAbelianQuotientKernel_commute
    (U : OpenNormalSubgroup Ab) (n m : (N : Subgroup H)) :
    Commute
      (QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H)
        (n : H))
      (QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H)
        (m : H))
theorem

mem_of_invariantResidualAbelianQuotientKernel_centralizes

L75 ↗
ProCGroups.FiniteStepSolvableQuotients.mem_of_invariantResidualAbelianQuotientKernel_centralizes
Documentation

Faithfulness on the finite invariant quotient forces every ambient element centralizing the subgroup image to lie in the original subgroup.

Source context 10 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (hC : FiniteGroupClass.FullFormation C) (N : OpenNormalSubgroup H)
local notation "Res" => (N : Subgroup H) ⧸ proCResidualCore C (N : Subgroup H)
local notation "Ab" => TopologicalAbelianization Res
local notation "ρ" => residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
local notation "hρ" => continuous_residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
Lean source · statement
theorem mem_of_invariantResidualAbelianQuotientKernel_centralizes
    (U : OpenNormalSubgroup Ab)
    (hfaithful : Function.Injective (invariantOpenNormalQuotientAction ρ hρ U))
    (h : H)
    (hcentralizes : ∀ n : (N : Subgroup H), Commute
      (QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H) h)
      (QuotientGroup.mk' (invariantResidualAbelianQuotientKernel hC N U : Subgroup H)
        (n : H))) :
    h ∈ N
theorem

invariantResidualAbelianQuotientKernel_range_mem

L101 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientKernel_range_mem
Documentation

The subgroup image belongs to the formation whenever the constructed finite invariant quotient does: their kernels agree and both identify with the same quotient of the original subgroup.

Source context 10 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (hC : FiniteGroupClass.FullFormation C) (N : OpenNormalSubgroup H)
local notation "Res" => (N : Subgroup H) ⧸ proCResidualCore C (N : Subgroup H)
local notation "Ab" => TopologicalAbelianization Res
local notation "ρ" => residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
local notation "hρ" => continuous_residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
Lean source · statement
theorem invariantResidualAbelianQuotientKernel_range_mem
    (U : OpenNormalSubgroup Ab)
    (hU : C (Ab ⧸ (invariantOpenNormalCore ρ hρ U : Subgroup Ab))) :
    C (((ProC.OpenNormalSubgroup.quotientProj
      (invariantResidualAbelianQuotientKernel hC N U)).toMonoidHom.comp
        (N : Subgroup H).subtype).range)
theorem

exists_openNormal_abelian_selfCentralizing_quotient_inClass

L134 ↗
ProCGroups.FiniteStepSolvableQuotients.exists_openNormal_abelian_selfCentralizing_quotient_inClass
Documentation

Faithful residual conjugation produces an open normal ambient quotient in which the original subgroup has abelian self-centralizing image in the formation. The ambient quotient itself need not belong to the class.

Source context 10 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.ProC ProCGroups.Abelian
universe u
variable {C : FiniteGroupClass.{u}}
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
variable (hC : FiniteGroupClass.FullFormation C) (N : OpenNormalSubgroup H)
local notation "Res" => (N : Subgroup H) ⧸ proCResidualCore C (N : Subgroup H)
local notation "Ab" => TopologicalAbelianization Res
local notation "ρ" => residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
local notation "hρ" => continuous_residualAbelianizationQuotientConjugation hC
  (N : Subgroup H) N.isClosed
Lean source · statement
theorem exists_openNormal_abelian_selfCentralizing_quotient_inClass
    (hfaithful : Function.Injective ρ) :
    ∃ R : OpenNormalSubgroup H, (R : Subgroup H) ≤ (N : Subgroup H) ∧
      C (((ProC.OpenNormalSubgroup.quotientProj R).toMonoidHom.comp
        (N : Subgroup H).subtype).range) ∧
      (∀ n m : (N : Subgroup H), Commute
        (QuotientGroup.mk' (R : Subgroup H) (n : H))
        (QuotientGroup.mk' (R : Subgroup H) (m : H))) ∧
      (∀ h : H, (∀ n : (N : Subgroup H), Commute
        (QuotientGroup.mk' (R : Subgroup H) h)
        (QuotientGroup.mk' (R : Subgroup H) (n : H))) → h ∈ N)

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