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.
Topology of the general linear group #
theorem
Matrix.GeneralLinearGroup.continuous_apply
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
{α : Type u_4}
[TopologicalSpace α]
(f : α → GL n R)
(hf : Continuous f)
(i : n)
:
Continuous fun (x : α) => ↑(f x) i
theorem
Continuous.generalLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : Continuous ⇑f)
:
theorem
Topology.IsInducing.generalLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : IsInducing ⇑f)
:
theorem
Topology.IsEmbedding.generalLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : IsEmbedding ⇑f)
:
theorem
Topology.IsClosedEmbedding.generalLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
[IsTopologicalRing R]
[T0Space R]
(hf : IsClosedEmbedding ⇑f)
:
theorem
Matrix.GeneralLinearGroup.continuous_det
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The determinant is continuous as a map from the general linear group to the units.
theorem
Matrix.GeneralLinearGroup.continuous_upperRightHom
{R : Type u_4}
[Ring R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
Topology of the special linear group #
@[implicit_reducible]
instance
Matrix.SpecialLinearGroup.instTopologicalSpace
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
:
Equations
- Matrix.SpecialLinearGroup.instTopologicalSpace = { IsOpen := Matrix.SpecialLinearGroup.instTopologicalSpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
theorem
Matrix.SpecialLinearGroup.continuous_apply
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
{α : Type u_4}
[TopologicalSpace α]
(f : α → SpecialLinearGroup n R)
(hf : Continuous f)
(i : n)
:
Continuous fun (x : α) => ↑(f x) i
theorem
Continuous.specialLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : Continuous ⇑f)
:
The topology on SL n R is functorial in R.
theorem
Topology.IsInducing.specialLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : IsInducing ⇑f)
:
theorem
Topology.IsEmbedding.specialLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
(hf : IsEmbedding ⇑f)
:
instance
Matrix.SpecialLinearGroup.instDiscreteTopology
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[DiscreteTopology R]
:
If R is a commutative ring with the discrete topology, then SL(n, R) has the discrete
topology.
theorem
Matrix.SpecialLinearGroup.isClosedEmbedding_val
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
[T1Space R]
:
theorem
Topology.IsClosedEmbedding.specialLinearGroup_map
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
{f : R →+* S}
[IsTopologicalRing R]
[T1Space R]
(hf : IsClosedEmbedding ⇑f)
:
instance
Matrix.SpecialLinearGroup.instT1Space
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
[T1Space R]
:
T1Space (SpecialLinearGroup n R)
instance
Matrix.SpecialLinearGroup.topologicalGroup
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The special linear group over a topological ring is a topological group.
Mapping SL(n, R) to GL(n, R) #
theorem
Matrix.SpecialLinearGroup.continuous_toGL
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
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]
:
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]
:
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_4}
[CommRing A]
:
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]
:
The natural inclusion of SL n A in GL n A is a closed embedding.
Shortcuts for the composite SL(n, R) → GL(n, S) #
theorem
Matrix.SpecialLinearGroup.continuous_mapGL
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
[Algebra R S]
[IsTopologicalRing S]
[ContinuousSMul R S]
:
Continuous ⇑(mapGL S)
theorem
Matrix.SpecialLinearGroup.isInducing_mapGL
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
[Algebra R S]
[IsTopologicalRing S]
(h : Topology.IsInducing ⇑(algebraMap R S))
:
Topology.IsInducing ⇑(mapGL S)
theorem
Matrix.SpecialLinearGroup.isEmbedding_mapGL
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
[Algebra R S]
[IsTopologicalRing S]
(h : Topology.IsEmbedding ⇑(algebraMap R S))
:
theorem
Matrix.SpecialLinearGroup.isClosedEmbedding_mapGL
{n : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[CommRing S]
[TopologicalSpace S]
[Algebra R S]
[IsTopologicalRing S]
[IsTopologicalRing R]
[T1Space R]
[T1Space S]
(h : Topology.IsClosedEmbedding ⇑(algebraMap R S))
: