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.

class AlgebraicGeometry.PresheafedSpace.IsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 : Topology.IsOpenEmbedding ⇑f.base

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

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

  the underlying sheaf morphism is an isomorphism on each open subset

@[reducible, inline]

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

@[reducible, inline]

abbrev AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion {X 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.toHom

@[reducible, inline]

abbrev AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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.opensFunctor f = ⋯.functor

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.PresheafedSpace C} (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} [CategoryTheory.Category.{v, u} C] {X 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.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.

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : 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.opensFunctor f).obj U))) ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U) x) = (X.presheaf.map (CategoryTheory.eqToHom ⋯)) x

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : 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.opensFunctor f).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 f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : 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 f ((TopologicalSpace.Opens.map f.base).obj U)) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : 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.opensFunctor f).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 f ((TopologicalSpace.Opens.map f.base).obj U)) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

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

An isomorphism is an open immersion.

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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 (Y.ofRestrict ⋯) g

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] {X Y 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) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).fst = s.fst

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd = s.snd

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

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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 f g)

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

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

@[simp]

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

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

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] {X Y 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.toSheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] {X 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 = { toHom := 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.LocallyRingedSpace.Hom.toShHom (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f) = 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 Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.toHom = X

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 100]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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.instMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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} [CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] : AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.ConcreteCategory C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑f.base) [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.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.

@[reducible, inline]

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

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

Equations

• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f = ⋯.functor

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

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

Equations

• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f = AlgebraicGeometry.SheafedSpace.isoMk (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.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

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) [H : AlgebraicGeometry.SheafedSpace.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.SheafedSpace.IsOpenImmersion.stalk_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] [CategoryTheory.Limits.HasColimits C] (x : ↑↑X.toPresheafedSpace) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)

Equations

• ⋯ = ⋯

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

@[deprecated AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding]

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

Alias of AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding.

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

instance AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} 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.instOfRestrict (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat) (hf : Topology.IsOpenEmbedding ⇑f) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (X.ofRestrict hf)

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp {X Y 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 Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace {X 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 Y 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.instSndPullbackConeOfLeft {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd

Equations

• ⋯ = ⋯

def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit {X Y 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 Y 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 Y 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 Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

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

Open immersions are stable under base-change.

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion {X Y 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.forget_preservesPullbackOfLeft {X Y 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

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left {X Y 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.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = H

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left {X Y 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.comp (AlgebraicGeometry.SheafedSpace.forget CommRingCat))

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left {X Y 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

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right {X Y 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

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right {X Y 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.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right {X Y 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

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left {X Y 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.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right {X Y 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.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)

Equations

• ⋯ = ⋯

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

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

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

@[simp]

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

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

theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (H' : Set.range ⇑g.base ⊆ Set.range ⇑f.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 Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (H' : Set.range ⇑g.base ⊆ Set.range ⇑f.base) : Set.range ⇑(AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H').base = ⇑f.base ⁻¹' Set.range ⇑g.base

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

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.

@[reducible, inline]

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

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

Equations

• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f = ⋯.functor

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑X.toTopCat) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.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

• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f.toHom U

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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