Module

Separation.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.Separation

10 declarations indexed from sourceView source ↗

Module documentation

Separation by open normal quotients

This file detects equality and closed-subgroup membership in all open normal quotients. It also develops refinements avoiding a chosen coset, cyclic-containment consequences, and extensionality of continuous homomorphisms from their finite quotient maps.

Imports6

Imported by12

theorem

mem_closed_iff_forall_openNormal_quotient

L31 ↗

ProCGroups.mem_closed_iff_forall_openNormal_quotient

Documentation

Membership in a closed subset of a profinite group can be tested on all open-normal quotients.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups
universe u

Lean source · statement

theorem mem_closed_iff_forall_openNormal_quotient
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {S : Set G} (hSclosed : IsClosed S) {x : G} :
    x ∈ S ↔
      ∀ U : OpenNormalSubgroup G,
        ∃ y ∈ S, QuotientGroup.mk' (U : Subgroup G) y =
          QuotientGroup.mk' (U : Subgroup G) x

theorem

eq_of_forall_quotientProj_eq

L75 ↗

ProCGroups.ProC.OpenNormalSubgroup.eq_of_forall_quotientProj_eq

Documentation

Two elements of a profinite group are equal if all their open-normal quotient projections agree.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace OpenNormalSubgroup

Lean source · statement

theorem eq_of_forall_quotientProj_eq [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G] {x y : G}
    (hxy : ∀ U : OpenNormalSubgroup G, quotientProj U x = quotientProj U y) :
    x = y

theorem

mem_sup_of_quotient_mk_mem_map

L101 ↗

ProCGroups.ProC.mem_sup_of_quotient_mk_mem_map

Documentation

If the image of y modulo an open normal subgroup lies in the image of H, then y lies in H \(\sqcup\) U.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem mem_sup_of_quotient_mk_mem_map
    {Q : Type u} [TopologicalSpace Q] [Group Q]
    (H : Subgroup Q) (U : OpenNormalSubgroup Q)
    {y : Q}
    (hy :
      QuotientGroup.mk' (U : Subgroup Q) y ∈
        H.map (QuotientGroup.mk' (U : Subgroup Q))) :
    y ∈ H ⊔ (U : Subgroup Q)

theorem

mem_closedSubgroup_of_forall_openNormal_sup

L127 ↗

ProCGroups.ProC.mem_closedSubgroup_of_forall_openNormal_sup

Documentation

Closed-subgroup membership can be checked after adjoining every open normal subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem mem_closedSubgroup_of_forall_openNormal_sup
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    (H : ClosedSubgroup Q) {y : Q}
    (hy : ∀ U : OpenNormalSubgroup Q,
      y ∈ (H : Subgroup Q) ⊔ (U : Subgroup Q)) :
    y ∈ (H : Subgroup Q)

def

openNormalSubgroup_inf

L147 ↗

ProCGroups.ProC.openNormalSubgroup_inf

Documentation

The intersection of two open normal subgroups is open and normal.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def openNormalSubgroup_inf
    {Q : Type u} [TopologicalSpace Q] [Group Q]
    (U V : OpenNormalSubgroup Q) : OpenNormalSubgroup Q where
  toOpenSubgroup :=
    { toSubgroup := (U : Subgroup Q) ⊓ (V : Subgroup Q)
      isOpen' :=
        (ProCGroups.openNormalSubgroup_isOpen (G := Q) U).inter
          (ProCGroups.openNormalSubgroup_isOpen (G := Q) V) }
  isNormal' := by
    change ((U : Subgroup Q) ⊓ (V : Subgroup Q)).Normal
    infer_instance

theorem

exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup

L160 ↗

ProCGroups.ProC.exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup

Documentation

Cofinal separation from a closed subgroup by open normal subgroups.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    (H : ClosedSubgroup Q) {x : Q} (hx : x ∉ (H : Subgroup Q))
    (U : OpenNormalSubgroup Q) :
    ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
      x ∉ (H : Subgroup Q) ⊔ (W : Subgroup Q)

def

openNormalSubgroup_sup_normal

L189 ↗

ProCGroups.ProC.openNormalSubgroup_sup_normal

Documentation

The open normal subgroup K \(\sqcup\) U, where K is normal and U is open normal.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def openNormalSubgroup_sup_normal
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (K : Subgroup Q) [K.Normal] (U : OpenNormalSubgroup Q) :
    OpenNormalSubgroup Q where
  toOpenSubgroup :=
    { toSubgroup := K ⊔ (U : Subgroup Q)
      isOpen' :=
        Subgroup.isOpen_of_openSubgroup (K ⊔ (U : Subgroup Q))
          (show (U : Subgroup Q) ≤ K ⊔ (U : Subgroup Q) from le_sup_right) }
  isNormal' := by
    change (K ⊔ (U : Subgroup Q)).Normal
    infer_instance

theorem

cofinal_openNormal_cyclic_containment_of_finite_lift

L206 ↗

ProCGroups.ProC.cofinal_openNormal_cyclic_containment_of_finite_lift

Documentation

The cofinal quotient condition obtained from a separation statement and finite-stage cyclic containment on quotients where \(x^n\) remains nontrivial modulo \(K\).

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

theorem cofinal_openNormal_cyclic_containment_of_finite_lift
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [TotallyDisconnectedSpace Q]
    (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
    (hnotK : x ^ n ∉ K)
    (hfinite : ∀ W : OpenNormalSubgroup Q,
      x ^ n ∉ K ⊔ (W : Subgroup Q) →
        let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
        ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
          QuotientGroup.mk' (V : Subgroup Q) y ∈
            ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
              ClosedSubgroup Q) :
              Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
    ∀ U : OpenNormalSubgroup Q,
      ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
        let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
        ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
          QuotientGroup.mk' (V : Subgroup Q) y ∈
            ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
              ClosedSubgroup Q) :
              Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q)) := by
  intro U
  let Kclosed : ClosedSubgroup Q := ⟨K, hKclosed⟩
  rcases
      exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
        (H := Kclosed) hnotK U with
    ⟨W, hWU, hnotW⟩
  refine ⟨W, hWU, ?_⟩
  change x ^ n ∉ K ⊔ (W : Subgroup Q) at hnotW
  exact hfinite W hnotW

theorem

centralizerOf_zpow_le_cyclic_join_closedNormal_of_cofinal_openNormal_image

L241 ↗

ProCGroups.ProC.centralizerOf_zpow_le_cyclic_join_closedNormal_of_cofinal_openNormal_image

Documentation

Cofinal image criterion for bounding a centralizer by a cyclic subgroup joined with a closed normal subgroup.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

theorem centralizerOf_zpow_le_cyclic_join_closedNormal_of_cofinal_openNormal_image
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
    (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
    (himage : ∀ U : OpenNormalSubgroup Q,
      ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
        let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
        ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
          QuotientGroup.mk' (V : Subgroup Q) y ∈
            ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
              ClosedSubgroup Q) :
              Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
    ProCGroups.GroupTheory.centralizerOf (x ^ n) ≤
      ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
        ClosedSubgroup Q) :
        Subgroup Q) ⊔ K := by
  let L : Subgroup Q :=
    ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
      ClosedSubgroup Q) : Subgroup Q)
  let H : ClosedSubgroup Q :=
    ⟨L ⊔ K,
      Subgroup.isClosed_sup_of_normal L K
        (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q)).isClosed'
        hKclosed⟩
  intro y hy
  apply mem_closedSubgroup_of_forall_openNormal_sup H
  intro U
  rcases himage U with ⟨W, hWU, hWimage⟩
  let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
  have hyVL :
      QuotientGroup.mk' (V : Subgroup Q) y ∈
        L.map (QuotientGroup.mk' (V : Subgroup Q)) := by
    simpa [L, V] using hWimage y hy
  have hySupV : y ∈ L ⊔ (V : Subgroup Q) :=
    mem_sup_of_quotient_mk_mem_map L V hyVL
  have hle : L ⊔ (V : Subgroup Q) ≤ (H : Subgroup Q) ⊔ (U : Subgroup Q) := by
    change L ⊔ (K ⊔ (W : Subgroup Q)) ≤ (L ⊔ K) ⊔ (U : Subgroup Q)
    refine sup_le ?_ ?_
    · exact (show L ≤ L ⊔ K from le_sup_left).trans le_sup_left
    · refine sup_le ?_ ?_
      · exact (show K ≤ L ⊔ K from le_sup_right).trans le_sup_left
      · exact hWU.trans le_sup_right
  exact hle hySupV

theorem

continuousMonoidHom_ext_openNormalQuotients

L289 ↗

ProCGroups.ProC.continuousMonoidHom_ext_openNormalQuotients

Documentation

Continuous homomorphisms into a profinite group are equal if they agree after every open-normal finite quotient of the target.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.ProC
universe u v
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuousMonoidHom_ext_openNormalQuotients
    {A : Type u} [Group A] [TopologicalSpace A]
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    {φ ψ : A →ₜ* H}
    (h : ∀ U : OpenNormalSubgroup H,
      (OpenNormalSubgroup.quotientProj U).comp φ =
        (OpenNormalSubgroup.quotientProj U).comp ψ) :
    φ = ψ

Module documentation

Separation by open normal quotients

Declarations