mathlib documentation

@[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

@[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

@[reducible]

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

Prop

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

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

@[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) :

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

@[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 _)

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

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) :

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

Equations

@[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

@[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

@[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] :

@[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.

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

@[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'

@[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)

@[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)

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 _)

@[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'

@[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

@[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 _)

@[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'

@[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

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'

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.

algebraic_geometry.PresheafedSpace.is_open_immersion H.hom

@[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) :

An isomorphism is an open immersion.

algebraic_geometry.PresheafedSpace.is_open_immersion f

@[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] :

@[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)

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

@[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))

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.

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

@[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) :

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' := _}}

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

category_theory.limits.pullback_cone f g

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) :

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 _) _

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' := _}}

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

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

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

@[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) :

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

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) :

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, _⟩)

@[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) :

@[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) :

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

@[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) :

Open immersions are stable under base-change.

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

@[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) :

Open immersions are stable under base-change.

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

@[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] :

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

@[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) :

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))))

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

@[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) :

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

category_theory.is_iso category_theory.limits.pullback.snd

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)) :

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

@[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'

@[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

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

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' := _}

@[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 _

@[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 _

algebraic_geometry.SheafedSpace C

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] :

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 := _}

@[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

algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f ⟶ Y

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] :

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

@[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

@[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

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

@[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.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f = X

@[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.LocallyRingedSpace

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] :

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 := _}

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

@[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 ⟶ Y

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] :

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 := _}

@[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

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

@[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.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y f.val = X

@[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] :

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))

algebraic_geometry.SheafedSpace.is_open_immersion f

@[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] :

@[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)

@[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] :

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

@[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] :

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

@[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 g f ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)

@[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.creates_limit (category_theory.limits.cospan f g) algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

@[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] :

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)

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

@[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] :

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)

@[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)

@[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

@[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] :

@[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] :

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

@[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] :

Open immersions are stable under base-change.

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

@[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.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

@[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] :

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.

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)

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

@[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.LocallyRingedSpace.is_open_immersion g

@[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] :

@[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)

@[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] :

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

@[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] :

category_theory.limits.pullback_cone f g

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] :

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 _) _

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

@[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] :

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

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] :

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 := _}, _⟩)

@[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] :

@[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] :

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

@[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] :

Open immersions are stable under base-change.

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

@[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] :

Open immersions are stable under base-change.

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

@[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] :

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

@[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] :

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)))

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

@[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] :

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))

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

@[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] :

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

@[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] :

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))

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

@[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] :

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

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

@[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] :

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

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

@[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] :

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

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

@[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] :

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

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

@[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] :

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)

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

@[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] :

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)

category_theory.is_iso category_theory.limits.pullback.snd

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)) :

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

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

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_fac_assoc {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)) {X' : algebraic_geometry.LocallyRingedSpace} (f' : Z ⟶ X') :

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

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_fac {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)) :

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

theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_uniq {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)) (l : Y ⟶ X) (hl : l ≫ f = g) :

l = algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift f g H'

theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_range {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)) :

set.range ⇑((algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift f g H').val.base) = ⇑(f.val.base) ⁻¹' set.range ⇑(g.val.base)

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

X ≅ Y.restrict _

An open immersion is isomorphic to the induced open subscheme on its image.

Equations

H.iso_restrict = algebraic_geometry.LocallyRingedSpace.iso_of_SheafedSpace_iso (algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.preimage_iso (algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict H))

algebraic_geometry.Scheme

@[protected]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme (X : algebraic_geometry.LocallyRingedSpace) (h : ∀ (x : ↥X), ∃ (R : CommRing) (f : algebraic_geometry.Spec.to_LocallyRingedSpace.obj (opposite.op R) ⟶ X), x ∈ set.range ⇑(f.val.base) ∧ algebraic_geometry.LocallyRingedSpace.is_open_immersion f) :

To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme X h = {to_LocallyRingedSpace := X, local_affine := _}

theorem algebraic_geometry.is_open_immersion.open_range {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] :

is_open (set.range ⇑(f.val.base))

structure algebraic_geometry.Scheme.open_cover (X : algebraic_geometry.Scheme) :

Type (max (u+1) (v+1))

J : Type ?
obj : self.J → algebraic_geometry.Scheme
map : Π (j : self.J), self.obj j ⟶ X
f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → self.J
covers : ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), x ∈ set.range ⇑((self.map (self.f x)).val.base)
is_open : (∀ (x : self.J), algebraic_geometry.is_open_immersion (self.map x)) . "apply_instance"

An open cover of X consists of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.

This is merely a coverage in the Zariski pretopology, and it would be optimal if we could reuse the existing API about pretopologies, However, the definitions of sieves and grothendieck topologies uses Props, so that the actual open sets and immersions are hard to obtain. Also, since such a coverage in the pretopology usually contains a proper class of immersions, it is quite hard to glue them, reason about finite covers, etc.

Instances for algebraic_geometry.Scheme.open_cover

algebraic_geometry.Scheme.open_cover.has_sizeof_inst
algebraic_geometry.Scheme.open_cover.inhabited

noncomputable def algebraic_geometry.Scheme.affine_cover (X : algebraic_geometry.Scheme) :

The affine cover of a scheme.

Equations

X.affine_cover = {J := ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), obj := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.Scheme.Spec.obj (opposite.op (Exists.some _)), map := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), (nonempty.some _).inv ≫ X.to_LocallyRingedSpace.of_restrict _, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), x, covers := _, is_open := _}

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.open_cover.inhabited {X : algebraic_geometry.Scheme} :

inhabited X.open_cover

Equations

algebraic_geometry.Scheme.open_cover.inhabited = {default := X.affine_cover}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :

(𝒰.bind f).obj x = (f x.fst).obj x.snd

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :

(𝒰.bind f).J = Σ (i : 𝒰.J), (f i).J

noncomputable def algebraic_geometry.Scheme.open_cover.bind {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :

Given an open cover { Uᵢ } of X, and for each Uᵢ an open cover, we may combine these open covers to form an open cover of X.

Equations

𝒰.bind f = {J := Σ (i : 𝒰.J), (f i).J, obj := λ (x : Σ (i : 𝒰.J), (f i).J), (f x.fst).obj x.snd, map := λ (x : Σ (i : 𝒰.J), (f i).J), (f x.fst).map x.snd ≫ 𝒰.map x.fst, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.some _)⟩, covers := _, is_open := _}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :

(𝒰.bind f).map x = (f x.fst).map x.snd ≫ 𝒰.map x.fst

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_is_iso_map {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (_x : punit) :

(algebraic_geometry.Scheme.open_cover_of_is_iso f).map _x = f

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_is_iso_J {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

(algebraic_geometry.Scheme.open_cover_of_is_iso f).J = punit

def algebraic_geometry.Scheme.open_cover_of_is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

Y.open_cover

An isomorphism X ⟶ Y is an open cover of Y.

Equations

algebraic_geometry.Scheme.open_cover_of_is_iso f = {J := punit, obj := λ (_x : punit), X, map := λ (_x : punit), f, f := λ (_x : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), punit.star, covers := _, is_open := _}

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_is_iso_obj {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (_x : punit) :

(algebraic_geometry.Scheme.open_cover_of_is_iso f).obj _x = X

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) (i : J) :

(𝒰.copy J obj map e₁ e₂ e₂_1).map i = map i

def algebraic_geometry.Scheme.open_cover.copy {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) :

We construct an open cover from another, by providing the needed fields and showing that the provided fields are isomorphic with the original open cover.

Equations

𝒰.copy J obj map e₁ e₂ e₂_1 = {J := J, obj := obj, map := map, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), ⇑(e₁.symm) (𝒰.f x), covers := _, is_open := _}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) :

(𝒰.copy J obj map e₁ e₂ e₂_1).J = J

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) (ᾰ : J) :

(𝒰.copy J obj map e₁ e₂ e₂_1).obj ᾰ = obj ᾰ

noncomputable def algebraic_geometry.Scheme.open_cover.pushforward_iso {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] :

Y.open_cover

The pushforward of an open cover along an isomorphism.

Equations

𝒰.pushforward_iso f = ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).copy 𝒰.J (λ (_x : 𝒰.J), ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).obj (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x)) (λ (_x : 𝒰.J), ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).map (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x)) ((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) (λ (_x : 𝒰.J), category_theory.iso.refl (((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).obj (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x))) _

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_map {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] (_x : 𝒰.J) :

(𝒰.pushforward_iso f).map _x = 𝒰.map _x ≫ f

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_obj {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] (_x : 𝒰.J) :

(𝒰.pushforward_iso f).obj _x = 𝒰.obj _x

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_J {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] :

(𝒰.pushforward_iso f).J = 𝒰.J

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_f {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(𝒰.add f).f x = option.some (𝒰.f x)

def algebraic_geometry.Scheme.open_cover.add {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] :

Adding an open immersion into an open cover gives another open cover.

Equations

𝒰.add f = {J := option 𝒰.J, obj := λ (i : option 𝒰.J), option.rec Y 𝒰.obj i, map := λ (i : option 𝒰.J), option.rec f 𝒰.map i, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), option.some (𝒰.f x), covers := _, is_open := _}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (i : option 𝒰.J) :

(𝒰.add f).map i = option.rec f 𝒰.map i

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] :

(𝒰.add f).J = option 𝒰.J

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (i : option 𝒰.J) :

(𝒰.add f).obj i = option.rec Y 𝒰.obj i

@[protected, instance]

def algebraic_geometry.Scheme.val_base_is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso f.val.base

@[protected, instance]

def algebraic_geometry.Scheme.basic_open_is_open_immersion {R : CommRing} (f : ↥R) :

algebraic_geometry.is_open_immersion (algebraic_geometry.Scheme.Spec.map (CommRing.of_hom (algebra_map ↥R (localization.away f))).op)

noncomputable def algebraic_geometry.Scheme.affine_basis_cover_of_affine (R : CommRing) :

(algebraic_geometry.Scheme.Spec.obj (opposite.op R)).open_cover

The basic open sets form an affine open cover of Spec R.

Equations

algebraic_geometry.Scheme.affine_basis_cover_of_affine R = {J := ↥R, obj := λ (r : ↥R), algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of (localization.away r))), map := λ (r : ↥R), algebraic_geometry.Scheme.Spec.map (quiver.hom.op (algebra_map ↥R (localization.away r))), f := λ (x : ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), 1, covers := _, is_open := _}

noncomputable def algebraic_geometry.Scheme.affine_basis_cover (X : algebraic_geometry.Scheme) :

We may bind the basic open sets of an open affine cover to form a affine cover that is also a basis.

Equations

X.affine_basis_cover = X.affine_cover.bind (λ (x : X.affine_cover.J), algebraic_geometry.Scheme.affine_basis_cover_of_affine (Exists.some _))

noncomputable def algebraic_geometry.Scheme.affine_basis_cover_ring (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

CommRing

The coordinate ring of a component in the affine_basis_cover.

Equations

X.affine_basis_cover_ring i = CommRing.of (localization.away i.snd)

theorem algebraic_geometry.Scheme.affine_basis_cover_obj (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

X.affine_basis_cover.obj i = algebraic_geometry.Scheme.Spec.obj (opposite.op (X.affine_basis_cover_ring i))

theorem algebraic_geometry.Scheme.affine_basis_cover_map_range (X : algebraic_geometry.Scheme) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (r : ↥(Exists.some _)) :

set.range ⇑((X.affine_basis_cover.map ⟨x, r⟩).val.base) = ⇑((X.affine_cover.map x).val.base) '' (prime_spectrum.basic_open r).carrier

theorem algebraic_geometry.Scheme.affine_basis_cover_is_basis (X : algebraic_geometry.Scheme) :

topological_space.is_topological_basis {x : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) | ∃ (a : X.affine_basis_cover.J), x = set.range ⇑((X.affine_basis_cover.map a).val.base)}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.finite_subcover_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (x : ↥(_.some)) :

𝒰.finite_subcover.obj x = 𝒰.obj (𝒰.f x.val)

noncomputable def algebraic_geometry.Scheme.open_cover.finite_subcover {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

Every open cover of a quasi-compact scheme can be refined into a finite subcover.

Equations

𝒰.finite_subcover = let t : finset ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) := _.some in {J := ↥t, obj := λ (x : ↥t), 𝒰.obj (𝒰.f x.val), map := λ (x : ↥t), 𝒰.map (𝒰.f x.val), f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), Exists.some _, covers := _, is_open := _}

@[simp]

theorem algebraic_geometry.Scheme.open_cover.finite_subcover_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (x : ↥(_.some)) :

𝒰.finite_subcover.map x = 𝒰.map (𝒰.f x.val)

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.J.fintype {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

fintype 𝒰.finite_subcover.J

Equations

algebraic_geometry.Scheme.J.fintype 𝒰 = id (finset.subtype.fintype _.some)

algebraic_geometry.Scheme

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

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

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f = algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme (algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y.to_LocallyRingedSpace f) _

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

@[simp]

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

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f ⟶ Y

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

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

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom Y f = algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y.to_LocallyRingedSpace f

@[simp]

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

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

algebraic_geometry.is_open_immersion (algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom Y f)

@[protected, instance]

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

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.Scheme_eq_of_LocallyRingedSpace_eq {X Y : algebraic_geometry.Scheme} (H : X.to_LocallyRingedSpace = Y.to_LocallyRingedSpace) :

X = Y

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

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

algebraic_geometry.Scheme

def algebraic_geometry.Scheme.restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

The restriction of a Scheme along an open embedding.

Equations

X.restrict h = {to_LocallyRingedSpace := {to_SheafedSpace := {to_PresheafedSpace := X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.restrict h, is_sheaf := _}, local_ring := _}, local_affine := _}

Instances for algebraic_geometry.Scheme.restrict

algebraic_geometry.Scheme.restrict.is_integral

@[simp]

theorem algebraic_geometry.Scheme.of_restrict_val_base {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

(X.of_restrict h).val.base = f

@[simp]

theorem algebraic_geometry.Scheme.of_restrict_val_c_app {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) (V : (topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) :

(X.of_restrict h).val.c.app V = X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (_.adjunction.counit.app (opposite.unop V)).op

def algebraic_geometry.Scheme.of_restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

X.restrict h ⟶ X

The canonical map from the restriction to the supspace.

Equations

X.of_restrict h = X.to_LocallyRingedSpace.of_restrict h

@[protected, instance]

def algebraic_geometry.is_open_immersion.of_restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

algebraic_geometry.is_open_immersion (X.of_restrict h)

algebraic_geometry.is_open_immersion g

@[protected, instance]

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

theorem algebraic_geometry.is_open_immersion.to_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [h : algebraic_geometry.is_open_immersion f] [category_theory.epi f.val.base] :

category_theory.is_iso f

algebraic_geometry.is_open_immersion f

theorem algebraic_geometry.is_open_immersion.of_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (hf : open_embedding ⇑(f.val.base)) [∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)] :

theorem algebraic_geometry.is_open_immersion.iff_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

algebraic_geometry.is_open_immersion f ↔ open_embedding ⇑(f.val.base) ∧ ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)

theorem algebraic_geometry.is_iso_iff_is_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

category_theory.is_iso f ↔ algebraic_geometry.is_open_immersion f ∧ category_theory.epi f.val.base

theorem algebraic_geometry.is_iso_iff_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

category_theory.is_iso f ↔ category_theory.is_iso f.val.base ∧ ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)

noncomputable def algebraic_geometry.is_open_immersion.iso_restrict {X Z : algebraic_geometry.Scheme} (f : X ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

X ≅ Z.restrict _

A open immersion induces an isomorphism from the domain onto the image

Equations

algebraic_geometry.is_open_immersion.iso_restrict f = {hom := (algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict H).hom, inv := (algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict H).inv, hom_inv_id' := _, inv_hom_id' := _}

@[protected, instance]

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

algebraic_geometry.LocallyRingedSpace.is_open_immersion (algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.map f)

@[protected, instance]

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

category_theory.limits.has_limit (category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)

@[protected, instance]

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

category_theory.limits.has_limit (category_theory.limits.cospan ((category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inl) ((category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inr))

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_left' {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)

@[protected, instance]

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

category_theory.limits.has_limit (category_theory.limits.cospan ((category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inl) ((category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inr))

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_right' {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.creates_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[protected, instance]

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

Equations

algebraic_geometry.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_Scheme Y category_theory.limits.pullback.snd.val) (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.Scheme.forget_to_LocallyRingedSpace)).symm)

category_theory.creates_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[protected, instance]

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

Equations

algebraic_geometry.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_Scheme Y category_theory.limits.pullback.fst.val) (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.Scheme.forget_to_LocallyRingedSpace)).symm)

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[protected, instance]

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

Equations

algebraic_geometry.is_open_immersion.forget_preserves_of_left f g = category_theory.preserves_limit_of_creates_limit_and_has_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[protected, instance]

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

Equations

algebraic_geometry.is_open_immersion.forget_preserves_of_right f g = category_theory.limits.preserves_pullback_symmetry algebraic_geometry.Scheme.forget_to_LocallyRingedSpace f g

@[protected, instance]

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

@[protected, instance]

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

algebraic_geometry.is_open_immersion category_theory.limits.pullback.snd

@[protected, instance]

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

algebraic_geometry.is_open_immersion category_theory.limits.pullback.fst

@[protected, instance]

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

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

@[protected, instance]

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

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_Top

@[protected, instance]

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

Equations

algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_left f g = category_theory.limits.comp_preserves_limit algebraic_geometry.Scheme.forget_to_LocallyRingedSpace algebraic_geometry.LocallyRingedSpace.forget_to_Top

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_Top

@[protected, instance]

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

Equations

algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_right f g = category_theory.limits.preserves_pullback_symmetry algebraic_geometry.Scheme.forget_to_Top f g

theorem algebraic_geometry.is_open_immersion.range_pullback_snd_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑(category_theory.limits.pullback.snd.val.base) = ↑((topological_space.opens.map g.val.base).obj {carrier := set.range ⇑(f.val.base), is_open' := _})

theorem algebraic_geometry.is_open_immersion.range_pullback_fst_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑(category_theory.limits.pullback.fst.val.base) = ↑((topological_space.opens.map g.val.base).obj {carrier := set.range ⇑(f.val.base), is_open' := _})

theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑((category_theory.limits.pullback.fst ≫ f).val.base) = set.range ⇑(f.val.base) ∩ set.range ⇑(g.val.base)

theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑((category_theory.limits.pullback.fst ≫ g).val.base) = set.range ⇑(g.val.base) ∩ set.range ⇑(f.val.base)