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 an IsTopologicalAddTorsor. 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.