Topology on Hom (Topological Ring valued points on a scheme)

Stream: mathlib4

[Ruiqi Chen]

I've got some concerns about the definition showed. Do we need to deal with the cases where $\hom (R,S)$ is taken in the category of algebra over a ring , e.g. $\mathbb{C}$-value points on an affine $\mathbb{C}$-scheme instead of $\mathbb{Z}$-scheme (i.e. a general scheme) as in the code.

Andrew Yang said:

Ruiqi Chen said:

https://doi.org/10.4171/lem/58-1-3

This thing is on my todo list too and I already have some existing code on it. Maybe we can collaborate? So we have the topology on $\mathrm{Hom}(R, S)$ for a topogical ring here #21283, and we do have the global version of it as well. Currently we are stuck on showing that every scheme over $\mathbb{A}_F$ has a model over $\mathcal{O}_{F, S}$ for some $S$, and the right (mathlib) thing to do here is to do EGA 4.8 (or equivalently stacks#01ZM)

[Kevin Buzzard]

That stuff in EGA 4.8 to 4.11 is really important for reducing to the noetherian case, it would be very cool to have it in mathlib.

[Andrew Yang]

Since $\mathrm{Hom}_{\mathbf{Sch}/S}(X, Y) \subseteq \mathrm{Hom}_{\mathbf{Sch}}(X, Y)$, we can just restrict the topology later when necessary.

[Ruiqi Chen]

Fine, I think i should deal with $R$-valued points on an $R$-scheme. Cuz we want to prove a smooth scheme admits $R$-valued points as a manifold. Maybe I should develop more about Under R. Another question is whether base-change to $Y$ and consider $\hom_Y (X,Y)$ for $Y$-scheme or in general embed all $\hom_S (X,Y)$.

[Christian Merten]

What do you mean by "a smooth scheme admits R-valued points as a manifold"? Can you write a formal statement (in Lean)?

[Yury G. Kudryashov]

Could you please mention in the title which Homs this topic is about? E.g., I can't guess without following some links if there is a potential overlap with some point-set topology instance here.

[Ruiqi Chen]

Christian Merten said:

What do you mean by "a smooth scheme admits R-valued points as a manifold"? Can you write a formal statement (in Lean)?

Sorry, I mistakenly typed $\mathbb{R}$ for $R$. I'm not familiar with manifolds, below is an example including sorries.

universe u
def good_over_R : CategoryTheory.ObjectProperty <| CategoryTheory.Over (AlgebraicGeometry.Spec <| CommRingCat.of.{u} <| Shrink.{u} ℝ) :=
  fun X => ∃ d : ℕ, AlgebraicGeometry.IsSmoothOfRelativeDimension d X.hom ∧ AlgebraicGeometry.IsSeparated X.hom

def category_of_mnfd : Type u := sorry
instance : CategoryTheory.Category category_of_mnfd := sorry

open CategoryTheory in
def to_mnfd : CategoryTheory.FullSubcategory good_over_R.{u} ⥤ category_of_mnfd.{u} := sorry

[Andrew Yang]

I have to warn you that formalizing this is mostly an differential geometric problem. We have basically all the ingredients on the algebraic side but it is currently not possible yet to make a smooth level set of an affine space into a manifold yet and some serious work will need to be done before this happens.

[Christian Merten]

@Michael Rothgang is actively working on the DG side of this.

[Christian Merten]

Also, I believe the topology on Hom(X, Y) is not really needed for what you describe, because you will automatically get a topology from the regular value theorem.
Of course in a second step, you might want to show that the topologies coincide.

[Michael Rothgang]

Christian Merten said:

Michael Rothgang is actively working on the DG side of this.

Yes, and more helping hands are always welcome; there's a lot to do. One self-contained sorry you could help with is in #23186 (which is mostly about functional analysis).