How to endow a space with a certain topology?

Stream: general

[Ryan Lahfa]

I have some set $M(A)$ of points and I want to endow it with the weakest topology making some evaluation maps continuous.

Namely, given the set of real-valued multiplicative seminorms $s : A \to \mathbb{R}$, I would like to get the weakest topology making $\{ \lvert f \rvert : M(A) \to \mathbb{R} \mid f \in A \}$

So I have a proper definition of $M(A)$ and I do not know exactly how to derive a specific [topological_space (spectrum A)] instance that I will use to prove specific results on it, e.g. compactness, etc.

[Adam Topaz]

This is the Sup of the induced topologies associated to your evalaution functions.

[Ryan Lahfa]

So something like this https://leanprover-community.github.io/mathlib_docs/topology/order.html#topological_space.induced and then some sup theorem on the set of those (the subtypes of those)?

[Adam Topaz]

Let me sketch some code. 1 sec.

[Adam Topaz]

Here's a version that's probably more general than what you actually want:

import topology.order

variables {α β ι : Type*}

example (fs : ι → α → β) [I : topological_space β] : topological_space α :=
⨆ (i : ι), topological_space.induced (fs i) I

[Patrick Massot]

Ryan, you should have a look at how the product topology is defined.

[Patrick Massot]

(and how its basic properties are proved)

[Ryan Lahfa]

Patrick Massot said:

Ryan, you should have a look at how the product topology is defined.

Alright, will do so!

[Adam Topaz]

Oh, sorry I should have used Inf not Sup in the code above (I forgot the ordering on topologies is backwards :smile: ) (fixed the code)