Convergence in special linear groups

The special linear group SL(n, R) carries the topology induced from the matrices, which is the product topology on the entries. So a sequence, or more generally a function along any filter, converges in SL(n, R) exactly when each of its entries converges. For the same reason SL(n, R) acts jointly continuously on column vectors, and it is second countable when R is; over a topological ring, so then is its quotient PSL(n, R). Over a T1 topological ring it is a closed subset of the matrices, so it is σ-compact when R is.

Main results

• Matrix.SpecialLinearGroup.tendsto_iff_tendsto_apply: convergence in SL(n, R) is entrywise convergence.
• Matrix.SpecialLinearGroup.instContinuousSMulVec: SL(n, R) acts jointly continuously on column vectors.
• Matrix.SpecialLinearGroup.instSigmaCompactSpace: over a σ-compact T1 topological ring, SL(n, R) is σ-compact.
• Matrix.SpecialLinearGroup.instSecondCountableTopology: over a second-countable ring, SL(n, R) is second countable, and hence so is its quotient PSL(n, R).
• Matrix.SpecialLinearGroup.exists_tendsto_dilation_conj: a sequence in SL(2, ℝ) whose first diagonal entry converges to that of a diagonal matrix D, and whose off-diagonal products tend to 0, converges to D after conjugating each term by a suitable power of a dilation.

theorem Matrix.SpecialLinearGroup.tendsto_iff_tendsto_apply {n : Type u_1} {R : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] {l : Filter α} {M : α → SpecialLinearGroup n R} {D : SpecialLinearGroup n R} : Filter.Tendsto M l (nhds D) ↔ ∀ (i j : n), Filter.Tendsto (fun (x : α) => ↑(M x) i j) l (nhds (↑D i j))

Convergence in SL(n, R) is entrywise convergence.

instance Matrix.SpecialLinearGroup.instContinuousSMulVec {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousMul R] : ContinuousSMul (SpecialLinearGroup n R) (n → R)

When addition and multiplication are continuous on R, SL(n, R) acts jointly continuously on column vectors, by restricting the action of all square matrices.

instance Matrix.SpecialLinearGroup.instSigmaCompactSpace {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] [SigmaCompactSpace R] : SigmaCompactSpace (SpecialLinearGroup n R)

Over a σ-compact T1 topological ring, SL(n, R) is σ-compact, as a closed subset of the σ-compact space of matrices.

instance Matrix.SpecialLinearGroup.instSecondCountableTopology {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [SecondCountableTopology R] : SecondCountableTopology (SpecialLinearGroup n R)

Over a second-countable ring, SL(n, R) is second countable, as a subspace of the second-countable space of matrices.

Over a topological ring, PSL(n, R) is the quotient of SL(n, R) by its centre, so it is then second countable as well, by QuotientGroup.instSecondCountableTopology; in particular SL(2, ℝ) and PSL(2, ℝ) are second countable.

theorem Matrix.SpecialLinearGroup.exists_tendsto_dilation_conj {s : ℝ} (hs : 0 < s) {M : ℕ → SpecialLinearGroup (Fin 2) ℝ} {D : SpecialLinearGroup (Fin 2) ℝ} (h00 : Filter.Tendsto (fun (n : ℕ) => ↑(M n) 0 0) Filter.atTop (nhds (↑D 0 0))) (hD01 : ↑D 0 1 = 0) (hD10 : ↑D 1 0 = 0) (hβ : Filter.Tendsto (fun (n : ℕ) => ↑(M n) 0 1 * ↑(M n) 1 0) Filter.atTop (nhds 0)) : ∃ (k : ℕ → ℤ), Filter.Tendsto (fun (n : ℕ) => dilation (↑(k n) * s) * M n * dilation (-(↑(k n) * s))) Filter.atTop (nhds D)

If the first diagonal entry of a sequence of matrices of SL(2, ℝ) converges to that of a diagonal matrix D and the products of its off-diagonal entries tend to 0, then conjugating each term by a suitable power of dilation s, s > 0, gives a sequence converging to D. The other diagonal entry then converges too, by the determinant.