NYLL
Module

QuotientFormation.lean

Nyll.ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
18 declarations indexed from sourceView source ↗

Module documentation

Quotient formations and their subgroup topology

A quotient formation specifies admissible normal quotient kernels and their closure properties. This file defines the induced open subgroups, pro-\(C\) closure, closed subgroups, and residuality, and proves their basic lattice and separation characterizations.

Imports1
  • Mathlib.Topology.Algebra.Group.Basic
Imported by2

Declarations

structure

QuotientFormation

L28 ↗
ProCGroups.Topologies.QuotientFormation
Documentation

A quotient formation records which quotient subgroups belong to the chosen class and the closure properties needed for the pro-\(C\) topology.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
Lean source · full declaration
structure QuotientFormation where
  /-- The predicate selecting the subgroups that define admissible quotients. -/
  contains : ∀ {G : Type u} [Group G], Subgroup G → Prop
  /-- The whole group is an admissible quotient kernel. -/
  top_mem : ∀ {G : Type u} [Group G], contains (G := G) (⊤ : Subgroup G)
  /-- Every admissible quotient kernel is normal. -/
  normal_of_mem : ∀ {G : Type u} [Group G] {N : Subgroup G}, contains (G := G) N → N.Normal
  /--
  An admissible kernel remains admissible when enlarged to a normal subgroup.
  -/
  upward_closed :
    ∀ {G : Type u} [Group G] {N K : Subgroup G},
      contains (G := G) N → N ≤ K → K.Normal → contains (G := G) K
  /-- The intersection of two admissible quotient kernels is admissible. -/
  inf_closed :
    ∀ {G : Type u} [Group G] {N K : Subgroup G},
      contains (G := G) N → contains (G := G) K → contains (G := G) (N ⊓ K)
def

IsOpenSubgroup

L54 ↗
ProCGroups.Topologies.QuotientFormation.IsOpenSubgroup
Documentation

A subgroup is open in the pro-\(C\) topology if and only if it contains one of the basic kernels.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
Lean source · statement
def IsOpenSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop
def

proCClosure

L58 ↗
ProCGroups.Topologies.QuotientFormation.proCClosure
Documentation

Algebraic closure operator attached to the pro-\(C\) topology.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
Lean source · statement
def proCClosure {G : Type u} [Group G] (H : Subgroup G) : Subgroup G
def

IsClosedSubgroup

L65 ↗
ProCGroups.Topologies.QuotientFormation.IsClosedSubgroup
Documentation

A subgroup is closed in the algebraic pro-\(C\) topology exactly when it equals its pro-\(C\) closure.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
Lean source · statement
def IsClosedSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop
def

IsResiduallyC

L69 ↗
ProCGroups.Topologies.QuotientFormation.IsResiduallyC
Documentation

Residuality for the pro-\(C\) topology: the identity is separated by the basic open kernels.

Source context 6 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
Lean source · statement
def IsResiduallyC {G : Type u} [Group G] : Prop
theorem

isOpenSubgroup_top

L76 ↗
ProCGroups.Topologies.QuotientFormation.isOpenSubgroup_top
Documentation

The whole group is open for a quotient formation.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isOpenSubgroup_top (C : QuotientFormation) :
    C.IsOpenSubgroup (⊤ : Subgroup G)
theorem

isOpenSubgroup_sup_left

L84 ↗
ProCGroups.Topologies.QuotientFormation.isOpenSubgroup_sup_left
Documentation

A subgroup containing an open subgroup for a quotient formation is open in the left-hand quotient-formation topology.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isOpenSubgroup_sup_left (C : QuotientFormation) {H K : Subgroup G}
    (hH : C.IsOpenSubgroup H) :
    C.IsOpenSubgroup (H ⊔ K)
theorem

isOpenSubgroup_sup_right

L94 ↗
ProCGroups.Topologies.QuotientFormation.isOpenSubgroup_sup_right
Documentation

A subgroup containing an open subgroup for a quotient formation is open in the right-hand quotient-formation topology.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isOpenSubgroup_sup_right (C : QuotientFormation) {H K : Subgroup G}
    (hK : C.IsOpenSubgroup K) :
    C.IsOpenSubgroup (H ⊔ K)
theorem

le_proCClosure

L101 ↗
ProCGroups.Topologies.QuotientFormation.le_proCClosure
Documentation

A subgroup is contained in its pro-\(C\) closure.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem le_proCClosure (C : QuotientFormation) (H : Subgroup G) :
    H ≤ C.proCClosure H
theorem

proCClosure_mono

L107 ↗
ProCGroups.Topologies.QuotientFormation.proCClosure_mono
Documentation

The pro-\(C\) closure operation is monotone.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem proCClosure_mono (C : QuotientFormation) {H K : Subgroup G}
    (hHK : H ≤ K) :
    C.proCClosure H ≤ C.proCClosure K
theorem

proCClosure_idem

L118 ↗
ProCGroups.Topologies.QuotientFormation.proCClosure_idem
Documentation

The pro-\(C\) closure operation is idempotent.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem proCClosure_idem (C : QuotientFormation) (H : Subgroup G) :
    C.proCClosure (C.proCClosure H) = C.proCClosure H
theorem

isClosedSubgroup_iff_proCClosure_le

L132 ↗
ProCGroups.Topologies.QuotientFormation.isClosedSubgroup_iff_proCClosure_le
Documentation

Closed subgroups for the quotient formation are exactly those containing the pro-\(C\) closure of every smaller subgroup.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isClosedSubgroup_iff_proCClosure_le {C : QuotientFormation} {H : Subgroup G} :
    C.IsClosedSubgroup H ↔ C.proCClosure H ≤ H
theorem

isResiduallyC_iff_proCClosure_bot_eq_bot

L144 ↗
ProCGroups.Topologies.QuotientFormation.isResiduallyC_iff_proCClosure_bot_eq_bot
Documentation

Residual \(C\)-ness is equivalent to the pro-\(C\) closure of the bottom subgroup being bottom.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isResiduallyC_iff_proCClosure_bot_eq_bot {C : QuotientFormation} :
    C.IsResiduallyC (G := G) ↔ C.proCClosure (⊥ : Subgroup G) = ⊥
theorem

exists_openSubgroup_not_mem_of_not_mem_proCClosure

L152 ↗
ProCGroups.Topologies.QuotientFormation.exists_openSubgroup_not_mem_of_not_mem_proCClosure
Documentation

An element outside the pro-\(C\) closure is separated by an open subgroup in the quotient formation.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem exists_openSubgroup_not_mem_of_not_mem_proCClosure
    (C : QuotientFormation) {H : Subgroup G} {x : G}
    (hx : x ∉ C.proCClosure H) :
    ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ H ≤ K ∧ x ∉ K
theorem

exists_openSubgroup_not_mem_of_isResiduallyC

L165 ↗
ProCGroups.Topologies.QuotientFormation.exists_openSubgroup_not_mem_of_isResiduallyC
Documentation

In a residually \(C\) group, a nontrivial element is excluded by some open subgroup in the quotient formation.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem exists_openSubgroup_not_mem_of_isResiduallyC
    (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
    {x : G} (hx : x ≠ 1) :
    ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ x ∉ K
theorem

normalCore_mem_of_open

L177 ↗
ProCGroups.Topologies.QuotientFormation.normalCore_mem_of_open
Documentation

The normal core of an open subgroup again defines a quotient in the formation.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem normalCore_mem_of_open (C : QuotientFormation) {H : Subgroup G}
    (hH : C.IsOpenSubgroup H) :
    C.contains H.normalCore
theorem

exists_openKernel_not_mem_of_isResiduallyC

L189 ↗
ProCGroups.Topologies.QuotientFormation.exists_openKernel_not_mem_of_isResiduallyC
Documentation

In a residually \(C\) group, a nontrivial element is excluded by an open normal kernel in the quotient formation.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem exists_openKernel_not_mem_of_isResiduallyC
    (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
    {x : G} (hx : x ≠ 1) :
    ∃ N : Subgroup G, C.contains N ∧ N.Normal ∧ x ∉ N
theorem

isClosedSubgroup_iff_exists_sInf_openSubgroups

L201 ↗
ProCGroups.Topologies.QuotientFormation.isClosedSubgroup_iff_exists_sInf_openSubgroups
Documentation

Closed subgroups are exactly intersections of open subgroups.

Source context 8 commands

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

open Set
open scoped Topology
namespace ProCGroups.Topologies
universe u
namespace QuotientFormation
variable (C : QuotientFormation)
variable {C}
variable {G : Type u} [Group G]
Lean source · statement
theorem isClosedSubgroup_iff_exists_sInf_openSubgroups
    {C : QuotientFormation} {H : Subgroup G} :
    C.IsClosedSubgroup H ↔
      ∃ S : Set (Subgroup G), (∀ K ∈ S, C.IsOpenSubgroup K) ∧ H = sInf S

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