The topology of finite-dimensional linear automorphisms

The endomorphism algebra of a finite-dimensional vector space has its canonical module topology. Mathlib's IsModuleTopology.isTopologicalRing supplies continuous composition. The unit topology on that algebra records both an automorphism and its inverse. Transporting it along Mathlib's LinearMap.GeneralLinearGroup.generalLinearEquiv equips linear automorphisms with a topological group structure. In particular, continuity into this group is equivalent to continuity of both the forward and inverse endomorphisms. Conjugation by a linear equivalence V ≃ₗ[K] W acts on both the forward and the inverse endomorphism by the linear map LinearEquiv.conj, so it is continuous between these groups (LinearEquiv.continuous_autCongr).

Over a field, the endomorphism algebra of a finite-dimensional space is itself finite-dimensional, so its module topology is Hausdorff when the field is Hausdorff and locally compact when the field is locally compact. The unit topology inherits both properties, so the linear automorphisms of a finite-dimensional space over a Hausdorff locally compact field form a locally compact group. This is the local-compactness input for the orthogonal point group over ℝ and ℚ_p. Over a field with the indiscrete topology, on the other hand, both the endomorphism algebra and the linear automorphisms are indiscrete, so no proper nonempty subset of them is open or closed.

Over a commutative topological ring the determinant is continuous on endomorphisms, being a polynomial in the matrix entries in any finite basis, and hence LinearEquiv.det is a continuous homomorphism from linear automorphisms to the units of the ring.

@[instance_reducible]

noncomputable instance TauCeti.instTopologicalSpaceModuleEnd {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] : TopologicalSpace (Module.End K V)

The endomorphism algebra carries the canonical module topology.

instance TauCeti.instIsTopologicalRingModuleEnd {K : Type u_1} {V : Type u_2} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [AddCommGroup V] [Module K V] [Module.Finite K (Module.End K V)] : IsTopologicalRing (Module.End K V)

The endomorphism algebra is a topological ring when it is finite over the scalar ring.

@[instance_reducible]

noncomputable instance TauCeti.instTopologicalSpaceLinearEquiv {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] : TopologicalSpace (V ≃ₗ[K] V)

A linear automorphism has the topology induced by its forward and inverse endomorphisms.

instance TauCeti.instIsTopologicalGroupLinearEquiv {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] [ContinuousMul (Module.End K V)] : IsTopologicalGroup (V ≃ₗ[K] V)

Linear automorphisms form a topological group in the forward-and-inverse topology.

noncomputable def TauCeti.generalLinearContinuousMulEquiv {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] : LinearMap.GeneralLinearGroup K V ≃ₜ* V ≃ₗ[K] V

The canonical equivalence between invertible endomorphisms and linear automorphisms is continuous in both directions.

@[simp]

theorem TauCeti.coe_generalLinearContinuousMulEquiv {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] : ↑generalLinearContinuousMulEquiv = LinearMap.GeneralLinearGroup.generalLinearEquiv K V

The topological equivalence has Mathlib's canonical algebraic equivalence as its underlying multiplicative equivalence.

theorem TauCeti.continuous_linearEquiv_iff {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] {X : Type u_3} [TopologicalSpace X] {f : X → V ≃ₗ[K] V} : Continuous f ↔ (Continuous fun (x : X) => ↑(f x)) ∧ Continuous fun (x : X) => ↑(f x)⁻¹

A family of linear automorphisms is continuous exactly when its forward and inverse endomorphisms are both continuous.

theorem TauCeti.continuous_linearEquiv_toLinearMap {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] : Continuous fun (e : V ≃ₗ[K] V) => ↑e

The underlying endomorphism varies continuously with a linear automorphism.

theorem LinearEquiv.continuous_autCongr {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] {W : Type u_3} [AddCommMonoid W] [Module K W] (e : V ≃ₗ[K] W) : Continuous ⇑e.autCongr

Conjugation by a linear equivalence is continuous for the forward-and-inverse topologies on linear automorphisms: on both the forward and the inverse endomorphism it is the linear map LinearEquiv.conj e, which is continuous for the module topologies.

theorem Module.Basis.continuous_iff_apply {K : Type u_1} {V : Type u_2} [CommSemiring K] [TopologicalSpace K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] {X : Type u_3} {ι : Type u_4} [TopologicalSpace X] [Finite ι] (b : Basis ι K V) (f : X → End K V) : Continuous f ↔ ∀ (i : ι), Continuous fun (x : X) => (f x) (b i)

A family of endomorphisms is continuous exactly when its values on the vectors of a finite basis vary continuously.

instance TauCeti.instT2SpaceModuleEnd {K : Type u_3} {V : Type u_4} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [T2Space K] : T2Space (Module.End K V)

The endomorphism algebra of a finite-dimensional space over a Hausdorff field is Hausdorff.

instance TauCeti.instLocallyCompactSpaceModuleEnd {K : Type u_3} {V : Type u_4} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LocallyCompactSpace K] : LocallyCompactSpace (Module.End K V)

The endomorphism algebra of a finite-dimensional space over a locally compact field is locally compact.

instance TauCeti.instT2SpaceLinearEquiv {K : Type u_3} {V : Type u_4} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [T2Space K] : T2Space (V ≃ₗ[K] V)

The linear automorphisms of a finite-dimensional space over a Hausdorff field form a Hausdorff space.

instance TauCeti.instIndiscreteTopologyModuleEnd {K : Type u_3} {V : Type u_4} [CommSemiring K] [TopologicalSpace K] [IndiscreteTopology K] [AddCommMonoid V] [Module K V] : IndiscreteTopology (Module.End K V)

The endomorphism algebra over a scalar ring with the indiscrete topology is indiscrete.

instance TauCeti.instIndiscreteTopologyLinearEquiv {K : Type u_3} {V : Type u_4} [CommSemiring K] [TopologicalSpace K] [IndiscreteTopology K] [AddCommMonoid V] [Module K V] : IndiscreteTopology (V ≃ₗ[K] V)

The linear automorphisms over a scalar ring with the indiscrete topology form an indiscrete space.

instance TauCeti.instLocallyCompactSpaceLinearEquiv {K : Type u_3} {V : Type u_4} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [LocallyCompactSpace K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LocallyCompactSpace (V ≃ₗ[K] V)

The linear automorphisms of a finite-dimensional space over a Hausdorff locally compact field form a locally compact group: the automorphism group is closed in the product of two copies of the locally compact endomorphism algebra, through an automorphism and its inverse.

theorem TauCeti.continuous_linearMap_det {K : Type u_3} {V : Type u_4} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [AddCommGroup V] [Module K V] : Continuous ⇑LinearMap.det

The determinant of an endomorphism is continuous in the module topology: in a finite basis it is a polynomial in the matrix entries, and without a finite basis it is the constant 1.

theorem TauCeti.continuous_linearEquiv_det {K : Type u_3} {V : Type u_4} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [AddCommGroup V] [Module K V] : Continuous ⇑LinearEquiv.det

The determinant of a linear automorphism is continuous as a map to the units of the scalar ring.