algebraic_geometry.open_immersion.basic

@[class]

structure algebraic_geometry.PresheafedSpace.is_open_immersion {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) :

Prop

base_open : open_embedding ⇑(f.base)
c_iso : ∀ (U : topological_space.opens ↥X), category_theory.is_iso (f.c.app (opposite.op (_.functor.obj U)))

An open immersion of PresheafedSpaces is an open embedding f : X ⟶ U ⊆ Y of the underlying spaces, such that the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Instances of this typeclass

source

@[reducible]

def algebraic_geometry.SheafedSpace.is_open_immersion {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) :

Prop

A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism of PresheafedSpaces

source

@[reducible]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) :

Prop

A morphism of LocallyRingedSpaces is an open immersion if it is an open immersion as a morphism of SheafedSpaces

source

@[reducible]

def algebraic_geometry.PresheafedSpace.is_open_immersion.open_functor {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) :

topological_space.opens ↥↑X ⥤ topological_space.opens ↥↑Y

The functor opens X ⥤ opens Y associated with an open immersion f : X ⟶ Y.

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_c_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (X_1 : (topological_space.opens ↥((Y.restrict algebraic_geometry.PresheafedSpace.is_open_immersion.base_open).carrier))ᵒᵖ) :

H.iso_restrict.hom.c.app X_1 = f.c.app (opposite.op (H.open_functor.obj (opposite.unop X_1))) ≫ X.presheaf.map (category_theory.eq_to_hom _)

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) :

X ≅ Y.restrict algebraic_geometry.PresheafedSpace.is_open_immersion.base_open

An open immersion f : X ⟶ Y induces an isomorphism X ≅ Y|_{f(X)}.

Equations

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_of_restrict {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) :

H.iso_restrict.hom ≫ Y.of_restrict algebraic_geometry.PresheafedSpace.is_open_immersion.base_open = f

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_inv_of_restrict {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) :

H.iso_restrict.inv ≫ f = Y.of_restrict algebraic_geometry.PresheafedSpace.is_open_immersion.base_open

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.mono {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

category_theory.mono f

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.comp {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) [hg : algebraic_geometry.PresheafedSpace.is_open_immersion g] :

algebraic_geometry.PresheafedSpace.is_open_immersion (f ≫ g)

The composition of two open immersions is an open immersion.

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) :

X.presheaf.obj (opposite.op U) ⟶ Y.presheaf.obj (opposite.op (H.open_functor.obj U))

For an open immersion f : X ⟶ Y and an open set U ⊆ X, we have the map X(U) ⟶ Y(U).

Equations

H.inv_app U = X.presheaf.map (category_theory.eq_to_hom _) ≫ category_theory.inv (f.c.app (opposite.op (H.open_functor.obj U)))

Instances for algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app

algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app.category_theory.is_iso

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_naturality_assoc {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) {U V : (topological_space.opens ↥X)ᵒᵖ} (i : U ⟶ V) {X' : C} (f' : Y.presheaf.obj (opposite.op (H.open_functor.obj (opposite.unop V))) ⟶ X') :

X.presheaf.map i ≫ H.inv_app (opposite.unop V) ≫ f' = H.inv_app (opposite.unop U) ≫ Y.presheaf.map (H.open_functor.op.map i) ≫ f'

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_naturality {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) {U V : (topological_space.opens ↥X)ᵒᵖ} (i : U ⟶ V) :

X.presheaf.map i ≫ H.inv_app (opposite.unop V) = H.inv_app (opposite.unop U) ≫ Y.presheaf.map (H.open_functor.op.map i)

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app.category_theory.is_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) :

category_theory.is_iso (H.inv_app U)

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_inv_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) :

category_theory.inv (H.inv_app U) = f.c.app (opposite.op (H.open_functor.obj U)) ≫ X.presheaf.map (category_theory.eq_to_hom _)

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app_assoc {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) {X' : C} (f' : (f.base _* X.presheaf).obj (opposite.op (H.open_functor.obj U)) ⟶ X') :

H.inv_app U ≫ f.c.app (opposite.op (H.open_functor.obj U)) ≫ f' = X.presheaf.map (category_theory.eq_to_hom _) ≫ f'

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app_apply {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) [I : category_theory.concrete_category C] (x : ↥(X.presheaf.obj (opposite.op U))) :

⇑(f.c.app (opposite.op (H.open_functor.obj U))) (⇑(H.inv_app U) x) = ⇑(X.presheaf.map (category_theory.eq_to_hom _)) x

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥X) :

H.inv_app U ≫ f.c.app (opposite.op (H.open_functor.obj U)) = X.presheaf.map (category_theory.eq_to_hom _)

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app_assoc {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥Y) {X' : C} (f' : Y.presheaf.obj (opposite.op (H.open_functor.obj ((topological_space.opens.map f.base).obj U))) ⟶ X') :

f.c.app (opposite.op U) ≫ H.inv_app ((topological_space.opens.map f.base).obj U) ≫ f' = Y.presheaf.map (category_theory.hom_of_le _).op ≫ f'

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥Y) :

f.c.app (opposite.op U) ≫ H.inv_app ((topological_space.opens.map f.base).obj U) = Y.presheaf.map (category_theory.hom_of_le _).op

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app'_assoc {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥Y) (hU : ↑U ⊆ set.range ⇑(f.base)) {X' : C} (f' : Y.presheaf.obj (opposite.op (H.open_functor.obj ((topological_space.opens.map f.base).obj U))) ⟶ X') :

f.c.app (opposite.op U) ≫ H.inv_app ((topological_space.opens.map f.base).obj U) ≫ f' = Y.presheaf.map (category_theory.eq_to_hom _).op ≫ f'

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app' {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} (H : algebraic_geometry.PresheafedSpace.is_open_immersion f) (U : topological_space.opens ↥Y) (hU : ↑U ⊆ set.range ⇑(f.base)) :

f.c.app (opposite.op U) ≫ H.inv_app ((topological_space.opens.map f.base).obj U) = Y.presheaf.map (category_theory.eq_to_hom _).op

A variant of app_inv_app that gives an eq_to_hom instead of hom_of_le.

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.of_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (H : X ≅ Y) :

algebraic_geometry.PresheafedSpace.is_open_immersion H.hom

An isomorphism is an open immersion.

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.of_is_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) [category_theory.is_iso f] :

algebraic_geometry.PresheafedSpace.is_open_immersion f

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict {C : Type u} [category_theory.category C] {X : Top} (Y : algebraic_geometry.PresheafedSpace C) {f : X ⟶ Y.carrier} (hf : open_embedding ⇑f) :

algebraic_geometry.PresheafedSpace.is_open_immersion (Y.of_restrict hf)

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict_inv_app_apply {C : Type u_1} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) {Y : Top} {f : Y ⟶ Top.of ↥(X.carrier)} (h : open_embedding ⇑f) (U : topological_space.opens ↥((X.restrict h).carrier)) [I : category_theory.concrete_category C] (x : ↥((X.restrict h).presheaf.obj (opposite.op U))) :

⇑(_.inv_app U) x = x

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict_inv_app {C : Type u_1} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) {Y : Top} {f : Y ⟶ Top.of ↥(X.carrier)} (h : open_embedding ⇑f) (U : topological_space.opens ↥((X.restrict h).carrier)) :

_.inv_app U = 𝟙 ((X.restrict h).presheaf.obj (opposite.op U))

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) [h : algebraic_geometry.PresheafedSpace.is_open_immersion f] [h' : category_theory.epi f.base] :

category_theory.is_iso f

An open immersion is an iso if the underlying continuous map is epi.

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.stalk_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {f : X ⟶ Y} [category_theory.limits.has_colimits C] [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] (x : ↥X) :

category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f x)

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

Y.restrict _ ⟶ X

(Implementation.) The projection map when constructing the pullback along an open immersion.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst f g = {base := category_theory.limits.pullback.fst _, c := {app := λ (U : (topological_space.opens ↥(X.carrier))ᵒᵖ), hf.inv_app (opposite.unop U) ≫ g.c.app (opposite.op (_.functor.obj (opposite.unop U))) ≫ Y.presheaf.map (category_theory.eq_to_hom _), naturality' := _}}

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_condition {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst f g ≫ f = Y.of_restrict _ ≫ g

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.pullback_cone f g

We construct the pullback along an open immersion via restricting along the pullback of the maps of underlying spaces (which is also an open embedding).

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g = category_theory.limits.pullback_cone.mk (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst f g) (Y.of_restrict _) _

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (s : category_theory.limits.pullback_cone f g) :

s.X ⟶ (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).X

(Implementation.) Any cone over cospan f g indeed factors through the constructed cone.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift f g s = {base := category_theory.limits.pullback.lift s.fst.base s.snd.base _, c := {app := λ (U : (topological_space.opens ↥((algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).X.carrier))ᵒᵖ), s.snd.c.app (_.functor.op.obj U) ≫ s.X.presheaf.map (category_theory.eq_to_hom _), naturality' := _}}

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift_fst {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (s : category_theory.limits.pullback_cone f g) :

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift f g s ≫ (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).fst = s.fst

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift_snd {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (s : category_theory.limits.pullback_cone f g) :

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift f g s ≫ (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).snd = s.snd

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_snd_is_open_immersion {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

algebraic_geometry.PresheafedSpace.is_open_immersion (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).snd

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.is_limit (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g)

The constructed pullback cone is indeed the pullback.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit f g = (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift f g s, _⟩)

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.has_pullback_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.has_pullback f g

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.has_pullback_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.has_pullback g f

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

algebraic_geometry.PresheafedSpace.is_open_immersion category_theory.limits.pullback.snd

Open immersions are stable under base-change.

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_fst_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

algebraic_geometry.PresheafedSpace.is_open_immersion category_theory.limits.pullback.fst

Open immersions are stable under base-change.

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_to_base_is_open_immersion {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) [algebraic_geometry.PresheafedSpace.is_open_immersion g] :

algebraic_geometry.PresheafedSpace.is_open_immersion (category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

source

@[protected, instance]

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) (algebraic_geometry.PresheafedSpace.forget C)

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_left f g = category_theory.limits.preserves_limit_of_preserves_limit_cone (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit f g) ((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan f g ⋙ algebraic_geometry.PresheafedSpace.forget C)) ((algebraic_geometry.PresheafedSpace.forget C).map_cone (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left f g))).to_fun ((category_theory.limits.is_limit.equiv_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl (category_theory.limits.limit.cone (category_theory.limits.cospan ((category_theory.limits.cospan f g ⋙ algebraic_geometry.PresheafedSpace.forget C).map category_theory.limits.walking_cospan.hom.inl) ((category_theory.limits.cospan f g ⋙ algebraic_geometry.PresheafedSpace.forget C).map category_theory.limits.walking_cospan.hom.inr))).X) _)).to_fun (category_theory.limits.limit.is_limit (category_theory.limits.cospan f.base g.base))))

source

@[protected, instance]

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) (algebraic_geometry.PresheafedSpace.forget C)

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_right f g = category_theory.limits.preserves_pullback_symmetry (algebraic_geometry.PresheafedSpace.forget C) f g

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (H : set.range ⇑(g.base) ⊆ set.range ⇑(f.base)) :

category_theory.is_iso category_theory.limits.pullback.snd

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.lift {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (H : set.range ⇑(g.base) ⊆ set.range ⇑(f.base)) :

Y ⟶ X

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g H = category_theory.inv category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.lift_fac_assoc {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (H : set.range ⇑(g.base) ⊆ set.range ⇑(f.base)) {X' : algebraic_geometry.PresheafedSpace C} (f' : Z ⟶ X') :

algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g H ≫ f ≫ f' = g ≫ f'

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.lift_fac {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (H : set.range ⇑(g.base) ⊆ set.range ⇑(f.base)) :

algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g H ≫ f = g

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.lift_uniq {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) (H : set.range ⇑(g.base) ⊆ set.range ⇑(f.base)) (l : Y ⟶ X) (hl : l ≫ f = g) :

l = algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g H

source

noncomputable def algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) [algebraic_geometry.PresheafedSpace.is_open_immersion g] (e : set.range ⇑(f.base) = set.range ⇑(g.base)) :

X ≅ Y

Two open immersions with equal range is isomorphic.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq f g e = {hom := algebraic_geometry.PresheafedSpace.is_open_immersion.lift g f _, inv := algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g _, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq_inv {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) [algebraic_geometry.PresheafedSpace.is_open_immersion g] (e : set.range ⇑(f.base) = set.range ⇑(g.base)) :

(algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq f g e).inv = algebraic_geometry.PresheafedSpace.is_open_immersion.lift f g _

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq_hom {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Z) [hf : algebraic_geometry.PresheafedSpace.is_open_immersion f] (g : Y ⟶ Z) [algebraic_geometry.PresheafedSpace.is_open_immersion g] (e : set.range ⇑(f.base) = set.range ⇑(g.base)) :

(algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq f g e).hom = algebraic_geometry.PresheafedSpace.is_open_immersion.lift g f _

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.SheafedSpace C

If X ⟶ Y is an open immersion, and Y is a SheafedSpace, then so is X.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f = {to_PresheafedSpace := X, is_sheaf := _}

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_to_PresheafedSpace {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f).to_PresheafedSpace = X

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f ⟶ Y

If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a SheafedSpace, we can upgrade it into a morphism of SheafedSpaces.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom Y f = f

Instances for algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_is_open_immersion

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom_base {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom Y f).base = f.base

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom_c {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom Y f).c = f.c

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_is_open_immersion {C : Type u} [category_theory.category C] {X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.SheafedSpace.is_open_immersion (algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom Y f)

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.SheafedSpace_to_SheafedSpace {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) [algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f = X

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace

If X ⟶ Y is an open immersion, and Y is a LocallyRingedSpace, then so is X.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y f = {to_SheafedSpace := algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y.to_SheafedSpace f H, local_ring := _}

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_to_SheafedSpace {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y f).to_SheafedSpace = algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y.to_SheafedSpace f

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y f ⟶ Y

If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a LocallyRingedSpace, we can upgrade it into a morphism of LocallyRingedSpace.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y f = {val := f, prop := _}

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom_val {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y f).val = f

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_is_open_immersion {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y f)

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.LocallyRingedSpace_to_LocallyRingedSpace {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) [algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y f.val = X

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.is_iso_of_subset {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] (U : topological_space.opens ↥(Y.carrier)) (hU : ↑U ⊆ set.range ⇑(f.base)) :

category_theory.is_iso (f.c.app (opposite.op U))

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.of_is_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) [category_theory.is_iso f] :

algebraic_geometry.SheafedSpace.is_open_immersion f

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.comp {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) [algebraic_geometry.SheafedSpace.is_open_immersion f] [algebraic_geometry.SheafedSpace.is_open_immersion g] :

algebraic_geometry.SheafedSpace.is_open_immersion (f ≫ g)

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.category_theory.mono {C : Type u} [category_theory.category C] {X Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.mono f

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.forget_map_is_open_immersion {C : Type u} [category_theory.category C] {X Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion (algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.map f)

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.has_limit_cospan_forget_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan f g ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.has_limit_cospan_forget_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan g f ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

source

@[protected, instance]

noncomputable def algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.creates_limit (category_theory.limits.cospan f g) algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

Equations

algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_left f g = category_theory.creates_limit_of_fully_faithful_of_iso (algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y category_theory.limits.pullback.snd) (category_theory.eq_to_iso _ ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan f g ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)).symm)

source

@[protected, instance]

noncomputable def algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.creates_limit (category_theory.limits.cospan g f) algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

Equations

algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_right f g = category_theory.creates_limit_of_fully_faithful_of_iso (algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y category_theory.limits.pullback.fst) (category_theory.eq_to_iso _ ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan g f ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)).symm)

source

@[protected, instance]

noncomputable def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) (algebraic_geometry.SheafedSpace.forget C)

Equations

algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_left f g = category_theory.limits.comp_preserves_limit algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace (algebraic_geometry.PresheafedSpace.forget C)

source

@[protected, instance]

noncomputable def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) (algebraic_geometry.SheafedSpace.forget C)

Equations

algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_right f g = category_theory.limits.preserves_pullback_symmetry (algebraic_geometry.SheafedSpace.forget C) f g

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_has_pullback_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.has_pullback f g

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_has_pullback_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

category_theory.limits.has_pullback g f

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_pullback_snd_of_left {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

algebraic_geometry.SheafedSpace.is_open_immersion category_theory.limits.pullback.snd

Open immersions are stable under base-change.

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_pullback_fst_of_right {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] :

algebraic_geometry.SheafedSpace.is_open_immersion category_theory.limits.pullback.fst

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_pullback_to_base_is_open_immersion {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.SheafedSpace.is_open_immersion f] [algebraic_geometry.SheafedSpace.is_open_immersion g] :

algebraic_geometry.SheafedSpace.is_open_immersion (category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

source

Suppose X Y : SheafedSpace C, where C is a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then a morphism X ⟶ Y that is a topological open embedding is an open immersion iff every stalk map is an iso.

source

theorem algebraic_geometry.SheafedSpace.is_open_immersion.sigma_ι_open_embedding {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] {ι : Type v} (F : category_theory.discrete ι ⥤ algebraic_geometry.SheafedSpace C) [category_theory.limits.has_colimit F] (i : category_theory.discrete ι) :

open_embedding ⇑((category_theory.limits.colimit.ι F i).base)

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_open_immersion.sigma_ι_is_open_immersion {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] {ι : Type v} (F : category_theory.discrete ι ⥤ algebraic_geometry.SheafedSpace C) [category_theory.limits.has_colimit F] (i : category_theory.discrete ι) [category_theory.limits.has_strict_terminal_objects C] :

algebraic_geometry.SheafedSpace.is_open_immersion (category_theory.limits.colimit.ι F i)

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.of_is_iso {Y Z : algebraic_geometry.LocallyRingedSpace} (g : Y ⟶ Z) [category_theory.is_iso g] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion g

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.comp {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] (g : Z ⟶ Y) [algebraic_geometry.LocallyRingedSpace.is_open_immersion g] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (f ≫ g)

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.mono {X Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.mono f

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.map.algebraic_geometry.SheafedSpace.is_open_immersion {X Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.SheafedSpace.is_open_immersion (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.map f)

source

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.pullback_cone f g

An explicit pullback cone over cospan f g if f is an open immersion.

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left f g = category_theory.limits.pullback_cone.mk {val := algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst f.val g.val, prop := _} (Y.of_restrict _) _

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.snd.is_open_immersion {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left f g).snd

source

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left_is_limit {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.is_limit (algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left f g)

The constructed pullback_cone_of_left is indeed limiting.

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left_is_limit f g = (algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left f g).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨{val := algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift f.val g.val (category_theory.limits.pullback_cone.mk s.fst.val s.snd.val _), prop := _}, _⟩)

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.has_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.has_pullback f g

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.has_pullback_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.has_pullback g f

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_snd_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion category_theory.limits.pullback.snd

Open immersions are stable under base-change.

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_fst_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion category_theory.limits.pullback.fst

Open immersions are stable under base-change.

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_to_base_is_open_immersion {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] [algebraic_geometry.LocallyRingedSpace.is_open_immersion g] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_left f g = category_theory.limits.preserves_limit_of_preserves_limit_cone (algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left_is_limit f g) ((category_theory.limits.is_limit_map_cone_pullback_cone_equiv algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace _).symm.to_fun (category_theory.limits.is_limit_of_is_limit_pullback_cone_map algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace _ (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit f.val g.val)))

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_left f g = category_theory.limits.preserves_limit_of_preserves_limit_cone (algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left_is_limit f g) ((category_theory.limits.is_limit_map_cone_pullback_cone_equiv (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace) _).symm.to_fun (algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit f.val g.val))

source

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_open_immersion {X Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion ((algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace).map f)

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_Top_preserves_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget CommRing)

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_Top_preserves_pullback_of_left f g = id (category_theory.limits.comp_preserves_limit (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace) (algebraic_geometry.PresheafedSpace.forget CommRing))

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.reflects_limit (category_theory.limits.cospan f g) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_left f g = category_theory.limits.reflects_limit_of_reflects_isomorphisms (category_theory.limits.cospan f g) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_right f g = category_theory.limits.preserves_pullback_symmetry algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace f g

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_preserves_pullback_of_right f g = category_theory.limits.preserves_pullback_symmetry (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace) f g

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.reflects_limit (category_theory.limits.cospan g f) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_right f g = category_theory.limits.reflects_limit_of_reflects_isomorphisms (category_theory.limits.cospan g f) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_left {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.reflects_limit (category_theory.limits.cospan f g) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_left f g = category_theory.limits.reflects_limit_of_reflects_isomorphisms (category_theory.limits.cospan f g) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

source

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_right {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] :

category_theory.limits.reflects_limit (category_theory.limits.cospan g f) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_to_PresheafedSpace_reflects_pullback_of_right f g = category_theory.limits.reflects_limit_of_reflects_isomorphisms (category_theory.limits.cospan g f) (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

source

theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) :

category_theory.is_iso category_theory.limits.pullback.snd

source

noncomputable def algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.LocallyRingedSpace.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) :

Y ⟶ X

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Equations