Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit b7ed03f

Browse files
erdOneerdOne
committed
feat(algebraic_geometry): Open immersions of presheafed spaces (#10437)
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
1 parent 2f44ac8 commit b7ed03f

File tree

3 files changed

+326
-0
lines changed

3 files changed

+326
-0
lines changed

‎src/algebraic_geometry/open_immersion.lean

Lines changed: 279 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,279 @@
1+
/-
2+
Copyright (c) 2021 Andrew Yang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Andrew Yang
5+
-/
6+
import algebraic_geometry.presheafed_space.has_colimits
7+
import category_theory.limits.shapes.binary_products
8+
import category_theory.limits.preserves.shapes.pullbacks
9+
import topology.sheaves.functors
10+
import algebraic_geometry.Scheme
11+
12+
/-!
13+
# Open immersions of structured spaces
14+
15+
We say that a morphism of presheafed spaces `f : X ⟶ Y` is an open immersions if
16+
the underlying map of spaces is an open embedding `f : X ⟶ U ⊆ Y`,
17+
and the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
18+
19+
Abbreviations are also provided for `SheafedSpace`, `LocallyRingedSpace` and `Scheme`.
20+
21+
## Main definitions
22+
23+
* `algebraic_geometry.PresheafedSpace.is_open_immersion`: the `Prop`-valued typeclass asserting
24+
that a PresheafedSpace hom `f` is an open_immersion.
25+
* `algebraic_geometry.is_open_immersion`: the `Prop`-valued typeclass asserting
26+
that a Scheme morphism `f` is an open_immersion.
27+
* `algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict`: The source of an
28+
open immersion is isomorphic to the restriction of the target onto the image.
29+
30+
## Main results
31+
32+
* `algebraic_geometry.PresheafedSpace.is_open_immersion.comp`: The composition of two open
33+
immersions is an open immersion.
34+
* `algebraic_geometry.PresheafedSpace.is_open_immersion.of_iso`: An iso is an open immersion.
35+
* `algebraic_geometry.PresheafedSpace.is_open_immersion.to_iso`:
36+
A surjective open immersion is an isomorphism.
37+
* `algebraic_geometry.PresheafedSpace.is_open_immersion.stalk_iso`: An open immersion induces
38+
an isomorphism on stalks.
39+
40+
-/
41+
42+
open topological_space category_theory opposite
43+
open category_theory.limits
44+
namespace algebraic_geometry
45+
46+
universes v u
47+
48+
variables {C : Type u} [category.{v} C]
49+
50+
/--
51+
An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying
52+
spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
53+
-/
54+
class PresheafedSpace.is_open_immersion {X Y : PresheafedSpace C} (f : X ⟶ Y) : Prop :=
55+
(base_open : open_embedding f.base)
56+
(c_iso : ∀ U : opens X, is_iso (f.c.app (op (base_open.is_open_map.functor.obj U))))
57+
58+
/--
59+
A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism
60+
of PresheafedSpaces
61+
-/
62+
abbreviation SheafedSpace.is_open_immersion
63+
[has_products C] {X Y : SheafedSpace C} (f : X ⟶ Y) : Prop :=
64+
PresheafedSpace.is_open_immersion f
65+
66+
/--
67+
A morphism of LocallyRingedSpaces is an open immersion if it is an open immersion as a morphism
68+
of SheafedSpaces
69+
-/
70+
abbreviation LocallyRingedSpace.is_open_immersion {X Y : LocallyRingedSpace} (f : X ⟶ Y) : Prop :=
71+
SheafedSpace.is_open_immersion f.1
72+
73+
/--
74+
A morphism of Schemes is an open immersion if it is an open immersion as a morphism
75+
of LocallyRingedSpaces
76+
-/
77+
abbreviation is_open_immersion {X Y : Scheme} (f : X ⟶ Y) : Prop :=
78+
LocallyRingedSpace.is_open_immersion f
79+
80+
namespace PresheafedSpace.is_open_immersion
81+
82+
open PresheafedSpace
83+
84+
local notation `is_open_immersion` := PresheafedSpace.is_open_immersion
85+
86+
attribute [instance] is_open_immersion.c_iso
87+
88+
section
89+
90+
variables {X Y : PresheafedSpace C} {f : X ⟶ Y} (H : is_open_immersion f)
91+
92+
/-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
93+
abbreviation open_functor := H.base_open.is_open_map.functor
94+
95+
/-
96+
We want to keep `eq_to_hom`s in the form of `F.map (eq_to_hom _)` so that the lemmas about
97+
naturality can be applied.
98+
-/
99+
local attribute [-simp] eq_to_hom_map eq_to_iso_map
100+
101+
/-- An open immersion `f : X ⟶ Y` induces an isomorphism `X ≅ Y|_{f(X)}`. -/
102+
@[simps] noncomputable
103+
def iso_restrict : X ≅ Y.restrict H.base_open :=
104+
PresheafedSpace.iso_of_components (iso.refl _)
105+
begin
106+
symmetry,
107+
fapply nat_iso.of_components,
108+
intro U,
109+
refine as_iso (f.c.app (op (H.open_functor.obj (unop U)))) ≪≫ X.presheaf.map_iso (eq_to_iso _),
110+
{ induction U using opposite.rec,
111+
cases U,
112+
dsimp only [is_open_map.functor, functor.op, opens.map],
113+
congr' 2,
114+
erw set.preimage_image_eq _ H.base_open.inj,
115+
refl },
116+
{ intros U V i,
117+
simp only [category_theory.eq_to_iso.hom, Top.presheaf.pushforward_obj_map, category.assoc,
118+
functor.op_map, iso.trans_hom, as_iso_hom, functor.map_iso_hom, ←X.presheaf.map_comp],
119+
erw [f.c.naturality_assoc, ←X.presheaf.map_comp],
120+
congr }
121+
end
122+
123+
@[simp] lemma iso_restrict_hom_of_restrict : H.iso_restrict.hom ≫ Y.of_restrict _ = f :=
124+
begin
125+
ext,
126+
{ simp only [comp_c_app, iso_restrict_hom_c_app, nat_trans.comp_app,
127+
eq_to_hom_refl, of_restrict_c_app, category.assoc, whisker_right_id'],
128+
erw [category.comp_id, f.c.naturality_assoc, ←X.presheaf.map_comp],
129+
transitivity f.c.app x ≫ X.presheaf.map (𝟙 _),
130+
{ congr },
131+
{ erw [X.presheaf.map_id, category.comp_id] } },
132+
{ simp }
133+
end
134+
135+
@[simp] lemma iso_restrict_inv_of_restrict : H.iso_restrict.inv ≫ f = Y.of_restrict _ :=
136+
by { rw iso.inv_comp_eq, simp }
137+
138+
instance mono [H : is_open_immersion f] : mono f :=
139+
by { rw ← H.iso_restrict_hom_of_restrict, apply mono_comp }
140+
141+
/-- The composition of two open immersions is an open immersion. -/
142+
instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : is_open_immersion f] (g : Y ⟶ Z)
143+
[hg : is_open_immersion g] :
144+
is_open_immersion (f ≫ g) :=
145+
{ base_open := hg.base_open.comp hf.base_open,
146+
c_iso := λ U,
147+
begin
148+
generalize_proofs h,
149+
dsimp only [algebraic_geometry.PresheafedSpace.comp_c_app, unop_op, functor.op, comp_base,
150+
Top.presheaf.pushforward_obj_obj, opens.map_comp_obj],
151+
apply_with is_iso.comp_is_iso { instances := ff },
152+
swap,
153+
{ have : (opens.map g.base).obj (h.functor.obj U) = hf.open_functor.obj U,
154+
{ dsimp only [opens.map, is_open_map.functor, PresheafedSpace.comp_base],
155+
congr' 1,
156+
rw [coe_comp, ←set.image_image, set.preimage_image_eq _ hg.base_open.inj] },
157+
rw this,
158+
apply_instance },
159+
{ have : h.functor.obj U = hg.open_functor.obj (hf.open_functor.obj U),
160+
{ dsimp only [is_open_map.functor],
161+
congr' 1,
162+
rw [comp_base, coe_comp, ←set.image_image],
163+
congr },
164+
rw this,
165+
apply_instance }
166+
end }
167+
168+
/-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`. -/
169+
noncomputable
170+
def inv_app (U : opens X) : X.presheaf.obj (op U) ⟶ Y.presheaf.obj (op (H.open_functor.obj U)) :=
171+
X.presheaf.map (eq_to_hom (by simp [opens.map, set.preimage_image_eq _ H.base_open.inj])) ≫
172+
inv (f.c.app (op (H.open_functor.obj U)))
173+
174+
@[simp, reassoc] lemma inv_naturality {U V : (opens X)ᵒᵖ} (i : U ⟶ V) :
175+
X.presheaf.map i ≫ H.inv_app (unop V) = H.inv_app (unop U) ≫
176+
Y.presheaf.map (H.open_functor.op.map i) :=
177+
begin
178+
simp only [inv_app, ←category.assoc],
179+
rw [is_iso.comp_inv_eq],
180+
simp only [category.assoc, f.c.naturality, is_iso.inv_hom_id_assoc, ← X.presheaf.map_comp],
181+
erw ← X.presheaf.map_comp,
182+
congr
183+
end
184+
185+
instance (U : opens X) : is_iso (H.inv_app U) := by { delta inv_app, apply_instance }
186+
187+
lemma inv_inv_app (U : opens X) :
188+
inv (H.inv_app U) = f.c.app (op (H.open_functor.obj U)) ≫
189+
X.presheaf.map (eq_to_hom (by simp [opens.map, set.preimage_image_eq _ H.base_open.inj])) :=
190+
begin
191+
rw ← cancel_epi (H.inv_app U),
192+
rw is_iso.hom_inv_id,
193+
delta inv_app,
194+
simp [← functor.map_comp]
195+
end
196+
197+
@[simp, reassoc] lemma inv_app_app (U : opens X) :
198+
H.inv_app U ≫ f.c.app (op (H.open_functor.obj U)) =
199+
X.presheaf.map (eq_to_hom (by simp [opens.map, set.preimage_image_eq _ H.base_open.inj])) :=
200+
by rw [inv_app, category.assoc, is_iso.inv_hom_id, category.comp_id]
201+
202+
@[simp, reassoc] lemma app_inv_app (U : opens Y) :
203+
f.c.app (op U) ≫ H.inv_app ((opens.map f.base).obj U) =
204+
Y.presheaf.map ((hom_of_le (by exact set.image_preimage_subset f.base U)).op :
205+
op U ⟶ op (H.open_functor.obj ((opens.map f.base).obj U))) :=
206+
by { erw ← category.assoc, rw [is_iso.comp_inv_eq, f.c.naturality], congr }
207+
208+
/-- A variant of `app_inv_app` that gives an `eq_to_hom` instead of `hom_of_le`. -/
209+
@[reassoc] lemma app_inv_app' (U : opens Y) (hU : (U : set Y) ⊆ set.range f.base) :
210+
f.c.app (op U) ≫ H.inv_app ((opens.map f.base).obj U) =
211+
Y.presheaf.map (eq_to_hom (by
212+
{ apply has_le.le.antisymm,
213+
{ exact set.image_preimage_subset f.base U.1 },
214+
{ change U ⊆ _,
215+
refine has_le.le.trans_eq _ (@set.image_preimage_eq_inter_range _ _ f.base U.1).symm,
216+
exact set.subset_inter_iff.mpr ⟨λ _ h, h, hU⟩ } })).op :=
217+
by { erw ← category.assoc, rw [is_iso.comp_inv_eq, f.c.naturality], congr }
218+
219+
/-- An isomorphism is an open immersion. -/
220+
instance of_iso {X Y : PresheafedSpace C} (H : X ≅ Y) : is_open_immersion H.hom :=
221+
{ base_open := (Top.homeo_of_iso ((forget C).map_iso H)).open_embedding,
222+
c_iso := λ _, infer_instance }
223+
224+
@[priority 100]
225+
instance of_is_iso {X Y : PresheafedSpace C} (f : X ⟶ Y) [is_iso f] : is_open_immersion f :=
226+
algebraic_geometry.PresheafedSpace.is_open_immersion.of_iso (as_iso f)
227+
228+
instance of_restrict {X : Top} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier}
229+
(hf : open_embedding f) : is_open_immersion (Y.of_restrict hf) :=
230+
{ base_open := hf,
231+
c_iso := λ U,
232+
begin
233+
dsimp,
234+
have : (opens.map f).obj (hf.is_open_map.functor.obj U) = U,
235+
{ cases U,
236+
dsimp only [opens.map, is_open_map.functor],
237+
congr' 1,
238+
rw set.preimage_image_eq _ hf.inj,
239+
refl },
240+
convert (show is_iso (Y.presheaf.map (𝟙 _)), from infer_instance),
241+
{ apply subsingleton.helim,
242+
rw this },
243+
{ rw Y.presheaf.map_id,
244+
apply_instance }
245+
end }
246+
247+
/-- An open immersion is an iso if the underlying continuous map is epi. -/
248+
lemma to_iso (f : X ⟶ Y) [h : is_open_immersion f] [h' : epi f.base] : is_iso f :=
249+
begin
250+
apply_with is_iso_of_components { instances := ff },
251+
{ let : X ≃ₜ Y := (homeomorph.of_embedding _ h.base_open.to_embedding).trans
252+
{ to_fun := subtype.val, inv_fun := λ x, ⟨x,
253+
by { rw set.range_iff_surjective.mpr ((Top.epi_iff_surjective _).mp h'), trivial }⟩,
254+
left_inv := λ ⟨_,_⟩, rfl, right_inv := λ _, rfl },
255+
convert is_iso.of_iso (Top.iso_of_homeo this),
256+
{ ext, refl } },
257+
{ apply_with nat_iso.is_iso_of_is_iso_app { instances := ff },
258+
intro U,
259+
have : U = op (h.open_functor.obj ((opens.map f.base).obj (unop U))),
260+
{ induction U using opposite.rec,
261+
cases U,
262+
dsimp only [functor.op, opens.map],
263+
congr,
264+
exact (set.image_preimage_eq _ ((Top.epi_iff_surjective _).mp h')).symm },
265+
convert @@is_open_immersion.c_iso _ h ((opens.map f.base).obj (unop U)) }
266+
end
267+
268+
instance stalk_iso [has_colimits C] [H : is_open_immersion f] (x : X) : is_iso (stalk_map f x) :=
269+
begin
270+
rw ← H.iso_restrict_hom_of_restrict,
271+
rw PresheafedSpace.stalk_map.comp,
272+
apply_instance
273+
end
274+
275+
end
276+
277+
end PresheafedSpace.is_open_immersion
278+
279+
end algebraic_geometry

‎src/algebraic_geometry/stalks.lean

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,27 @@ lemma restrict_stalk_iso_inv_eq_germ {U : Top} (X : PresheafedSpace C) {f : U
8383
(restrict_stalk_iso X h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩ :=
8484
by rw [← restrict_stalk_iso_hom_eq_germ, category.assoc, iso.hom_inv_id, category.comp_id]
8585

86+
lemma restrict_stalk_iso_inv_eq_of_restrict {U : Top} (X : PresheafedSpace C)
87+
{f : U ⟶ (X : Top.{v})} (h : open_embedding f) (x : U) :
88+
(X.restrict_stalk_iso h x).inv = stalk_map (X.of_restrict h) x :=
89+
begin
90+
ext V,
91+
induction V using opposite.rec,
92+
let i : (h.is_open_map.functor_nhds x).obj ((open_nhds.map f x).obj V) ⟶ V :=
93+
hom_of_le (set.image_preimage_subset f _),
94+
erw [iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre],
95+
simp_rw category.assoc,
96+
erw colimit.ι_pre ((open_nhds.inclusion (f x)).op ⋙ X.presheaf)
97+
(h.is_open_map.functor_nhds x).op,
98+
erw ← X.presheaf.map_comp_assoc,
99+
exact (colimit.w ((open_nhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm,
100+
end
101+
102+
instance of_restrict_stalk_map_is_iso {U : Top} (X : PresheafedSpace C)
103+
{f : U ⟶ (X : Top.{v})} (h : open_embedding f) (x : U) :
104+
is_iso (stalk_map (X.of_restrict h) x) :=
105+
by { rw ← restrict_stalk_iso_inv_eq_of_restrict, apply_instance }
106+
86107
end restrict
87108

88109
namespace stalk_map

‎src/topology/sheaves/stalks.lean

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import topology.sheaves.presheaf
88
import topology.sheaves.sheaf_condition.unique_gluing
99
import category_theory.limits.types
1010
import category_theory.limits.preserves.filtered
11+
import category_theory.limits.final
1112
import tactic.elementwise
1213

1314
/-!
@@ -183,7 +184,32 @@ begin
183184
refl,
184185
end
185186

187+
lemma stalk_pushforward_iso_of_open_embedding {f : X ⟶ Y} (hf : open_embedding f)
188+
(F : X.presheaf C) (x : X) : is_iso (F.stalk_pushforward _ f x) :=
189+
begin
190+
haveI := functor.initial_of_adjunction (hf.is_open_map.adjunction_nhds x),
191+
convert is_iso.of_iso ((functor.final.colimit_iso (hf.is_open_map.functor_nhds x).op
192+
((open_nhds.inclusion (f x)).op ⋙ f _* F) : _).symm ≪≫ colim.map_iso _),
193+
swap,
194+
{ fapply nat_iso.of_components,
195+
{ intro U,
196+
refine F.map_iso (eq_to_iso _),
197+
dsimp only [functor.op],
198+
exact congr_arg op (subtype.eq $ set.preimage_image_eq (unop U).1.1 hf.inj) },
199+
{ intros U V i, erw [← F.map_comp, ← F.map_comp], congr } },
200+
{ ext U,
201+
rw ← iso.comp_inv_eq,
202+
erw colimit.ι_map_assoc,
203+
rw [colimit.ι_pre, category.assoc],
204+
erw [colimit.ι_map_assoc, colimit.ι_pre, ← F.map_comp_assoc],
205+
apply colimit.w ((open_nhds.inclusion (f x)).op ⋙ f _* F) _,
206+
dsimp only [functor.op],
207+
refine ((hom_of_le _).op : op (unop U) ⟶ _),
208+
exact set.image_preimage_subset _ _ },
209+
end
210+
186211
end stalk_pushforward
212+
187213
section stalk_pullback
188214

189215
/-- The morphism `ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ` that factors through `(f_*f⁻¹ℱ)_{f x}`. -/

0 commit comments

Comments
 (0)