ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful

12 Theorem | 3 Definition

This module studies faithful for pro cgroups. An action has no nontrivial fixed points if every globally fixed element is trivial. Every open subgroup acts faithfully on the topological abelianization of each open normal subgroup.

Open this file on GitHub

import

Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
ProCGroups.FiniteStepSolvableQuotients.Abelianization
ProCGroups.ProC.Quotients.ClosedNormal

Imported by

Definition ProCGroups.FiniteStepSolvableQuotients.HasNoNontrivialFixedPoints GitHub

def HasNoNontrivialFixedPoints
    {Q : Type u} [Group Q]
    {A : Type v} [Group A]
    (ρ : Q →* MulAut A) : Prop :=
  ∀ a : A, (∀ q : Q, ρ q a = a) → a = 1

An action has no nontrivial fixed points if every globally fixed element is trivial.

Definition ProCGroups.FiniteStepSolvableQuotients.IsAbFaithful GitHub

def IsAbFaithful
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
  ∀ H : OpenSubgroup G,
    ∀ N : OpenNormalSubgroup ↥(H : Subgroup G),
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap
          (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))))

Every open subgroup acts faithfully on the topological abelianization of each open normal subgroup.

Definition ProCGroups.FiniteStepSolvableQuotients.openNormalSubgroupTop GitHub

def openNormalSubgroupTop
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (U : OpenNormalSubgroup G) :
    OpenNormalSubgroup ↥((⊤ : OpenSubgroup G) : Subgroup G) where
  toOpenSubgroup :=
    OpenSubgroup.comap ((⊤ : Subgroup G).subtype) continuous_subtype_val U.toOpenSubgroup
  isNormal' := by
    change ((U : Subgroup G).comap ((⊤ : Subgroup G).subtype)).Normal
    infer_instance

The same open normal subgroup viewed inside the \(\top\) open subgroup.

Theorem ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop GitHub

theorem inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (U : OpenNormalSubgroup G)
    (hTop :
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap
          (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
          (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G))))) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := G) (N := (U : Subgroup G)))

Injectivity on the top-open-subgroup model implies injectivity in the ambient group.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop GitHub

theorem inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (U : OpenNormalSubgroup G)
    (hU :
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap
          (G := G) (N := (U : Subgroup G)))) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
        (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G))))

Injectivity in the ambient group transfers to the corresponding open normal subgroup inside the \(\top\) open subgroup model.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.exists_openNormalSubgroup_not_mem_of_ne_one GitHub

theorem exists_openNormalSubgroup_not_mem_of_ne_one
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {x : G} (hx : x ≠ 1) :
    ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G)

A nontrivial element is omitted by some open normal subgroup.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_injective_action_on_openNormalsTop GitHub

theorem center_eq_bot_of_injective_action_on_openNormalsTop
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    (hfaithful :
      ∀ U : OpenNormalSubgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q),
        Function.Injective
          (quotientConjugationTopologicalAbelianizationMap
            (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
            (N := (U : Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q))))) :
    Subgroup.center Q = ⊥

Faithfulness of the conjugation action on every open normal subgroup of the \(\top\) open subgroup forces the ambient center to be trivial.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_isAbFaithful GitHub

theorem center_eq_bot_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G) :
    Subgroup.center G = ⊥

An abelianization-faithful profinite group has trivial center.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.openSubgroup_center_eq_bot_of_isAbFaithful GitHub

theorem openSubgroup_center_eq_bot_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G) (H : OpenSubgroup G) :
    Subgroup.center ↥((H : Subgroup G)) = ⊥

Every open subgroup of an abelianization-faithful profinite group has trivial center.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.anonymous_390 GitHub

theorem
    injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hG : IsAbFaithful G)
    {m : ℕ} (hm : 2 ≤ m)
    (hclosedπ : IsClosedMap (continuousToMaxSolvQuot G m))
    (H : OpenSubgroup (MaxSolvQuot G m))
    (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
    (hContain : containsLastDerived m H N) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := ↥(H : Subgroup (MaxSolvQuot G m)))
        (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m)))))

The auxiliary pro-\(C\) coordinate identity follows from the finite-stage quotient data defining the construction.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful GitHub

theorem injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G)
    {m : ℕ} (hm : 2 ≤ m)
    (H : OpenSubgroup (MaxSolvQuot G m))
    (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
    (hContain : containsLastDerived (G := G) m H N) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := ↥(H : Subgroup (MaxSolvQuot G m)))
        (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m)))))

Open normal subgroups inside open subgroups of a maximal finite-step solvable quotient inherit faithful quotient conjugation actions once they contain the last derived subgroup.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful GitHub

theorem inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G)
    {m : ℕ} (hm : 2 ≤ m)
    (H : OpenSubgroup (MaxSolvQuot G m))
    (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
    (hN :
      lastDerivedSubgroup (G := G) m ≤
        (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
          ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := ↥(H : Subgroup (MaxSolvQuot G m)))
        (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m)))))

Ambient containment form of faithful quotient conjugation for open normal subgroups inside open subgroups of a maximal finite-step solvable quotient.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful GitHub

theorem injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G)
    {m : ℕ} (hm : 2 ≤ m)
    (U : OpenNormalSubgroup (MaxSolvQuot G m))
    (hU : lastDerivedSubgroup (G := G) m ≤ (U : Subgroup (MaxSolvQuot G m))) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := MaxSolvQuot G m) (N := (U : Subgroup (MaxSolvQuot G m))))

Open normal supergroups above the last derived subgroup inherit faithful quotient conjugation actions under the ambient abelianization-faithful hypothesis.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.center_le_lastDerivedSubgroup_of_isAbFaithful GitHub

theorem center_le_lastDerivedSubgroup_of_isAbFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsAbFaithful G)
    {m : ℕ} (hm : 1 ≤ m) :
    Subgroup.center (MaxSolvQuot G m) ≤ lastDerivedSubgroup (G := G) m

In a maximal finite-step solvable quotient, the center lies in the last derived subgroup under the ambient abelianization-faithful hypothesis.

Show proof

Theorem ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_center_le_of_noNontrivialFixedPoints_of_inj_topologicalAbelianization GitHub

theorem center_eq_bot_of_center_le_of_noNontrivialFixedPoints_of_inj_topologicalAbelianization
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {K : Subgroup Q} [K.Normal]
    (hcenter : Subgroup.center Q ≤ K)
    (hfixed :
      HasNoNontrivialFixedPoints
        (quotientConjugationTopologicalAbelianizationMap (G := Q) (N := K)))
    (hinj : Function.Injective (TopologicalAbelianization.mk ↥K)) :
    Subgroup.center Q = ⊥

If the center lies in a normal subgroup whose topological abelianization action has no nontrivial fixed points, then injectivity of the natural map to topological abelianization forces the ambient center to be trivial.

Show proof

ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful

Declarations