feat(algebraic_geometry/open_immersion): API for Scheme.restrict_functor. (#17184)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/algebraic_geometry/open_immersion.lean

@@ -1703,9 +1703,13 @@ def hom.opens_range {X Y : Scheme} (f : X ⟶ Y) [H : is_open_immersion f] : ope
 
 end Scheme
 
+section
+
+variable (X : Scheme)
+
 /-- The functor taking open subsets of `X` to open subschemes of `X`. -/
 @[simps obj_left obj_hom map_left]
-def Scheme.restrict_functor (X : Scheme) : opens X.carrier ⥤ over X :=
+def Scheme.restrict_functor : opens X.carrier ⥤ over X :=
 { obj := λ U, over.mk (X.of_restrict U.open_embedding),
   map := λ U V i, over.hom_mk (is_open_immersion.lift (X.of_restrict _) (X.of_restrict _)
     (by { change set.range coe ⊆ set.range coe, simp_rw [subtype.range_coe], exact i.le }))
@@ -1723,6 +1727,65 @@ def Scheme.restrict_functor (X : Scheme) : opens X.carrier ⥤ over X :=
     iterate 3 { rw [is_open_immersion.lift_fac] }
   end }
 
+@[reassoc]
+lemma Scheme.restrict_functor_map_of_restrict {U V : opens X.carrier} (i : U ⟶ V) :
+  (X.restrict_functor.map i).1 ≫ X.of_restrict _ = X.of_restrict _ :=
+is_open_immersion.lift_fac _ _ _
+
+lemma Scheme.restrict_functor_map_base {U V : opens X.carrier} (i : U ⟶ V) :
+  (X.restrict_functor.map i).1.1.base = (opens.to_Top _).map i :=
+begin
+  ext a,
+  exact (congr_arg (λ f : X.restrict U.open_embedding ⟶ X, by exact f.1.base a)
+    (X.restrict_functor_map_of_restrict i) : _),
+end
+
+lemma Scheme.restrict_functor_map_app_aux {U V : opens X.carrier} (i : U ⟶ V) (W : opens V) :
+  U.open_embedding.is_open_map.functor.obj
+    ((opens.map (X.restrict_functor.map i).1.val.base).obj W) ≤
+    V.open_embedding.is_open_map.functor.obj W :=
+begin
+  simp only [set.image_congr, subtype.mk_le_mk, is_open_map.functor, set.image_subset_iff,
+    Scheme.restrict_functor_map_base, opens.map, subtype.coe_mk, opens.inclusion_apply,
+    set.le_eq_subset],
+  rintros _ h,
+  exact ⟨_, h, rfl⟩,
+end
+
+lemma Scheme.restrict_functor_map_app {U V : opens X.carrier} (i : U ⟶ V) (W : opens V) :
+  (X.restrict_functor.map i).1.1.c.app (op W) = X.presheaf.map
+    (hom_of_le $ X.restrict_functor_map_app_aux i W).op :=
+begin
+  have e₁ := Scheme.congr_app (X.restrict_functor_map_of_restrict i)
+    (op $ V.open_embedding.is_open_map.functor.obj W),
+  rw Scheme.comp_val_c_app at e₁,
+  have e₂ := (X.restrict_functor.map i).1.val.c.naturality (eq_to_hom W.map_functor_eq).op,
+  rw ← is_iso.eq_inv_comp at e₂,
+  dsimp at e₁ e₂ ⊢,
+  rw [e₂, W.adjunction_counit_map_functor, ← is_iso.eq_inv_comp, is_iso.inv_comp_eq,
+    ← is_iso.eq_comp_inv] at e₁,
+  simp_rw [eq_to_hom_map (opens.map _), eq_to_hom_map (is_open_map.functor _), ← functor.map_inv,
+    ← functor.map_comp] at e₁,
+  rw e₁,
+  congr' 1,
+end
+
+/-- The functor that restricts to open subschemes and then takes global section is
+isomorphic to the structure sheaf. -/
+@[simps]
+def Scheme.restrict_functor_Γ :
+  X.restrict_functor.op ⋙ (over.forget X).op ⋙ Scheme.Γ ≅ X.presheaf :=
+nat_iso.of_components
+  (λ U, X.presheaf.map_iso ((eq_to_iso (unop U).open_embedding_obj_top).symm.op : _))
+begin
+  intros U V i,
+  dsimp [-subtype.val_eq_coe, -Scheme.restrict_functor_map_left],
+  rw [X.restrict_functor_map_app, ← functor.map_comp, ← functor.map_comp],
+  congr' 1
+end
+
+end
+
 /-- The restriction of an isomorphism onto an open set. -/
 noncomputable
 abbreviation Scheme.restrict_map_iso {X Y : Scheme} (f : X ⟶ Y) [is_iso f] (U : opens Y.carrier) :

src/topology/category/Top/opens.lean

@@ -131,6 +131,10 @@ def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
 { obj := λ U, ⟨ f ⁻¹' U.val, U.property.preimage f.continuous ⟩,
   map := λ U V i, ⟨ ⟨ λ x h, i.le h ⟩ ⟩ }.
 
+lemma map_coe (f : X ⟶ Y) (U : opens Y) :
+  ↑((map f).obj U) = f ⁻¹' U :=
+rfl
+
 @[simp] lemma map_obj (f : X ⟶ Y) (U) (p) :
   (map f).obj ⟨U, p⟩ = ⟨f ⁻¹' U, p.preimage f.continuous⟩ := rfl
 
@@ -302,4 +306,21 @@ begin
   { rintros ⟨⟨x, -, rfl⟩, hx⟩, exact ⟨x, hx, rfl⟩ }
 end
 
+@[simp] lemma functor_map_eq_inf {X : Top} (U V : opens X) :
+  U.open_embedding.is_open_map.functor.obj ((opens.map U.inclusion).obj V) = V ⊓ U :=
+by { ext1, refine set.image_preimage_eq_inter_range.trans _, simpa }
+
+lemma map_functor_eq' {X U : Top} (f : U ⟶ X) (hf : _root_.open_embedding f) (V) :
+  ((opens.map f).obj $ hf.is_open_map.functor.obj V) = V :=
+opens.ext $ set.preimage_image_eq _ hf.inj
+
+@[simp] lemma map_functor_eq {X : Top} {U : opens X} (V : opens U) :
+  ((opens.map U.inclusion).obj $ U.open_embedding.is_open_map.functor.obj V) = V :=
+topological_space.opens.map_functor_eq' _ U.open_embedding V
+
+@[simp] lemma adjunction_counit_map_functor {X : Top} {U : opens X} (V : opens U) :
+  U.open_embedding.is_open_map.adjunction.counit.app (U.open_embedding.is_open_map.functor.obj V)
+    = eq_to_hom (by { conv_rhs { rw ← V.map_functor_eq }, refl }) :=
+by ext
+
 end topological_space.opens