Open immersions of structured spaces

We say that a morphism of presheafed spaces f : X ⟶ Y is an open immersion if the underlying map of spaces is an open embedding f : X ⟶ U ⊆ Y, and the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Abbreviations are also provided for SheafedSpace, LocallyRingedSpace and Scheme.

Main definitions

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion: the Prop-valued typeclass asserting that a PresheafedSpace hom f is an open_immersion.
• AlgebraicGeometry.IsOpenImmersion: the Prop-valued typeclass asserting that a Scheme morphism f is an open_immersion.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict: The source of an open immersion is isomorphic to the restriction of the target onto the image.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift: Any morphism whose range is contained in an open immersion factors through the open immersion.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace: If f : X ⟶ Y is an open immersion of presheafed spaces, and Y is a sheafed space, then X is also a sheafed space. The morphism as morphisms of sheafed spaces is given by toSheafedSpaceHom.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace: If f : X ⟶ Y is an open immersion of presheafed spaces, and Y is a locally ringed space, then X is also a locally ringed space. The morphism as morphisms of locally ringed spaces is given by toLocallyRingedSpaceHom.

Main results

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp: The composition of two open immersions is an open immersion.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso: An iso is an open immersion.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso: A surjective open immersion is an isomorphism.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso: An open immersion induces an isomorphism on stalks.
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left: If f is an open immersion, then the pullback (f, g) exists (and the forgetful functor to TopCat preserves it).
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft: Open immersions are stable under pullbacks.
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso: A (topological) open embedding between two sheafed spaces is an open immersion if all the stalk maps are isomorphisms.

class AlgebraicGeometry.PresheafedSpace.IsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) : Prop

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.

• base_open : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

  the underlying continuous map of underlying spaces from the source to an open subset of the target.

• c_iso (U : TopologicalSpace.Opens ↑↑X) : CategoryTheory.IsIso (f.c.app (Opposite.op (⋯.functor.obj U)))

  the underlying sheaf morphism is an isomorphism on each open subset

@[reducible, inline]

abbrev AlgebraicGeometry.SheafedSpace.IsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : 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

theorem AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) : IsOpenImmersion f ↔ PresheafedSpace.IsOpenImmersion f.hom

@[reducible, inline]

abbrev AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion {X Y : LocallyRingedSpace} (f : X ⟶ Y) : Prop

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

instance AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion {X Y : LocallyRingedSpace} (f : X ⟶ Y) [LocallyRingedSpace.IsOpenImmersion f] : PresheafedSpace.IsOpenImmersion f.toHom

@[reducible, inline]

abbrev AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X) (TopologicalSpace.Opens ↑↑Y)

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

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : X ≅ Y.restrict ⋯

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (X✝ : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ) : (isoRestrict f).hom.c.app X✝ = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((opensFunctor f).obj (Opposite.unop X✝)))) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (Y.ofRestrict ⋯) = f

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : PresheafedSpace C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv f = Y.ofRestrict ⋯

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : PresheafedSpace C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.Mono f

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {V : TopologicalSpace.Opens ↑↑Y} (U : TopologicalSpace.Opens ↑↑X) (h : V = (opensFunctor f).obj U) : CategoryTheory.IsIso (f.c.app (Opposite.op V))

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : PresheafedSpace C} (g : Y ⟶ Z) [hg : IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)

The composition of two open immersions is an open immersion.

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((opensFunctor f).obj U))

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (invApp f (Opposite.unop V)) = CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (Y.presheaf.map ((opensFunctor f).op.map i))

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ} (i : U ⟶ V) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop V))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop V)) h) = CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (CategoryTheory.CategoryStruct.comp (Y.presheaf.map ((opensFunctor f).op.map i)) h)

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) : CategoryTheory.IsIso (invApp f U)

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) : CategoryTheory.inv (invApp f U) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((opensFunctor f).obj U))) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) : CategoryTheory.CategoryStruct.comp (invApp f U) (f.c.app (Opposite.op ((opensFunctor f).obj U))) = X.presheaf.map (CategoryTheory.eqToHom ⋯)

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) {Z : C} (h : ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).obj (Opposite.op ((opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (invApp f U) (CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((opensFunctor f).obj U))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op ((opensFunctor f).obj U)))) ((CategoryTheory.ConcreteCategory.hom (invApp f U)) x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (H : X ≅ Y) : IsOpenImmersion H.hom

An isomorphism is an open immersion.

@[instance 100]

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsOpenImmersion f

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ ↑Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (Y.ofRestrict hf)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h)) : invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h)) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (invApp (X.ofRestrict h) U)) x = x

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] [h' : CategoryTheory.Epi f.base] : CategoryTheory.IsIso f

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

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] [CategoryTheory.Limits.HasColimits C] (x : ↑↑X) : CategoryTheory.IsIso (Hom.stalkMap f x)

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : Y.restrict ⋯ ⟶ X

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackConeOfLeftFst f g) f = CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) g

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.PullbackCone 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).

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (s : CategoryTheory.Limits.PullbackCone f g) : s.pt ⟶ (pullbackConeOfLeft f g).pt

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (pullbackConeOfLeftLift f g s) (pullbackConeOfLeft f g).fst = s.fst

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (pullbackConeOfLeftLift f g s) (pullbackConeOfLeft f g).snd = s.snd

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : IsOpenImmersion (pullbackConeOfLeft f g).snd

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.IsLimit (pullbackConeOfLeft f g)

The constructed pullback cone is indeed the pullback.

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.HasPullback g f

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

Open immersions are stable under base-change.

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)

Open immersions are stable under base-change.

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (forget C)

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) (forget C)

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom 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.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.CategoryStruct.comp (lift f g H) f = g

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z✝ : PresheafedSpace C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift f g H) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_uniq {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (l : Y ⟶ X) (hl : CategoryTheory.CategoryStruct.comp l f = g) : l = lift f g H

noncomputable def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) [IsOpenImmersion g] (e : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : X ≅ Y

Two open immersions with equal range is isomorphic.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) [IsOpenImmersion g] (e : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : (isoOfRangeEq f g e).hom = lift g f ⋯

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) [IsOpenImmersion g] (e : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : (isoOfRangeEq f g e).inv = lift f g ⋯

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : SheafedSpace C

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_toPresheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSheafedSpace Y f).toPresheafedSpace = X

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : toSheafedSpace 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.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSheafedSpaceHom Y f).hom.base = f.base

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSheafedSpaceHom Y f).hom.c = f.c

@[deprecated AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base (since := "2025-12-18")]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSheafedSpaceHom Y f).hom.base = f.base

Alias of AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base.

@[deprecated AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c (since := "2025-12-18")]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSheafedSpaceHom Y f).hom.c = f.c

Alias of AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c.

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_isOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X : PresheafedSpace C} (Y : SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : SheafedSpace.IsOpenImmersion (toSheafedSpaceHom Y f)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [SheafedSpace.IsOpenImmersion f] : toSheafedSpace Y f.hom = X

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : LocallyRingedSpace

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_toSheafedSpace {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toLocallyRingedSpace Y f).toSheafedSpace = toSheafedSpace Y.toSheafedSpace f

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : toLocallyRingedSpace 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.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : LocallyRingedSpace.Hom.toShHom (toLocallyRingedSpaceHom Y f) = CategoryTheory.InducedCategory.homMk f

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_isOpenImmersion {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : LocallyRingedSpace.IsOpenImmersion (toLocallyRingedSpaceHom Y f)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace {X Y : LocallyRingedSpace} (f : X ⟶ Y) [LocallyRingedSpace.IsOpenImmersion f] : toLocallyRingedSpace Y f.toHom = X

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.IsIso (f.c.app (Opposite.op U))

@[instance 100]

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsOpenImmersion f

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Z : SheafedSpace C} (f : X ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Mono f

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Z : SheafedSpace C} (f : X ⟶ Z) [H : IsOpenImmersion f] : PresheafedSpace.IsOpenImmersion (forgetToPresheafedSpace.map f)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp forgetToPresheafedSpace)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan f g).comp forgetToPresheafedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan f g).comp forgetToPresheafedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan g f).comp forgetToPresheafedSpace)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan g f).comp forgetToPresheafedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan g f).comp forgetToPresheafedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetCreatesPullbackOfLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) forgetToPresheafedSpace

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetCreatesPullbackOfRight {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f) forgetToPresheafedSpace

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (forget C)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) (forget C)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasPullback g f

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_snd_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

Open immersions are stable under base-change.

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_fst_of_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X Y : SheafedSpace C} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (PresheafedSpace.Hom.stalkMap f.hom x)] : IsOpenImmersion f

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.

@[reducible, inline]

abbrev AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)

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

noncomputable def AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : X ≅ Y.restrict ⋯

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

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (X✝ : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ) : (isoRestrict f).hom.hom.c.app X✝ = CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.hom).obj (Opposite.unop X✝)))) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (Y.ofRestrict ⋯) = f

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : SheafedSpace C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv f = Y.ofRestrict ⋯

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : SheafedSpace C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h

noncomputable def AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((opensFunctor f).obj U))

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

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (invApp f (Opposite.unop V)) = CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (Y.presheaf.map ((opensFunctor f).op.map i))

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop V))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop V)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (Y.presheaf.map ((opensFunctor f).op.map i))) h

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : CategoryTheory.IsIso (invApp f U)

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : CategoryTheory.inv (invApp f U) = CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op ((opensFunctor f).obj U))) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (invApp f U) (f.hom.c.app (Opposite.op ((opensFunctor f).obj U))) = X.presheaf.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {Z : C} (h : ((TopCat.Presheaf.pushforward C f.hom.base).obj X.presheaf).obj (Opposite.op ((opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (invApp f U) (CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op ((opensFunctor f).obj U))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (f.hom.c.app (Opposite.op ((opensFunctor f).obj U)))) ((CategoryTheory.ConcreteCategory.hom (invApp f U)) x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.hom.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) : CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) {Z : C} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.hom.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : SheafedSpace C) {f : X ⟶ ↑Y.toPresheafedSpace} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (Y.ofRestrict hf)

@[simp]

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : SheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) : invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : SheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (invApp (X.ofRestrict h) U)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U)))) x

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] [h' : CategoryTheory.Epi f.hom.base] : CategoryTheory.IsIso f

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

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : SheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f] [CategoryTheory.Limits.HasColimits C] (x : ↑↑X.toPresheafedSpace) : CategoryTheory.IsIso (PresheafedSpace.Hom.stalkMap f.hom x)

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i).hom.base)

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i j : CategoryTheory.Discrete ι) (h : i ≠ j) (U : TopologicalSpace.Opens ↑↑(F.obj i).toPresheafedSpace) : (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι (F.comp forgetToPresheafedSpace) j).base).obj ((TopologicalSpace.Opens.map (CategoryTheory.preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)) = ⊥

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion_aux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) [CategoryTheory.Limits.HasStrictTerminalObjects C] : IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type w} [Small.{v, w} ι] (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) [CategoryTheory.Limits.HasStrictTerminalObjects C] : IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instOfRestrict (X : LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (X.ofRestrict hf)

@[instance 100]

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso {Y Z : LocallyRingedSpace} (g : Y ⟶ Z) [CategoryTheory.IsIso g] : IsOpenImmersion g

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) [H : IsOpenImmersion f] (g : Z ⟶ Y) [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.mono {X Z : LocallyRingedSpace} (f : X ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Mono f

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace {X Z : LocallyRingedSpace} (f : X ⟶ Z) [H : IsOpenImmersion f] : SheafedSpace.IsOpenImmersion (forgetToSheafedSpace.map f)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PullbackCone f g

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

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (pullbackConeOfLeft f g).snd

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.IsLimit (pullbackConeOfLeft f g)

The constructed pullbackConeOfLeft is indeed limiting.

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasPullback g f

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

Open immersions are stable under base-change.

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_fst_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)

Open immersions are stable under base-change.

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] [IsOpenImmersion g] : IsOpenImmersion (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) forgetToSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (forgetToSheafedSpace.comp SheafedSpace.forgetToPresheafedSpace)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion {X Z : LocallyRingedSpace} (f : X ⟶ Z) [H : IsOpenImmersion f] : PresheafedSpace.IsOpenImmersion ((forgetToSheafedSpace.comp SheafedSpace.forgetToPresheafedSpace).map f)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (forgetToSheafedSpace.comp (SheafedSpace.forget CommRingCat))

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g) forgetToSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) forgetToSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) (forgetToSheafedSpace.comp SheafedSpace.forgetToPresheafedSpace)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan g f) forgetToSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g) (forgetToSheafedSpace.comp SheafedSpace.forgetToPresheafedSpace)

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan g f) (forgetToSheafedSpace.comp SheafedSpace.forgetToPresheafedSpace)

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom 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.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.CategoryStruct.comp (lift f g H') f = g

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac_assoc {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z✝ : LocallyRingedSpace} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift f g H') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (l : Y ⟶ X) (hl : CategoryTheory.CategoryStruct.comp l f = g) : l = lift f g H'

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_range {X Y Z : LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (lift f g H').base) = ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] : X ≅ Y.restrict ⋯

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

@[reducible, inline]

abbrev AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.Functor (TopologicalSpace.Opens ↑X.toTopCat) (TopologicalSpace.Opens ↑Y.toTopCat)

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

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)) [stalk_iso : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (Hom.stalkMap f x)] : IsOpenImmersion f

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.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (Y.ofRestrict ⋯) = f

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : LocallyRingedSpace} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).hom (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv f = Y.ofRestrict ⋯

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] {Z : LocallyRingedSpace} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoRestrict f).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((opensFunctor f).obj U))

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

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑X.toTopCat)ᵒᵖ} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (invApp f (Opposite.unop V)) = CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (Y.presheaf.map ((opensFunctor f).op.map i))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑X.toTopCat)ᵒᵖ} (i : U ⟶ V) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop V))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop V)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (invApp f (Opposite.unop U)) (Y.presheaf.map ((opensFunctor f).op.map i))) h

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) : CategoryTheory.IsIso (invApp f U)

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) : CategoryTheory.inv (invApp f U) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((opensFunctor f).obj U))) (X.presheaf.map (CategoryTheory.eqToHom ⋯))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (invApp f U) (f.c.app (Opposite.op ((opensFunctor f).obj U))) = X.presheaf.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) {Z : CommRingCat} (h : ((TopCat.Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (Opposite.op ((opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (invApp f U) (CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((opensFunctor f).obj U))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) (x : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op ((opensFunctor f).obj U)))) ((CategoryTheory.ConcreteCategory.hom (invApp f U)) x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑Y.toTopCat) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑Y.toTopCat) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app' {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑Y.toTopCat) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : TopologicalSpace.Opens ↑Y.toTopCat) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

A variant of app_inv_app that gives an eqToHom instead of homOfLe.

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict {X : TopCat} (Y : LocallyRingedSpace) {f : X ⟶ ↑Y.toPresheafedSpace} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (Y.ofRestrict hf)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp (X : LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) : invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply (X : LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) (x : ↑((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (invApp (X.ofRestrict h) U)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op (h.functor.obj U))))) x

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] (x : ↑X.toTopCat) : CategoryTheory.IsIso (Hom.stalkMap f x)

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : IsOpenImmersion f] [CategoryTheory.Epi f.base] : CategoryTheory.IsIso f