Restriction of open set to subtype topology

Stream: maths

[Calvin Lee]

Hi! Unsure about whether to post this in #maths or #Is there code for X?.

I'm currently working on formalizing https://stacks.math.columbia.edu/tag/00AK, which (though _relatively_ easy in set theory) is quite difficult to get right in type theory, due to the multitude of restrictions of functions and sheaves on a topological space.
In particular, for some (pre)sheaf $\mathcal{F}:\mathsf{C}^{\mathrm{op}}\to X$ we must consider the restriction to an open set $\mathcal{F}|_U$, in Lean this can be given the type presheaf C (Top.of U), equivalently (opens (Top.of U))ᵒᵖ ⥤ C, i.e. a functor from the category of open sets on $U$, using the subtype topology.

However, this becomes messy when working with subsets.
Let $\iota : U\to X$ be the inclusion map between two open sets, and $V\subseteq U$ be open. How can I witness that $\iota^{-1}(V)$ is open in $U$, and $\mathcal{F}|_U(\iota^{-1}(V))=\mathcal{F}(V)$? Is there any easy (more set theoretic) way to talk about these things?

for reference my definition of a restriction of presheaves is here and current work is here.

[Junyan Xu]

I think 6.33.1/2 has been done in https://leanprover-community.github.io/mathlib_docs/algebraic_geometry/presheafed_space/gluing.html by Andrew Yang. Maybe you can look into the code to see how it's done?
You could first look into docs#Top.glue_data, which underlies
docs#algebraic_geometry.PresheafedSpace.glue_data
docs#algebraic_geometry.SheafedSpace.glue_data
docs#algebraic_geometry.LocallyRingedSpace.glue_data and
docs#algebraic_geometry.Scheme.glue_data.

[Calvin Lee]

I'll definitely read into this
I'm working specifically on the corollary at the bottom of 6.33.1, which proves the sheaf condition for the presheaf of internal homs (which I'm not sure if is proved in any of the links shared above)

[Junyan Xu]

(deleted)

[Junyan Xu]

It took me a while to find that glueing of morphisms is at docs#algebraic_geometry.Scheme.open_cover.glue_morphisms, but there apparently isn't a PresheafedSpace version. I think no one has done internal homs, but maybe @Andrew Yang or @Jujian Zhang has it somewhere.

[Calvin Lee]

This is branched from @Jujian Zhang 's work already, but he didn't work on the sheaf condition which is why I'm developing on it as a "first significant addition"

[Calvin Lee]

This branch is quite old though, and I've already had to rework it a bit to include some editions from "modern mathlib"
there could certainly be better structures to build off than what I'm currently using

[Andrew Yang]

I'd say that it would be relatively easy to copy what was done in docs#algebraic_geometry.Scheme.open_cover.glue_morphisms for presheafed spaces: To show that $\mathcal{F}$ is isomorphic to the glue (docs#algebraic_geometry.PresheafedSpace.glue_data) of $\{\mathcal{F}|_{U_i}\}_i$, and then use the limit library to do the gluing.

[Junyan Xu]

Calvin Lee said:

Let $\iota : U\to X$ be the inclusion map between two open sets, and $V\subseteq U$ be open.

You mean the inclusion of an open set into the whole space, right?

How can I witness that $\iota^{-1}(V)$ is open in $U$, and $\mathcal{F}|_U(\iota^{-1}(V))=\mathcal{F}(V)$? Is there any easy (more set theoretic) way to talk about these things?

You can get $\iota^{-1}(V)$ as an open in $U$ using docs#topological_space.opens.map applied to $\iota$. We have F|U(ι⁻¹(V)) = F(ι(ι⁻¹(V))) = F(V ⊓ U) by docs#topological_space.opens.functor_map_eq_inf. The latter equality isn't a defeq, so you probably need quiver.hom.op $ hom_of_le or eq_to_hom.

Jujian did some Cech cohomology last year so he surely also knows how to deal with open covers :)

[Calvin Lee]

aha! docs#topological_space.opens.functor_map_eq_inf is exactly what I was looking for, but I read over it. I am already using docs#topological_space.opens.map but I was looking at docs#is_open_map.adjunction instead which wouldn't work.
also yes, you described the inclusion correctly. that was from an earlier version of my message which I changed.