Module

EmbeddingFormulation.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.EmbeddingFormulation

18 declarations indexed from sourceView source ↗

Module documentation

Finite abelian embedding problems

An invariant finite quotient of the abelianization of an open normal subgroup produces an open normal subgroup of the ambient group and a proper finite embedding problem.

Imports4

Imported by2

theorem

continuous_quotientConjugationTopologicalAbelianizationMap

L30 ↗

ProCGroups.FiniteStepSolvableQuotients.continuous_quotientConjugationTopologicalAbelianizationMap

Documentation

Each automorphism in the quotient conjugation action is continuous.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem continuous_quotientConjugationTopologicalAbelianizationMap
    (N : Subgroup H) [N.Normal] (q : H ⧸ N) :
    Continuous (quotientConjugationTopologicalAbelianizationMap N q)

def

invariantAbelianQuotientMap

L45 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientMap

Documentation

The finite invariant quotient of the abelianization, pulled back to N.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def invariantAbelianQuotientMap [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    (N : Subgroup H) →ₜ*
      TopologicalAbelianization (N : Subgroup H) ⧸
        (invariantOpenNormalCore
          (quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))
          (continuous_quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))
          U : Subgroup (TopologicalAbelianization (N : Subgroup H)))

theorem

invariantAbelianQuotientMap_surjective

L61 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientMap_surjective

Documentation

The map from N onto its finite invariant abelian quotient is surjective.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem invariantAbelianQuotientMap_surjective [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    Function.Surjective (invariantAbelianQuotientMap N U)

def

invariantAbelianQuotientKernel

L73 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientKernel

Documentation

The kernel of the invariant quotient, regarded as an open normal subgroup of the ambient group. Its ambient normality follows from invariance of the core.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def invariantAbelianQuotientKernel [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    OpenNormalSubgroup H where
  toSubgroup := (invariantAbelianQuotientMap N U).toMonoidHom.ker.map
    (N : Subgroup H).subtype
  isOpen' := by
    exact N.isOpen'.isOpenMap_subtype_val
      ((invariantAbelianQuotientMap N U).toMonoidHom.ker : Set (N : Subgroup H))
      (ProC.OpenNormalSubgroup.ker (invariantAbelianQuotientMap N U)).isOpen'
  isNormal' := by
    refine ⟨?_⟩
    intro x hx h
    obtain ⟨n, hn, rfl⟩ := hx
    refine ⟨MulAut.conjNormal h n, ?_, ?_⟩
    · change invariantAbelianQuotientMap N U (MulAut.conjNormal h n) = 1
      apply ProC.OpenNormalSubgroup.quotientProj_eq_one_iff.mpr
      rw [← quotientConjugationTopologicalAbelianizationMap_mk_apply_mk]
      apply action_mem_invariantOpenNormalCore
      exact ProC.OpenNormalSubgroup.quotientProj_eq_one_iff.mp hn
    · exact MulAut.conjNormal_apply h n

theorem

invariantAbelianQuotientKernel_le

L96 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientKernel_le

Documentation

The constructed ambient kernel lies in the original open normal subgroup.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem invariantAbelianQuotientKernel_le [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    (invariantAbelianQuotientKernel N U : Subgroup H) ≤ (N : Subgroup H)

theorem

mem_invariantAbelianQuotientKernel_iff

L106 ↗

ProCGroups.FiniteStepSolvableQuotients.mem_invariantAbelianQuotientKernel_iff

Documentation

On elements of N, the ambient kernel is exactly the kernel of the finite abelian quotient map.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem mem_invariantAbelianQuotientKernel_iff [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H)))
    (n : (N : Subgroup H)) :
    (n : H) ∈ invariantAbelianQuotientKernel N U ↔
      invariantAbelianQuotientMap N U n = 1

theorem

invariantAbelianQuotientKernel_mk_eq_iff

L122 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientKernel_mk_eq_iff

Documentation

Two elements of N have the same ambient quotient class exactly when they have the same image in the invariant abelian quotient.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem invariantAbelianQuotientKernel_mk_eq_iff [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H)))
    (n m : (N : Subgroup H)) :
    QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) (n : H) =
        QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) (m : H) ↔
      invariantAbelianQuotientMap N U n = invariantAbelianQuotientMap N U m

theorem

invariantAbelianQuotientMap_conj

L137 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientMap_conj

Documentation

The finite quotient map from N intertwines conjugation and the induced finite action.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem invariantAbelianQuotientMap_conj [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H)))
    (h : H) (n : (N : Subgroup H)) :
    invariantAbelianQuotientMap N U (MulAut.conjNormal h n) =
      invariantOpenNormalQuotientAction
        (quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))
        (continuous_quotientConjugationTopologicalAbelianizationMap (N : Subgroup H)) U
        (QuotientGroup.mk' (N : Subgroup H) h) (invariantAbelianQuotientMap N U n)

theorem

invariantAbelianQuotientKernel_commute

L160 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianQuotientKernel_commute

Documentation

The image of N in the ambient finite quotient is abelian.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem invariantAbelianQuotientKernel_commute [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H)))
    (n m : (N : Subgroup H)) :
    Commute
      (QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) (n : H))
      (QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) (m : H))

theorem

mem_of_invariantAbelianQuotientKernel_centralizes

L174 ↗

ProCGroups.FiniteStepSolvableQuotients.mem_of_invariantAbelianQuotientKernel_centralizes

Documentation

Faithfulness on the finite abelian quotient forces every element whose ambient quotient class centralizes the image of N to belong to N.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem mem_of_invariantAbelianQuotientKernel_centralizes [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H)))
    (hfaithful : Function.Injective (invariantOpenNormalQuotientAction
      (quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))
      (continuous_quotientConjugationTopologicalAbelianizationMap (N : Subgroup H)) U))
    (h : H)
    (hcentralizes : ∀ n : (N : Subgroup H), Commute
      (QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) h)
      (QuotientGroup.mk' (invariantAbelianQuotientKernel N U : Subgroup H) (n : H))) :
    h ∈ N

theorem

exists_openNormal_abelian_selfCentralizing_quotient

L200 ↗

ProCGroups.FiniteStepSolvableQuotients.exists_openNormal_abelian_selfCentralizing_quotient

Documentation

A faithful action on N's topological abelianization yields an open normal R ≤ N such that N/R is abelian and is its own centralizer in H/R.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem exists_openNormal_abelian_selfCentralizing_quotient
    [CompactSpace H] [TotallyDisconnectedSpace H]
    (N : OpenNormalSubgroup H)
    (hfaithful : Function.Injective
      (quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))) :
    ∃ R : OpenNormalSubgroup H, (R : Subgroup H) ≤ (N : Subgroup H) ∧
      (∀ 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)

def

invariantAbelianEmbeddingProblem

L226 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianEmbeddingProblem

Documentation

The canonical finite embedding problem arising from the ambient kernel.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def invariantAbelianEmbeddingProblem [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    TopologicalEmbeddingProblem H where
  A := TopGrp.of (H ⧸ (invariantAbelianQuotientKernel N U : Subgroup H))
  B := TopGrp.of (H ⧸ (N : Subgroup H))
  α := ProC.OpenNormalSubgroup.transition
    (invariantAbelianQuotientKernel_le N U)
  surjective_α := ProC.OpenNormalSubgroup.transition_surjective
    (invariantAbelianQuotientKernel_le N U)
  φ := ProC.OpenNormalSubgroup.quotientProj N
  surjective_φ := ProC.OpenNormalSubgroup.quotientProj_surjective N

def

invariantAbelianEmbeddingProblemProperSolution

L240 ↗

ProCGroups.FiniteStepSolvableQuotients.invariantAbelianEmbeddingProblemProperSolution

Documentation

The ambient quotient projection is a proper solution.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def invariantAbelianEmbeddingProblemProperSolution [CompactSpace H]
    (N : OpenNormalSubgroup H)
    (U : OpenNormalSubgroup (TopologicalAbelianization (N : Subgroup H))) :
    (invariantAbelianEmbeddingProblem N U).ProperSolution

theorem

map_eq_of_topologicalAbelianization_eq

L251 ↗

ProCGroups.FiniteStepSolvableQuotients.map_eq_of_topologicalAbelianization_eq

Documentation

A continuous homomorphism with commutative image identifies any two elements identified by topological abelianization.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem map_eq_of_topologicalAbelianization_eq
    {D : Type u} [Group D] [TopologicalSpace D] [T1Space D]
    (f : H →ₜ* D) (hcomm : ∀ x y : H, Commute (f x) (f y))
    {x y : H}
    (hxy : TopologicalAbelianization.mk H x = TopologicalAbelianization.mk H y) :
    f x = f y

theorem

injective_quotientConjugation_of_selfCentralizing_image

L282 ↗

ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjugation_of_selfCentralizing_image

Documentation

An abelian image of N with no larger centralizer detects every nontrivial element of the conjugation action on the topological abelianization of N.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem injective_quotientConjugation_of_selfCentralizing_image
    {D : Type u} [Group D] [TopologicalSpace D] [T1Space D]
    (N : OpenNormalSubgroup H) (θ : H →ₜ* D)
    (hcomm : ∀ n m : (N : Subgroup H), Commute
      (θ (n : H)) (θ (m : H)))
    (hcentralizer : ∀ h : H, (∀ n : (N : Subgroup H), Commute
      (θ h) (θ (n : H))) → h ∈ N) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap (N : Subgroup H))

theorem

isAbFaithful_iff_exists_abelian_selfCentralizing_quotient

L312 ↗

ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_iff_exists_abelian_selfCentralizing_quotient

Documentation

Abelianization-faithfulness is equivalent to the existence of finite ambient quotients in which each open normal subgroup has abelian, self-centralizing image.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem isAbFaithful_iff_exists_abelian_selfCentralizing_quotient
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G] :
    IsAbFaithful G ↔
      ∀ H : OpenSubgroup G, ∀ N : OpenNormalSubgroup (H : Subgroup G),
        ∃ R : OpenNormalSubgroup (H : Subgroup G),
          (R : Subgroup (H : Subgroup G)) ≤ (N : Subgroup (H : Subgroup G)) ∧
          (∀ n m : (N : Subgroup (H : Subgroup G)), Commute
            (QuotientGroup.mk' (R : Subgroup (H : Subgroup G)) (n : (H : Subgroup G)))
            (QuotientGroup.mk' (R : Subgroup (H : Subgroup G)) (m : (H : Subgroup G)))) ∧
          (∀ h : (H : Subgroup G), (∀ n : (N : Subgroup (H : Subgroup G)), Commute
            (QuotientGroup.mk' (R : Subgroup (H : Subgroup G)) h)
            (QuotientGroup.mk' (R : Subgroup (H : Subgroup G)) (n : (H : Subgroup G)))) →
              h ∈ N)

def

HasFiniteFaithfulAbelianEmbeddingSolutions

L338 ↗

ProCGroups.FiniteStepSolvableQuotients.HasFiniteFaithfulAbelianEmbeddingSolutions

Documentation

Every finite quotient of every open subgroup admits a proper finite embedding problem with abelian kernel and faithful conjugation action of the given target.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def HasFiniteFaithfulAbelianEmbeddingSolutions
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

theorem

isAbFaithful_iff_hasFiniteFaithfulAbelianEmbeddingSolutions

L351 ↗

ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_iff_hasFiniteFaithfulAbelianEmbeddingSolutions

Documentation

The finite faithful abelian embedding formulation of abelianization-faithfulness.

Source context 5 commands

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

namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
open ProCGroups.FreeProC.Characterization
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem isAbFaithful_iff_hasFiniteFaithfulAbelianEmbeddingSolutions
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G] :
    IsAbFaithful G ↔ HasFiniteFaithfulAbelianEmbeddingSolutions G

Module documentation

Finite abelian embedding problems

Declarations