The path component of the identity in a locally path connected topological group

This file defines the path component of the identity is an OpenNormalSubgroup when the ambient topological group is locally path connected. We place this in a separate file to avoid importing additional algebra into the topology hierarchy.

def OpenNormalSubgroup.pathComponentOne (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] : OpenNormalSubgroup G

The path component of the identity in a locally path connected topological group, as an open normal subgroup. It is, in fact, clopen.

Equations

• OpenNormalSubgroup.pathComponentOne G = { toSubgroup := Subgroup.pathComponentOne G, isOpen' := ⋯, isNormal' := ⋯ }

def OpenNormalAddSubgroup.pathComponentZero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyPathConnectedSpace G] : OpenNormalAddSubgroup G

The path component of the identity in a locally path connected additive topological group, as an open normal additive subgroup. It is, in fact, clopen.

Equations

• OpenNormalAddSubgroup.pathComponentZero G = { toAddSubgroup := AddSubgroup.pathComponentZero G, isOpen' := ⋯, isNormal' := ⋯ }

@[simp]

theorem OpenNormalSubgroup.pathComponentOne_carrier (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] : ↑(pathComponentOne G) = pathComponent 1

@[simp]

theorem OpenNormalAddSubgroup.pathComponentZero_carrier (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyPathConnectedSpace G] : ↑(pathComponentZero G) = pathComponent 0

instance OpenNormalSubgroup.instIsClosedCoePathComponentOne (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] : IsClosed ↑(pathComponentOne G)

instance OpenNormalAddSubgroup.instIsClosedCoePathComponentZero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyPathConnectedSpace G] : IsClosed ↑(pathComponentZero G)