Discrete subgroups of topological groups

Note that the instance Subgroup.isClosed_of_discrete does not live here, in order that it can be used in other files without requiring lots of group-theoretic imports.

def Subgroup.subgroupOfContinuousMulEquivOfLe {G : Type u_1} [Group G] [TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) : ↥(H.subgroupOf K) ≃ₜ* ↥H

If G has a topology, and H ≤ K are subgroups, then H as a subgroup of K is isomorphic, as a topological group, to H as a subgroup of G. This is subgroupOfEquivOfLe upgraded to a ContinuousMulEquiv.

Equations

• Subgroup.subgroupOfContinuousMulEquivOfLe hHK = (Subgroup.subgroupOfEquivOfLe hHK).toContinuousMulEquiv ⋯

def AddSubgroup.addSubgroupOfContinuousAddEquivOfLe {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K) : ↥(H.addSubgroupOf K) ≃ₜ+ ↥H

If G has a topology, and H ≤ K are subgroups, then H as a subgroup of K is isomorphic, as a topological group, to H as a subgroup of G. This is addSubgroupOfEquivOfLe upgraded to a ContinuousAddEquiv.

Equations

• AddSubgroup.addSubgroupOfContinuousAddEquivOfLe hHK = (AddSubgroup.addSubgroupOfEquivOfLe hHK).toContinuousAddEquiv ⋯

@[simp]

theorem AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K) (a : ↥(H.addSubgroupOf K)) : (addSubgroupOfContinuousAddEquivOfLe hHK) a = (addSubgroupOfEquivOfLe hHK) a

@[simp]

theorem Subgroup.subgroupOfContinuousMulEquivOfLe_apply {G : Type u_1} [Group G] [TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) (a : ↥(H.subgroupOf K)) : (subgroupOfContinuousMulEquivOfLe hHK) a = (subgroupOfEquivOfLe hHK) a

@[simp]

theorem Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) (g : ↥H) : (subgroupOfContinuousMulEquivOfLe hHK).symm g = ⟨⟨↑g, ⋯⟩, ⋯⟩

@[simp]

theorem AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_symm_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K) (g : ↥H) : (addSubgroupOfContinuousAddEquivOfLe hHK).symm g = ⟨⟨↑g, ⋯⟩, ⋯⟩

@[simp]

theorem Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv {G : Type u_1} [Group G] [TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) : ↑(subgroupOfContinuousMulEquivOfLe hHK) = subgroupOfEquivOfLe hHK

@[simp]

theorem AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_toAddEquiv {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K) : ↑(addSubgroupOfContinuousAddEquivOfLe hHK) = addSubgroupOfEquivOfLe hHK

theorem Subgroup.discreteTopology_iff_of_finiteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Subgroup G} [H.FiniteIndex] : DiscreteTopology ↥H ↔ DiscreteTopology G

If G is a topological group and H a finite-index subgroup, then G is topologically discrete iff H is.

theorem AddSubgroup.discreteTopology_iff_of_finiteIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [H.FiniteIndex] : DiscreteTopology ↥H ↔ DiscreteTopology G

theorem Subgroup.discreteTopology_iff_of_isFiniteRelIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H K : Subgroup G} (hHK : H ≤ K) [H.IsFiniteRelIndex K] : DiscreteTopology ↥H ↔ DiscreteTopology ↥K

theorem AddSubgroup.discreteTopology_iff_of_isFiniteRelIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H K : AddSubgroup G} (hHK : H ≤ K) [H.IsFiniteRelIndex K] : DiscreteTopology ↥H ↔ DiscreteTopology ↥K

theorem Subgroup.Commensurable.discreteTopology_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H K : Subgroup G} (h : H.Commensurable K) : DiscreteTopology ↥H ↔ DiscreteTopology ↥K

theorem AddSubgroup.Commensurable.discreteTopology_iff {G : Type u_2} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H K : AddSubgroup G} (h : H.Commensurable K) : DiscreteTopology ↥H ↔ DiscreteTopology ↥K