Topology on matrix groups

Lemmas about the topology of matrix groups, such as GL(n, R) and SL(n, R) for a topological ring R.

Lemmas about matrix groups

theorem Matrix.GeneralLinearGroup.continuous_det {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : Continuous ⇑det

The determinant is continuous as a map from the general linear group to the units.

theorem Matrix.GeneralLinearGroup.continuous_upperRightHom {R : Type u_3} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] : Continuous ⇑upperRightHom

@[implicit_reducible]

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

Equations

• Matrix.SpecialLinearGroup.instTopologicalSpace = instTopologicalSpaceSubtype

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

If R is a commutative ring with the discrete topology, then SL(n, R) has the discrete topology.

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

The special linear group over a topological ring is a topological group.

theorem Matrix.SpecialLinearGroup.continuous_toGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : Continuous ⇑toGL

The natural map from SL n A to GL n A is continuous.

theorem Matrix.SpecialLinearGroup.isInducing_toGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : Topology.IsInducing ⇑toGL

The natural map from SL n A to GL n A is inducing, i.e. the topology on SL n A is the pullback of the topology from GL n A.

theorem Matrix.SpecialLinearGroup.isEmbedding_toGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : Topology.IsEmbedding ⇑toGL

The natural map from SL n A in GL n A is an embedding, i.e. it is an injection and the topology on SL n A coincides with the subspace topology from GL n A.

theorem Matrix.SpecialLinearGroup.range_toGL {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_3} [CommRing A] : Set.range ⇑toGL = ⇑GeneralLinearGroup.det ⁻¹' {1}

theorem Matrix.SpecialLinearGroup.isClosedEmbedding_toGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T0Space R] : Topology.IsClosedEmbedding ⇑toGL

The natural inclusion of SL n A in GL n A is a closed embedding.

theorem Matrix.SpecialLinearGroup.isInducing_mapGL {n : Type u_3} [Fintype n] [DecidableEq n] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing B] (h : Topology.IsInducing ⇑(algebraMap A B)) : Topology.IsInducing ⇑(mapGL B)

theorem Matrix.SpecialLinearGroup.isEmbedding_mapGL {n : Type u_3} [Fintype n] [DecidableEq n] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing B] (h : Topology.IsEmbedding ⇑(algebraMap A B)) : Topology.IsEmbedding ⇑(mapGL B)