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 though 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 to_SheafedSpace_hom.
• 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 to_LocallyRingedSpace_hom.

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 An (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_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.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 : OpenEmbedding ⇑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 ((IsOpenMap.functor ⋯).obj U)))

  the underlying sheaf morphism is an isomorphism on each open subset

@[inline, reducible]

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

Equations

• AlgebraicGeometry.SheafedSpace.IsOpenImmersion f = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f

@[inline, reducible]

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

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

Equations

• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f = AlgebraicGeometry.SheafedSpace.IsOpenImmersion f.val

@[inline, reducible]

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

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

Equations

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H = IsOpenMap.functor ⋯

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

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

The composition of two open immersions is an open immersion.

Equations

• ⋯ = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoObjOppositeOpensαTopologicalSpaceCarrierTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorPresheafOpObjToPrefunctorOpenFunctorInvApp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑X) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp H U)

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑X) {Z : C} (h : (f.base _* X.presheaf).obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp H U) (CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H).obj U))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑X) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (X.presheaf.obj (Opposite.op U))) : (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H).obj U))) ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp H U) x) = (X.presheaf.map (CategoryTheory.eqToHom ⋯)) x

@[simp]

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

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

@[simp]

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

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑Y) (hU : ↑U ⊆ Set.range ⇑f.base) : CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp H ((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.

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

An isomorphism is an open immersion.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (Y : AlgebraicGeometry.PresheafedSpace C) {f : X ⟶ ↑Y} (hf : OpenEmbedding ⇑f) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (AlgebraicGeometry.PresheafedSpace.ofRestrict Y hf)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : OpenEmbedding ⇑f) (U : TopologicalSpace.Opens ↑↑(AlgebraicGeometry.PresheafedSpace.restrict X h)) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj ((AlgebraicGeometry.PresheafedSpace.restrict X h).presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) x = x

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : OpenEmbedding ⇑f) (U : TopologicalSpace.Opens ↑↑(AlgebraicGeometry.PresheafedSpace.restrict X h)) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U = CategoryTheory.CategoryStruct.id ((AlgebraicGeometry.PresheafedSpace.restrict X h).presheaf.obj (Opposite.op U))

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) [h : AlgebraicGeometry.PresheafedSpace.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_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} [CategoryTheory.Limits.HasColimits C] [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (x : ↑↑X) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f x)

Equations

• ⋯ = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• ⋯ = ⋯

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

The constructed pullback cone is indeed the pullback.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forgetPreservesLimitsOfRight f g = CategoryTheory.Limits.preservesPullbackSymmetry (AlgebraicGeometry.PresheafedSpace.forget C) f g

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

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z) [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion 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

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv CategoryTheory.Limits.pullback.snd) CategoryTheory.Limits.pullback.fst

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

Two open immersions with equal range is isomorphic.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f = { toPresheafedSpace := X, IsSheaf := ⋯ }

@[simp]

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

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

Equations

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f = f

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = H

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f = { val := f, prop := ⋯ }

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.LocallyRingedSpace) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f).val = f

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

Equations

• ⋯ = H

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instMonoSheafedSpaceInstCategorySheafedSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.SheafedSpace C} {Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpaceForgetPreservesOfRight f g = CategoryTheory.Limits.preservesPullbackSymmetry (AlgebraicGeometry.SheafedSpace.forget C) f g

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Functor.ReflectsIsomorphisms (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X : AlgebraicGeometry.SheafedSpace C} {Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) (hf : OpenEmbedding ⇑f.base) [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f x)] : AlgebraicGeometry.SheafedSpace.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.

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_openEmbedding {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) : OpenEmbedding ⇑(CategoryTheory.Limits.colimit.ι F i).base

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = H

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

The constructed pullbackConeOfLeft is indeed limiting.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = H

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} {Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion 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

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.