Separation, countability and local compactness of the point topology

Let A be a k-algebra and R a topological k-algebra. The point topology on the R-points A →ₐ[k] R is induced from the product topology on A → R, and for A of finite type also from R ^ n by evaluation at finitely many generators. Point-set properties of R therefore pass to the points:

• if R is Hausdorff, so are the points;
• if R is totally disconnected, so are the points;
• if R is second countable and A is of finite type, so are the points;
• if R is locally compact and T1 and A is of finite type, so are the points (this is TauCeti.PointTopology.locallyCompactSpace_of_finiteType, made an instance here).

All four are instances, both on A →ₐ[k] R and on the convolution type WithConv (A →ₐ[k] R) carrying the group of points of an affine group scheme. Over a nonarchimedean local field E, which is Hausdorff, totally disconnected, locally compact and second countable (TauCeti/NumberTheory/LocalField/Topology.lean), they make the group G(E) of points of an affine group G = Spec H over E a Hausdorff and totally disconnected topological group, locally compact and second countable when H is of finite type.

Main declarations

• TauCeti.PointTopology.instT2Space, TauCeti.PointTopology.instT2SpaceWithConv.
• TauCeti.PointTopology.instTotallyDisconnectedSpace, TauCeti.PointTopology.instTotallyDisconnectedSpaceWithConv.
• TauCeti.PointTopology.instSecondCountableTopology, TauCeti.PointTopology.instSecondCountableTopologyWithConv.
• TauCeti.PointTopology.instLocallyCompactSpaceWithConv, with TauCeti.PointTopology.locallyCompactSpace_of_finiteType made an instance.

References

• B. Conrad, Weil and Grothendieck approaches to adelic points, Enseign. Math. (2) 58 (2012), Prop. 2.1, p. 2.

instance TauCeti.PointTopology.instT2Space {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] [T2Space R] : T2Space (A →ₐ[k] R)

Points with values in a Hausdorff ring form a Hausdorff space.

instance TauCeti.PointTopology.instT2SpaceWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] [T2Space R] : T2Space (WithConv (A →ₐ[k] R))

The convolution type WithConv (A →ₐ[k] R) of points with values in a Hausdorff ring is a Hausdorff space.

instance TauCeti.PointTopology.instTotallyDisconnectedSpace {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] [TotallyDisconnectedSpace R] : TotallyDisconnectedSpace (A →ₐ[k] R)

Points with values in a totally disconnected ring form a totally disconnected space.

instance TauCeti.PointTopology.instTotallyDisconnectedSpaceWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Semiring R] [Algebra k R] [TopologicalSpace R] [TotallyDisconnectedSpace R] : TotallyDisconnectedSpace (WithConv (A →ₐ[k] R))

The convolution type WithConv (A →ₐ[k] R) of points with values in a totally disconnected ring is a totally disconnected space.

instance TauCeti.PointTopology.instSecondCountableTopology {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [CommSemiring A] [Algebra k A] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [SecondCountableTopology R] [Algebra.FiniteType k A] : SecondCountableTopology (A →ₐ[k] R)

Points of a finite type algebra with values in a second countable ring form a second countable space, since finitely many generators embed them in a finite power of the ring.

instance TauCeti.PointTopology.instSecondCountableTopologyWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommSemiring k] [CommSemiring A] [Algebra k A] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [SecondCountableTopology R] [Algebra.FiniteType k A] : SecondCountableTopology (WithConv (A →ₐ[k] R))

The convolution type WithConv (A →ₐ[k] R) of points of a finite type algebra with values in a second countable ring is a second countable space.

instance TauCeti.PointTopology.instLocallyCompactSpaceWithConv {k : Type u_1} {A : Type u_2} {R : Type u_3} [CommRing k] [CommRing A] [Algebra k A] [CommRing R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] [LocallyCompactSpace R] [Algebra.FiniteType k A] : LocallyCompactSpace (WithConv (A →ₐ[k] R))

The convolution type WithConv (A →ₐ[k] R) of points of a finite type algebra with values in a locally compact T1 ring is a locally compact space.