NYLL
Module

Basic.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
29 declarations indexed from sourceView source ↗

Module documentation

Basic operations on open normal subgroups

This file develops bundled open normal subgroups, their finite discrete quotients and projections, maps and comaps, transition morphisms, normal cores, and finite intersections.

Imports4
Imported by29

Declarations

instance

instTopOpenNormalSubgroup

L30 ↗
ProCGroups.ProC.OpenNormalSubgroup.instTopOpenNormalSubgroup
Documentation

Open normal subgroups have a top element: the whole group.

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]
namespace OpenNormalSubgroup
Lean source · statement
instance instTopOpenNormalSubgroup : Top (OpenNormalSubgroup G)
def

ker

L37 ↗
ProCGroups.ProC.OpenNormalSubgroup.ker
Documentation

The kernel of a continuous homomorphism into a discrete group is an open normal subgroup.

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]
namespace OpenNormalSubgroup
Lean source · full declaration
def ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (f : G →ₜ* Q) : OpenNormalSubgroup G where
  toOpenSubgroup :=
    { toSubgroup := f.toMonoidHom.ker
      isOpen' := by
        change IsOpen (f ⁻¹' ({1} : Set Q))
        exact (isOpen_discrete _).preimage f.continuous_toFun }
  isNormal' := by
    change f.toMonoidHom.ker.Normal
    infer_instance
theorem

toSubgroup_ker

L50 ↗
ProCGroups.ProC.OpenNormalSubgroup.toSubgroup_ker
Documentation

The underlying subgroup of OpenNormalSubgroup.kernel is the algebraic kernel.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem toSubgroup_ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (f : G →ₜ* Q) :
    ((ker f : OpenNormalSubgroup G) : Subgroup G) = f.toMonoidHom.ker
theorem

mem_ker

L57 ↗
ProCGroups.ProC.OpenNormalSubgroup.mem_ker
Documentation

Membership in the open normal kernel is exactly mapping to \(1\).

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem mem_ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    {f : G →ₜ* Q} {x : G} :
    x ∈ ker f ↔ f x = 1
def

map

L65 ↗
ProCGroups.ProC.OpenNormalSubgroup.map
Documentation

An open surjective continuous homomorphism sends open normal subgroups to open normal subgroups.

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]
namespace OpenNormalSubgroup
Lean source · full declaration
def map {H : Type v} [Group H] [TopologicalSpace H]
    (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
    (U : OpenNormalSubgroup G) : OpenNormalSubgroup H where
  toOpenSubgroup :=
    { toSubgroup := (U : Subgroup G).map f.toMonoidHom
      isOpen' := by
        change IsOpen (f '' ((U : Subgroup G) : Set G))
        exact hfopen _ (openNormalSubgroup_isOpen (G := G) U) }
  isNormal' := by
    change ((U : Subgroup G).map f.toMonoidHom).Normal
    exact Subgroup.Normal.map U.isNormal' f.toMonoidHom hfsurj
theorem

toSubgroup_map

L79 ↗
ProCGroups.ProC.OpenNormalSubgroup.toSubgroup_map
Documentation

The underlying subgroup of the image open normal subgroup is the subgroup image.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem toSubgroup_map {H : Type v} [Group H] [TopologicalSpace H]
    (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
    (U : OpenNormalSubgroup G) :
    ((map f hfopen hfsurj U : OpenNormalSubgroup H) : Subgroup H) =
      (U : Subgroup G).map f.toMonoidHom
def

quotientMapContinuousMulEquiv

L89 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientMapContinuousMulEquiv
Documentation

A multiplicative homeomorphism identifies a quotient with the quotient by the image of an open normal subgroup. This is the source-producing transport used to prove that the canonical pro-C object property is invariant under isomorphism.

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]
namespace OpenNormalSubgroup
Lean source · statement
def quotientMapContinuousMulEquiv
    {H : Type u} [Group H] [TopologicalSpace H]
    (e : G ≃ₜ* H) (U : OpenNormalSubgroup G) :
    G ⧸ (U : Subgroup G) ≃*
      H ⧸ ((map (ContinuousMonoidHom.toContinuousMonoidHom e)
        (Homeomorph.isOpenMap e.toHomeomorph) e.surjective U : OpenNormalSubgroup H) :
          Subgroup H)
def

quotientProj

L141 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj
Documentation

The canonical quotient projection attached to an open normal subgroup.

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]
namespace OpenNormalSubgroup
Lean source · full declaration
def quotientProj (U : OpenNormalSubgroup G) : G →ₜ* G ⧸ (U : Subgroup G) where
  toMonoidHom := QuotientGroup.mk' (U : Subgroup G)
  continuous_toFun := continuous_quotient_mk'
instance

quotientFinite

L146 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientFinite
Documentation

Quotients by open normal subgroups of compact groups are finite.

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]
namespace OpenNormalSubgroup
Lean source · statement
instance quotientFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
    Finite (G ⧸ (U : Subgroup G))
instance

quotientDiscrete

L151 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientDiscrete
Documentation

Quotients by open normal subgroups carry the discrete topology.

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]
namespace OpenNormalSubgroup
Lean source · statement
instance quotientDiscrete [ContinuousMul G] (U : OpenNormalSubgroup G) :
    DiscreteTopology (G ⧸ (U : Subgroup G))
theorem

quotientProj_toMonoidHom

L156 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj_toMonoidHom
Documentation

The induced pro-\(C\) map agrees with the corresponding finite-quotient construction.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem quotientProj_toMonoidHom (U : OpenNormalSubgroup G) :
    (quotientProj U).toMonoidHom = QuotientGroup.mk' (U : Subgroup G)
theorem

quotientProj_apply

L162 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj_apply
Documentation

The quotient projection sends an element to its quotient class.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem quotientProj_apply (U : OpenNormalSubgroup G) (x : G) :
    quotientProj U x = QuotientGroup.mk' (U : Subgroup G) x
theorem

quotientProj_surjective

L168 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj_surjective
Documentation

The quotient projection by an open normal subgroup is surjective.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem quotientProj_surjective (U : OpenNormalSubgroup G) :
    Function.Surjective (quotientProj U)
theorem

quotientProj_eq_one_iff

L174 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj_eq_one_iff
Documentation

The quotient projection maps an element to \(1\) exactly on the subgroup.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem quotientProj_eq_one_iff {U : OpenNormalSubgroup G} {x : G} :
    quotientProj U x = 1 ↔ x ∈ (U : Subgroup G)
theorem

quotientProj_eq_quotientProj_iff

L182 ↗
ProCGroups.ProC.OpenNormalSubgroup.quotientProj_eq_quotientProj_iff
Documentation

Equality under a quotient projection is membership of the quotient difference in the subgroup.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroup G} {x y : G} :
    quotientProj U x = quotientProj U y ↔ x / y ∈ (U : Subgroup G)
theorem

mem_ker_quotientProj

L190 ↗
ProCGroups.ProC.OpenNormalSubgroup.mem_ker_quotientProj
Documentation

Kernel membership for the quotient projection is subgroup membership.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroup G} {x : G} :
    x ∈ ker (quotientProj U) ↔ x ∈ (U : Subgroup G)
theorem

ker_quotientProj

L196 ↗
ProCGroups.ProC.OpenNormalSubgroup.ker_quotientProj
Documentation

The open normal kernel of the quotient projection is the original subgroup.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroup G) :
    ((ker (quotientProj U) : OpenNormalSubgroup G) : Subgroup G) = (U : Subgroup G)
theorem

ker_comp

L202 ↗
ProCGroups.ProC.OpenNormalSubgroup.ker_comp
Documentation

Kernels commute with composition of continuous homomorphisms into discrete groups.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem ker_comp {H : Type v} [Group H] [TopologicalSpace H]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (g : H →ₜ* Q) (f : G →ₜ* H) :
    ker (g.comp f) =
      OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun (ker g)
theorem

comap_ker

L212 ↗
ProCGroups.ProC.OpenNormalSubgroup.comap_ker
Documentation

The comap of a kernel is the kernel of the composite.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem comap_ker {H : Type v} [Group H] [TopologicalSpace H]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (f : G →ₜ* H) (g : H →ₜ* Q) :
    OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun (ker g) =
      ker (g.comp f)
theorem

comap_quotientProj

L221 ↗
ProCGroups.ProC.OpenNormalSubgroup.comap_quotientProj
Documentation

Comapping an open normal subgroup is the kernel of the composite quotient projection.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem comap_quotientProj {H : Type v} [Group H] [TopologicalSpace H] [ContinuousMul H]
    (f : G →ₜ* H) (U : OpenNormalSubgroup H) :
    OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U =
      ker ((quotientProj U).comp f)
def

transition

L229 ↗
ProCGroups.ProC.OpenNormalSubgroup.transition
Documentation

The natural transition map between quotients by open normal subgroups \(U\le V\).

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]
namespace OpenNormalSubgroup
Lean source · statement
def transition {U V : OpenNormalSubgroup G}
    (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
    G ⧸ (U : Subgroup G) →ₜ* G ⧸ (V : Subgroup G)
theorem

transition_mk

L238 ↗
ProCGroups.ProC.OpenNormalSubgroup.transition_mk
Documentation

Transition maps send quotient classes to quotient classes.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem transition_mk {U V : OpenNormalSubgroup G}
    (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) (x : G) :
    transition hUV (QuotientGroup.mk' (U : Subgroup G) x) =
      QuotientGroup.mk' (V : Subgroup G) x
theorem

transition_comp_quotientProj

L249 ↗
ProCGroups.ProC.OpenNormalSubgroup.transition_comp_quotientProj
Documentation

Composing a transition map with the smaller quotient projection gives the larger quotient projection.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem transition_comp_quotientProj {U V : OpenNormalSubgroup G}
    (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
    (transition hUV).comp (quotientProj U) = quotientProj V
theorem

transition_surjective

L255 ↗
ProCGroups.ProC.OpenNormalSubgroup.transition_surjective
Documentation

Transition maps between quotients by nested open normal subgroups are surjective.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem transition_surjective {U V : OpenNormalSubgroup G}
    (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
    Function.Surjective (transition hUV)
theorem

ker_transition

L264 ↗
ProCGroups.ProC.OpenNormalSubgroup.ker_transition
Documentation

The kernel of the transition map is the image of the larger subgroup in the smaller quotient.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem ker_transition {U V : OpenNormalSubgroup G}
    [ContinuousMul G]
    (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
    ((ker (transition hUV) : OpenNormalSubgroup (G ⧸ (U : Subgroup G))) :
        Subgroup (G ⧸ (U : Subgroup G))) =
      (V : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))
def

normalCore

L281 ↗
ProCGroups.ProC.OpenNormalSubgroup.normalCore
Documentation

The normal core of an open subgroup in a compact topological group is an open normal subgroup.

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]
namespace OpenNormalSubgroup
Lean source · full declaration
def normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
    OpenNormalSubgroup G where
  toOpenSubgroup :=
    { toSubgroup := Subgroup.normalCore (U : Subgroup G)
      isOpen' := by
        have hclosed : IsClosed ((U : Subgroup G) : Set G) :=
          openSubgroup_isClosed (G := G) U
        let : (U : Subgroup G).FiniteIndex :=
          Subgroup.finiteIndex_of_finite_quotient (H := (U : Subgroup G))
        exact Subgroup.isOpen_of_isClosed_of_finiteIndex _
          ((U : Subgroup G).normalCore_isClosed hclosed) }
  isNormal' := by
    change (Subgroup.normalCore (U : Subgroup G)).Normal
    infer_instance
theorem

toSubgroup_normalCore

L298 ↗
ProCGroups.ProC.OpenNormalSubgroup.toSubgroup_normalCore
Documentation

The underlying subgroup of \(\mathrm{normalCore}\) is the algebraic normal core.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem toSubgroup_normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
    ((normalCore U : OpenNormalSubgroup G) : Subgroup G) =
      Subgroup.normalCore (U : Subgroup G)
theorem

normalCore_le

L304 ↗
ProCGroups.ProC.OpenNormalSubgroup.normalCore_le
Documentation

The normal core of an open subgroup is contained in that open subgroup.

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]
namespace OpenNormalSubgroup
Lean source · statement
theorem normalCore_le [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
    (normalCore U : Subgroup G) ≤ (U : Subgroup G)
def

finsetInf

L309 ↗
ProCGroups.ProC.OpenNormalSubgroup.finsetInf
Documentation

The infimum of a finite family of open normal subgroups.

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]
namespace OpenNormalSubgroup
Lean source · statement
def finsetInf {ι : Type v} (s : Finset ι) (U : ι → OpenNormalSubgroup G) :
    OpenNormalSubgroup G

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