Module

ClosedSubgroupNeighborhoods.lean

Nyll.ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

2 declarations indexed from sourceView source ↗

Module documentation

Open-normal neighborhoods of closed subgroups

Given an open neighborhood of a closed subgroup, this file finds an open normal subgroup whose intersection with the closed subgroup lies in that neighborhood, including a version whose finite quotient belongs to a prescribed class.

Imports3

Imported by5

theorem

exists_openNormalSubgroup_inter_closedSubgroup_le

L34 ↗

ProCGroups.ProC.exists_openNormalSubgroup_inter_closedSubgroup_le

Documentation

Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the intersection with an ambient open normal subgroup.

Source context 6 commands

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

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

Lean source · statement

theorem exists_openNormalSubgroup_inter_closedSubgroup_le
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (H : ClosedSubgroup G) (U : OpenSubgroup H) :
    ∃ V : OpenNormalSubgroup G,
      (OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V : Subgroup H) ≤
        (U : Subgroup H)

theorem

exists_openNormalSubgroupInClass_inter_closedSubgroup_le

L57 ↗

ProCGroups.ProC.exists_openNormalSubgroupInClass_inter_closedSubgroup_le