Pointwise operations on sets in topological groups

Topological operations on pointwise sums and products

A few results about interior and closure of the pointwise addition/multiplication of sets in groups with continuous addition/multiplication. See also Submonoid.top_closure_mul_self_eq in Topology.Algebra.Monoid.

theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s • interior t ⊆ interior (s • t)

theorem subset_interior_vadd {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem IsClosed.smul_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s • t)

theorem IsClosed.vadd_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s +ᵥ t)

One may expect a version of IsClosed.smul_left_of_isCompact where t is compact and s is closed, but such a lemma can't be true in this level of generality. For a counterexample, consider ℚ acting on ℝ by translation, and let s : Set ℚ := univ, t : set ℝ := {0}. Then s is closed and t is compact, but s +ᵥ t is the set of all rationals, which is definitely not closed in ℝ. To fix the proof, we would need to make two additional assumptions:

• for any x ∈ t, s • {x} is closed
• for any x ∈ t, there is a continuous function g : s • {x} → s such that, for all y ∈ s • {x}, we have y = (g y) • x These are fairly specific hypotheses so we don't state this version of the lemmas, but an interesting fact is that these two assumptions are verified in the case of a NormedAddTorsor (or really, any AddTorsor with continuous -ᵥ). We prove this special case in IsClosed.vadd_right_of_isCompact.

theorem MulAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem AddAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem IsOpen.mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : IsOpen t → IsOpen (s * t)

theorem IsOpen.add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : IsOpen t → IsOpen (s + t)

theorem subset_interior_mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : s * interior t ⊆ interior (s * t)

theorem subset_interior_add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : s + interior t ⊆ interior (s + t)

theorem subset_interior_mul {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem subset_interior_add {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem singleton_mul_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} * s ∈ nhds (a * b)

theorem singleton_add_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} + s ∈ nhds (a + b)

theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) (h : s ∈ nhds 1) : {a} * s ∈ nhds a

theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) (h : s ∈ nhds 0) : {a} + s ∈ nhds a

theorem IsOpen.mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} (hs : IsOpen s) : IsOpen (s * t)

theorem IsOpen.add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} (hs : IsOpen s) : IsOpen (s + t)

theorem subset_interior_mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} : interior s * t ⊆ interior (s * t)

theorem subset_interior_add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} : interior s + t ⊆ interior (s + t)

theorem subset_interior_mul' {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem subset_interior_add' {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem mul_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s * {a} ∈ nhds (b * a)

theorem add_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s + {a} ∈ nhds (b + a)

theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 1) : s * {a} ∈ nhds a

theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 0) : s + {a} ∈ nhds a

theorem IsOpen.div_left {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsOpen t) : IsOpen (s / t)

theorem IsOpen.sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsOpen t) : IsOpen (s - t)

theorem IsOpen.div_right {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (hs : IsOpen s) : IsOpen (s / t)

theorem IsOpen.sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (hs : IsOpen s) : IsOpen (s - t)

theorem subset_interior_div_left {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : interior s / t ⊆ interior (s / t)

theorem subset_interior_sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - t ⊆ interior (s - t)

theorem subset_interior_div_right {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : s / interior t ⊆ interior (s / t)

theorem subset_interior_sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : s - interior t ⊆ interior (s - t)

theorem subset_interior_div {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : interior s / interior t ⊆ interior (s / t)

theorem subset_interior_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - interior t ⊆ interior (s - t)

theorem IsOpen.mul_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s * closure t = s * t

theorem IsOpen.add_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s + closure t = s + t

theorem IsOpen.closure_mul {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s * t = s * t

theorem IsOpen.closure_add {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s + t = s + t

theorem IsOpen.div_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s / closure t = s / t

theorem IsOpen.sub_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s - closure t = s - t

theorem IsOpen.closure_div {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s / t = s / t

theorem IsOpen.closure_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s - t = s - t

theorem IsClosed.mul_left_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t)

theorem IsClosed.add_left_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s + t)

theorem IsClosed.mul_right_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t * s)

theorem IsClosed.add_right_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t + s)

theorem subset_mul_closure_one {G : Type u_1} [MulOneClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s * closure {1}

theorem subset_add_closure_zero {G : Type u_1} [AddZeroClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s + closure {0}

theorem IsCompact.mul_closure_one_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) : K * closure {1} = closure K

theorem IsCompact.add_closure_zero_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) : K + closure {0} = closure K

theorem IsClosed.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {F : Set G} (hF : IsClosed F) : F * closure {1} = F

theorem IsClosed.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Set G} (hF : IsClosed F) : F + closure {0} = F

theorem compl_mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : t * closure {1} = t) : tᶜ * closure {1} = tᶜ

theorem compl_add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : t + closure {0} = t) : tᶜ + closure {0} = tᶜ

theorem compl_mul_closure_one_eq_iff {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} : tᶜ * closure {1} = tᶜ ↔ t * closure {1} = t

theorem compl_add_closure_zero_eq_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} : tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t

theorem IsOpen.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (hU : IsOpen U) : U * closure {1} = U

theorem IsOpen.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : IsOpen U) : U + closure {0} = U

@[instance 100]

instance IsTopologicalGroup.regularSpace (G : Type w) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : RegularSpace G

@[instance 100]

instance IsTopologicalAddGroup.regularSpace (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : RegularSpace G

theorem group_inseparable_iff {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {x y : G} : Inseparable x y ↔ x / y ∈ closure 1

theorem addGroup_inseparable_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x y : G} : Inseparable x y ↔ x - y ∈ closure 0

theorem IsTopologicalGroup.t2Space_iff_one_closed {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : T2Space G ↔ IsClosed {1}

theorem IsTopologicalAddGroup.t2Space_iff_zero_closed {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : T2Space G ↔ IsClosed {0}

theorem IsTopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (H : ∀ (x : G), x ≠ 1 → ∃ U ∈ nhds 1, x ∉ U) : T2Space G

theorem IsTopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (H : ∀ (x : G), x ≠ 0 → ∃ U ∈ nhds 0, x ∉ U) : T2Space G

theorem exists_closed_nhds_one_inv_eq_mul_subset {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (hU : U ∈ nhds 1) : ∃ V ∈ nhds 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V * V ⊆ U.

theorem exists_closed_nhds_zero_neg_eq_add_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V + V ⊆ U.

theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

If a point in a topological group has a compact neighborhood, then the group is locally compact.

theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has compact support, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has compact support, then either the function is trivial or the group is locally compact.