NYLL
Module

ResidualFiniteInvariantQuotient.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualFiniteInvariantQuotient
9 declarations indexed from sourceView source ↗

Module documentation

Finite invariant quotients of residual abelianizations

A faithful finite relative action on the actual residual abelianization admits a faithful finite invariant quotient in the original formation. Pulling its projection back to the normal subgroup produces an open normal subgroup of the ambient group. In particular, the class of finite Sigma groups gives finite abelian Sigma quotients with an actual ambient kernel.

Imports10
Imported by2

Declarations

theorem

continuous_residualAbelianizationQuotientConjugation

L39 ↗
ProCGroups.FiniteStepSolvableQuotients.continuous_residualAbelianizationQuotientConjugation
Documentation

Each automorphism in residual quotient conjugation is continuous.

Source context 5 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]
Lean source · statement
theorem continuous_residualAbelianizationQuotientConjugation
    (hC : FiniteGroupClass.FullFormation C)
    (N : Subgroup H) [N.Normal] (hN : IsClosed (N : Set H)) (q : H ⧸ N) :
    Continuous (residualAbelianizationQuotientConjugation hC N hN q)
def

invariantResidualAbelianQuotientMap

L62 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientMap
Documentation

The projection to the finite invariant residual abelian quotient, pulled back along the two canonical quotient maps from 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
def invariantResidualAbelianQuotientMap (U : OpenNormalSubgroup Ab) :
    (N : Subgroup H) →ₜ* Ab ⧸ (invariantOpenNormalCore ρ hρ U : Subgroup Ab)
theorem

invariantResidualAbelianQuotientMap_apply

L71 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientMap_apply
Documentation

The composite is the actual residual and abelianization projection on every subgroup representative.

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 invariantResidualAbelianQuotientMap_apply
    (U : OpenNormalSubgroup Ab) (n : (N : Subgroup H)) :
    invariantResidualAbelianQuotientMap hC N U n =
      QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup Ab)
        (TopologicalAbelianization.mk Res
          (QuotientGroup.mk' (proCResidualCore C (N : Subgroup H)) n))
theorem

invariantResidualAbelianQuotientMap_surjective

L80 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientMap_surjective
Documentation

The composite onto the finite invariant quotient is surjective.

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 invariantResidualAbelianQuotientMap_surjective
    (U : OpenNormalSubgroup Ab) :
    Function.Surjective (invariantResidualAbelianQuotientMap hC N U)
theorem

invariantResidualAbelianQuotientMap_conj

L92 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientMap_conj
Documentation

The composite preserves the actual ambient conjugation action.

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 invariantResidualAbelianQuotientMap_conj
    (U : OpenNormalSubgroup Ab) (h : H) (n : (N : Subgroup H)) :
    invariantResidualAbelianQuotientMap hC N U (MulAut.conjNormal h n) =
      invariantOpenNormalQuotientAction ρ hρ U
        (QuotientGroup.mk' (N : Subgroup H) h)
        (invariantResidualAbelianQuotientMap hC N U n)
def

invariantResidualAbelianQuotientKernel

L113 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientKernel
Documentation

The finite invariant quotient has an actual open normal kernel in the ambient group; normality follows from the constructed conjugation formula.

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 · full declaration
def invariantResidualAbelianQuotientKernel
    (U : OpenNormalSubgroup Ab) : OpenNormalSubgroup H where
  toSubgroup := (invariantResidualAbelianQuotientMap hC N U).toMonoidHom.ker.map
    (N : Subgroup H).subtype
  isOpen' := by
    exact N.isOpen'.isOpenMap_subtype_val
      ((invariantResidualAbelianQuotientMap hC N U).toMonoidHom.ker : Set (N : Subgroup H))
      (ProC.OpenNormalSubgroup.ker (invariantResidualAbelianQuotientMap hC N U)).isOpen'
  isNormal' := by
    refine ⟨?_⟩
    intro x hx h
    obtain ⟨n, hn, rfl⟩ := hx
    refine ⟨MulAut.conjNormal h n, ?_, MulAut.conjNormal_apply h n⟩
    change invariantResidualAbelianQuotientMap hC N U (MulAut.conjNormal h n) = 1
    change invariantResidualAbelianQuotientMap hC N U n = 1 at hn
    rw [invariantResidualAbelianQuotientMap_conj, hn, map_one]
theorem

invariantResidualAbelianQuotientKernel_le

L131 ↗
ProCGroups.FiniteStepSolvableQuotients.invariantResidualAbelianQuotientKernel_le
Documentation

The ambient kernel is contained in the original open normal 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_le
    (U : OpenNormalSubgroup Ab) :
    (invariantResidualAbelianQuotientKernel hC N U : Subgroup H) ≤ (N : Subgroup H)
theorem

mem_invariantResidualAbelianQuotientKernel_iff

L140 ↗
ProCGroups.FiniteStepSolvableQuotients.mem_invariantResidualAbelianQuotientKernel_iff
Documentation

Restricting the ambient kernel back to the original subgroup recovers exactly the kernel of the finite quotient map.

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_invariantResidualAbelianQuotientKernel_iff
    (U : OpenNormalSubgroup Ab) (n : (N : Subgroup H)) :
    (n : H) ∈ invariantResidualAbelianQuotientKernel hC N U ↔
      invariantResidualAbelianQuotientMap hC N U n = 1
theorem

exists_faithful_invariantResidualAbelianQuotient

L155 ↗
ProCGroups.FiniteStepSolvableQuotients.exists_faithful_invariantResidualAbelianQuotient
Documentation

A faithful action on the residual abelianization admits a faithful finite invariant quotient in the same formation. For sigmaGroup sigma, this is a finite abelian Sigma group, with the ambient kernel constructed above.

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_faithful_invariantResidualAbelianQuotient
    (hfaithful : Function.Injective ρ) :
    ∃ U : OpenNormalSubgroup Ab,
      Function.Injective (invariantOpenNormalQuotientAction ρ hρ U) ∧
        C (Ab ⧸ (invariantOpenNormalCore ρ hρ U : Subgroup Ab))

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