## Stream: general

### Topic: How to endow a space with a certain topology?

#### Ryan Lahfa (Feb 05 2021 at 14:37):

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 (Feb 05 2021 at 14:49):

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

#### Ryan Lahfa (Feb 05 2021 at 14:52):

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 (Feb 05 2021 at 14:55):

Let me sketch some code. 1 sec.

#### Adam Topaz (Feb 05 2021 at 15:03):

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 (Feb 05 2021 at 15:05):

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

#### Patrick Massot (Feb 05 2021 at 15:06):

(and how its basic properties are proved)

#### Ryan Lahfa (Feb 05 2021 at 15:09):

Patrick Massot said:

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

Alright, will do so!

#### Adam Topaz (Feb 05 2021 at 15:12):

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)

Last updated: Dec 20 2023 at 11:08 UTC