NYLL
Module

Faithful.lean

Nyll.ProCGroups.FiniteStepSolvableQuotients.Faithful
18 declarations indexed from sourceView source ↗

Module documentation

Faithful actions on topological abelianizations

This module defines abelianization-faithfulness for open subgroups and proves that it is preserved under continuous multiplicative equivalences and passage between suitable quotients.

Imports4
Imported by3

Declarations

def

HasNoNontrivialFixedPoints

L28 ↗
ProCGroups.FiniteStepSolvableQuotients.HasNoNontrivialFixedPoints
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
def HasNoNontrivialFixedPoints
    {Q : Type u} [Group Q]
    {A : Type v} [Group A]
    (ρ : Q →* MulAut A) : Prop
theorem

quotientConjAbelianization_injective_of_continuousMulEquiv_image

L37 ↗
ProCGroups.FiniteStepSolvableQuotients.quotientConjAbelianization_injective_of_continuousMulEquiv_image
Documentation

Faithfulness of the quotient-conjugation action pulls back across a continuous multiplicative equivalence, with the open normal subgroup pushed forward along the equivalence.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem quotientConjAbelianization_injective_of_continuousMulEquiv_image
    {G : Type u} {H : Type v}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) (N : OpenNormalSubgroup G)
    (hinjH :
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap
          (G := H)
          (N := (ProCGroups.ProC.OpenNormalSubgroup.map
            (ContinuousMonoidHom.toContinuousMonoidHom e) (Homeomorph.isOpenMap e.toHomeomorph)
            e.surjective N : Subgroup H)))) :
    Function.Injective
      (quotientConjugationTopologicalAbelianizationMap
        (G := G) (N := (N : Subgroup G)))
theorem

isAbFaithful_of_continuousMulEquiv

L244 ↗
ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_of_continuousMulEquiv
Documentation

IsAbFaithful is transported by a continuous multiplicative equivalence.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem isAbFaithful_of_continuousMulEquiv
    {G : Type u} {H : Type v}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) (hH : IsAbFaithful H) :
    IsAbFaithful G
theorem

isAbFaithful_iff_continuousMulEquiv

L313 ↗
ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_iff_continuousMulEquiv
Documentation

Continuous multiplicative equivalence invariance of IsAbFaithful.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem isAbFaithful_iff_continuousMulEquiv
    {G : Type u} {H : Type v}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) :
    IsAbFaithful G ↔ IsAbFaithful H
theorem

isAbFaithful_openSubgroup

L323 ↗
ProCGroups.FiniteStepSolvableQuotients.isAbFaithful_openSubgroup
Documentation

Open subgroups of an ab-faithful topological group are ab-faithful.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem isAbFaithful_openSubgroup
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (hG : IsAbFaithful G) (U : OpenSubgroup G) :
    IsAbFaithful ((U : Subgroup G) : Type u)
def

openNormalSubgroupTop

L390 ↗
ProCGroups.FiniteStepSolvableQuotients.openNormalSubgroupTop
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · full declaration
def openNormalSubgroupTop
    {G : Type u} [TopologicalSpace G] [Group 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
theorem

inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop

L401 ↗
ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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)))
theorem

inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop

L575 ↗
ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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))))
theorem

exists_openNormalSubgroup_not_mem_of_ne_one

L744 ↗
ProCGroups.FiniteStepSolvableQuotients.exists_openNormalSubgroup_not_mem_of_ne_one
Documentation

A nontrivial element is omitted by some open normal subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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)
theorem

center_eq_bot_of_injective_action_on_openNormalsTop

L764 ↗
ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_injective_action_on_openNormalsTop
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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 = ⊥
theorem

center_eq_bot_of_isAbFaithful

L810 ↗
ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_isAbFaithful
Documentation

An abelianization-faithful profinite group has trivial center.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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 = ⊥
theorem

openSubgroup_center_eq_bot_of_isAbFaithful

L820 ↗
ProCGroups.FiniteStepSolvableQuotients.openSubgroup_center_eq_bot_of_isAbFaithful
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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)) = ⊥
theorem

injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap

L860 ↗
ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
Documentation

If an open normal subgroup in an open subgroup of a maximal finite-step solvable quotient contains the last derived term, then the quotient conjugation action on its topological abelianization is faithful.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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)))))
theorem

injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful

L1198 ↗
ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
Documentation

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.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace 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)))))
theorem

inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful

L1220 ↗
ProCGroups.FiniteStepSolvableQuotients.inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace 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)))))
theorem

injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful

L1244 ↗
ProCGroups.FiniteStepSolvableQuotients.injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
theorem injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace 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))))
theorem

center_le_lastDerivedSubgroup_of_isAbFaithful

L1279 ↗
ProCGroups.FiniteStepSolvableQuotients.center_le_lastDerivedSubgroup_of_isAbFaithful
Documentation

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

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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
theorem

center_eq_bot_of_center_le_of_noNontrivialFixedPoints_of_inj_topologicalAbelianization

L1342 ↗
ProCGroups.FiniteStepSolvableQuotients.center_eq_bot_of_center_le_of_noNontrivialFixedPoints_of_inj_topologicalAbelianization
Documentation

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.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.FiniteStepSolvableQuotients
open ProCGroups.Abelian
universe u v
Lean source · statement
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 = ⊥

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