[Merged by Bors] - feat(topology/algebra/group): discrete subgroup acts properly discontinuously

[hrmacbeth]

A discrete subgroup of a topological group acts properly discontinuously on the left and on the right. Here discrete means finite intersection with any compact subset.

Co-authored-by: Alex Kontorovich 58564076+AlexKontorovich@users.noreply.github.com

---

[ocfnash]

I think it is worth avoiding the word "discrete" here since there are two possible meanings. How about:

Suggested change

	/-- A discrete subgroup of a topological group `G` acts on `G` properly discontinuously on the left.
	-/
	/-- Given a subgroup `S` of topological group `G`, if `S ∩ K` is finite for all compact `K`, then `S` acts on `G` properly discontinuously on the left.
	-/

The second meaning is that one might mean S gets the discrete topology. Of course they're related: I think the following is true:

example {α : Type*} [topological_space α] [locally_compact_space α] [t2_space α]
  (s : set α) (hs : is_closed s) :
  tendsto (coe : s → α) filter.cofinite (cocompact α) ↔ discrete_topology s :=

but missing from Mathlib.

See also

mathlib/src/topology/instances/real.lean

Line 233 in b381419

lemma tendsto_zmultiples_hom_cofinite {a : ℝ} (ha : a ≠ 0) :

vs

mathlib/src/analysis/normed_space/basic.lean

Line 165 in b381419

instance {E : Type*} [normed_add_comm_group E] [normed_space ℚ E] (e : E) :

[hrmacbeth]

I actually would like to leave in the word "discrete", because it's clearly related, and someone might search mathlib using that term. How about a phrasing which makes clear that this is not necessarily the standard use, like

A subgroup S of topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also discrete_topology.)

And indeed, someone should figure out and Lean-ify what the relationship between the concepts is.

[ocfnash]

Perfect; go for it.

[ocfnash]

One remark about terminology in comments but otherwise LGTM.

bors d+

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests