Closed subgroups of a topological group

This file builds the frame of closed subgroups in a topological group G, and its additive version ClosedAddSubgroup.

Main definitions and results

• normalCore_isClosed: The normalCore of a closed subgroup is closed.

• finindex_closedSubgroup_isOpen: A closed subgroup with finite index is open.

TODO

Actually provide the Order.Frame (ClosedSubgroup G) instance.

structure ClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] extends Subgroup G : Type u

The type of closed subgroups of a topological group.

• carrier : Set G
• mul_mem' {a b : G} : a ∈ (↑self).carrier → b ∈ (↑self).carrier → a * b ∈ (↑self).carrier
• one_mem' : 1 ∈ (↑self).carrier
• inv_mem' {x : G} : x ∈ (↑self).carrier → x⁻¹ ∈ (↑self).carrier
• isClosed' : IsClosed (↑self).carrier

theorem ClosedSubgroup.ext_iff {G : Type u} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {x y : ClosedSubgroup G} : x = y ↔ (↑x).carrier = (↑y).carrier

theorem ClosedSubgroup.ext {G : Type u} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {x y : ClosedSubgroup G} (carrier : (↑x).carrier = (↑y).carrier) : x = y

structure ClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] extends AddSubgroup G : Type u

The type of closed subgroups of an additive topological group.

• carrier : Set G
• add_mem' {a b : G} : a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
• zero_mem' : 0 ∈ (↑self).carrier
• neg_mem' {x : G} : x ∈ (↑self).carrier → -x ∈ (↑self).carrier
• isClosed' : IsClosed (↑self).carrier

theorem ClosedAddSubgroup.ext {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : ClosedAddSubgroup G} (carrier : (↑x).carrier = (↑y).carrier) : x = y

theorem ClosedAddSubgroup.ext_iff {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : ClosedAddSubgroup G} : x = y ↔ (↑x).carrier = (↑y).carrier

theorem ClosedSubgroup.toSubgroup_injective {G : Type u} [Group G] [TopologicalSpace G] : Function.Injective toSubgroup

theorem ClosedAddSubgroup.toAddSubgroup_injective {G : Type u} [AddGroup G] [TopologicalSpace G] : Function.Injective toAddSubgroup

instance ClosedSubgroup.instSetLike (G : Type u) [Group G] [TopologicalSpace G] : SetLike (ClosedSubgroup G) G

instance ClosedAddSubgroup.instSetLike (G : Type u) [AddGroup G] [TopologicalSpace G] : SetLike (ClosedAddSubgroup G) G

instance ClosedSubgroup.instPartialOrder (G : Type u) [Group G] [TopologicalSpace G] : PartialOrder (ClosedSubgroup G)

instance ClosedAddSubgroup.instPartialOrder (G : Type u) [AddGroup G] [TopologicalSpace G] : PartialOrder (ClosedAddSubgroup G)

instance ClosedSubgroup.instSubgroupClass (G : Type u) [Group G] [TopologicalSpace G] : SubgroupClass (ClosedSubgroup G) G

instance ClosedAddSubgroup.instAddSubgroupClass (G : Type u) [AddGroup G] [TopologicalSpace G] : AddSubgroupClass (ClosedAddSubgroup G) G

instance ClosedSubgroup.instCoeSubgroup (G : Type u) [Group G] [TopologicalSpace G] : Coe (ClosedSubgroup G) (Subgroup G)

instance ClosedAddSubgroup.instCoeAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] : Coe (ClosedAddSubgroup G) (AddSubgroup G)

instance ClosedSubgroup.instInfClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] : Min (ClosedSubgroup G)

instance ClosedAddSubgroup.instInfClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] : Min (ClosedAddSubgroup G)

instance ClosedSubgroup.instSemilatticeInfClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] : SemilatticeInf (ClosedSubgroup G)

instance ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] : SemilatticeInf (ClosedAddSubgroup G)

instance ClosedSubgroup.instCompactSpaceSubtypeMem (G : Type u) [Group G] [TopologicalSpace G] [CompactSpace G] (H : ClosedSubgroup G) : CompactSpace ↥H

instance ClosedAddSubgroup.instCompactSpaceSubtypeMem (G : Type u) [AddGroup G] [TopologicalSpace G] [CompactSpace G] (H : ClosedAddSubgroup G) : CompactSpace ↥H

theorem Subgroup.normalCore_isClosed {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) (h : IsClosed ↑H) : IsClosed ↑H.normalCore

theorem Subgroup.isOpen_of_isClosed_of_finiteIndex {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) [H.FiniteIndex] (h : IsClosed ↑H) : IsOpen ↑H

theorem AddSubgroup.isOpen_of_isClosed_of_finiteIndex {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) [H.FiniteIndex] (h : IsClosed ↑H) : IsOpen ↑H