Open embeddings and over categories of open subsets

Let f : X ⟶ Y be an open embedding of topological spaces, with open image U = range f. Mathlib's TopologicalSpace.Opens.overEquivalence identifies Over U with the open subsets of the subspace U. This file gives the corresponding equivalence Over U ≌ Opens X for the open embedding itself: an open subset W ⊆ U goes to f⁻¹(W), and an open subset V ⊆ X goes back to f(V). The equivalence is a dense subsite in both directions, so it induces an equivalence of sheaf categories under which a sheaf F on Y, restricted to U, becomes the sheaf V ↦ F(f(V)) on X.

Working with f rather than with the subspace U keeps that sheaf literally equal to the pushforward along f(-), which is how Mathlib defines the restriction of a sheaf of modules along an open immersion of schemes.

The construction of the dense-subsite instances is adapted from Mathlib.Topology.Sheaves.Over, by Joël Riou.

Main declarations

• Topology.IsOpenEmbedding.overEquivalence: the equivalence Over (range f) ≌ Opens X.
• The instances saying that its functor and inverse are dense subsites for the Grothendieck topologies of open covers.

def Topology.IsOpenEmbedding.overEquivalence {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ } ≌ TopologicalSpace.Opens ↑X

An open embedding f : X ⟶ Y identifies the open subsets of Y contained in the range of f with the open subsets of X, by taking preimages and images under f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Topology.IsOpenEmbedding.overEquivalence_functor_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (W : CategoryTheory.Over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) : hf.overEquivalence.functor.obj W = (TopologicalSpace.Opens.map f).obj W.left

def Topology.IsOpenEmbedding.overEquivalenceInverseCompForgetIso {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : hf.overEquivalence.inverse.comp (CategoryTheory.Over.forget { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) ≅ hf.functor

The inverse of overEquivalence, followed by the forgetful functor from the over category, is the image functor on open subsets.

Equations

• One or more equations did not get rendered due to their size.

instance Topology.IsOpenEmbedding.isDenseSubsite_overEquivalence_functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology ↑Y).over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) (Opens.grothendieckTopology ↑X) hf.overEquivalence.functor

instance Topology.IsOpenEmbedding.isDenseSubsite_overEquivalence_symm_inverse {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology ↑Y).over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) (Opens.grothendieckTopology ↑X) hf.overEquivalence.symm.inverse

instance Topology.IsOpenEmbedding.isDenseSubsite_overEquivalence_inverse {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor.IsDenseSubsite (Opens.grothendieckTopology ↑X) ((Opens.grothendieckTopology ↑Y).over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) hf.overEquivalence.inverse

instance Topology.IsOpenEmbedding.isContinuous_functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : hf.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)

def Topology.IsOpenEmbedding.overPullbackSheafCongrIso {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] : ((Opens.grothendieckTopology ↑Y).overPullback A { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }).comp (CategoryTheory.Equivalence.sheafCongr ((Opens.grothendieckTopology ↑Y).over { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f), is_open' := ⋯ }) (Opens.grothendieckTopology ↑X) hf.overEquivalence A).functor ≅ hf.functor.sheafPushforwardContinuous A (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)

Restriction to the range of an open embedding, followed by transport along overEquivalence, is naturally isomorphic to pushforward along the image functor on opens.

Equations

• One or more equations did not get rendered due to their size.