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 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 An (topological) open embedding between two sheafed spaces is an open immersion if all the stalk maps are isomorphisms.

source

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

Instances

source

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

Equations

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

source

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

Equations

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f = AlgebraicGeometry.SheafedSpace.IsOpenImmersion f.toHom

source

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

Equations

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f = ⋯.functor

source

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

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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

Equations

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

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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 : CategoryTheory.ToType (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) = (X.presheaf.map (CategoryTheory.eqToHom ⋯)) x

source

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

source

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

source

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.

source

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

source

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.

source

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

source

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)

source

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp {C : Type u_1} [CategoryTheory.Category.{u_2, 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))

source

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, 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 : CategoryTheory.ToType ((X.restrict h).presheaf.obj (Opposite.op U))) :

(CategoryTheory.ConcreteCategory.hom (invApp (X.ofRestrict h) U)) x = (CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op (⋯.functor.obj U)))) x

source

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.

source

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)

source

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.

Equations

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

source

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

source

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

Equations

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

source

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.

Equations

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

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

source

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.

source

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)

source

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)

source

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)

source

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)

source

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.

Equations

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

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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.

Equations

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

source

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

source

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.

Equations

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f = f

source

@[simp]

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).base = f.base

source

@[simp]

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).c = f.c

source

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)

source

@[simp]

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

toSheafedSpace Y f = X

source

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.

Equations

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

source

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

source

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.

Equations

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

source

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

source

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

LocallyRingedSpace.IsOpenImmersion (toLocallyRingedSpaceHom Y f)

source

@[simp]

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

toLocallyRingedSpace Y f.toHom = X

source

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

source

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

source

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)

source

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

source

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)

source

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)

source

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

source

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)

source

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

source

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

Equations

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

source

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

Equations

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

source

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)

source

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)

source

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

source

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

source

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.

source

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)

source

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)

source

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.base)) [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (PresheafedSpace.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.

source

@[reducible, inline]