Open immersions of schemes

@[reducible, inline]

abbrev AlgebraicGeometry.IsOpenImmersion : CategoryTheory.MorphismProperty Scheme

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

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

def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme (X : LocallyRingedSpace) (h : ∀ (x : ↑X.toTopCat), ∃ (R : CommRingCat) (f : Spec.toLocallyRingedSpace.obj (Opposite.op R) ⟶ X), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ∧ IsOpenImmersion f) : Scheme

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

theorem AlgebraicGeometry.IsOpenImmersion.isOpen_range {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : IsOpen (Set.range ⇑f)

theorem AlgebraicGeometry.Scheme.Hom.isOpenEmbedding {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : Topology.IsOpenEmbedding ⇑f

def AlgebraicGeometry.Scheme.Hom.opensRange {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : Y.Opens

The image of an open immersion as an open set.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_opensRange {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : ↑(opensRange f) = Set.range ⇑f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.mem_opensRange {X Y : Scheme} {f : X ⟶ Y} [IsOpenImmersion f] {y : ↥Y} : y ∈ opensRange f ↔ ∃ (x : ↥X), f x = y

def AlgebraicGeometry.Scheme.Hom.opensFunctor {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : CategoryTheory.Functor X.Opens Y.Opens

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

def AlgebraicGeometry.«term_''ᵁ_» : Lean.TrailingParserDescr

f ''ᵁ U is notation for the image (as an open set) of U under an open immersion f. The preferred name in lemmas is image and it should be treated as an infix.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_image {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U : X.Opens} : ↑((opensFunctor f).obj U) = ⇑f '' ↑U

theorem AlgebraicGeometry.Scheme.Hom.image_mono {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V) : (opensFunctor f).obj U ≤ (opensFunctor f).obj V

@[deprecated AlgebraicGeometry.Scheme.Hom.image_mono (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Hom.image_le_image_of_le {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V) : (opensFunctor f).obj U ≤ (opensFunctor f).obj V

Alias of AlgebraicGeometry.Scheme.Hom.image_mono.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V) : (opensFunctor f).map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯

instance AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : (opensFunctor f).IsContinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : (opensFunctor f).obj ⊤ = opensRange f

theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] : opensRange (CategoryTheory.CategoryStruct.comp f g) = (opensFunctor g).obj (opensRange f)

theorem AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : opensRange f = ⊤

theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [IsOpenImmersion g] : opensRange (CategoryTheory.CategoryStruct.comp f g) = opensRange g

theorem AlgebraicGeometry.Scheme.Hom.image_le_opensRange {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : (opensFunctor f).obj U ≤ opensRange f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : (TopologicalSpace.Opens.map f.base).obj ((opensFunctor f).obj U) = U

theorem AlgebraicGeometry.Scheme.Hom.image_le_image_iff {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U U' : X.Opens) : (opensFunctor f).obj U ≤ (opensFunctor f).obj U' ↔ U ≤ U'

theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) : (opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U) = opensRange f ⊓ U

@[deprecated AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) : (opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U) = opensRange f ⊓ U

Alias of AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf.

theorem AlgebraicGeometry.Scheme.Hom.image_preimage_le {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) : (opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U) ≤ U

theorem AlgebraicGeometry.Scheme.Hom.image_injective {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : Function.Injective fun (x : X.Opens) => (opensFunctor f).obj x

theorem AlgebraicGeometry.Scheme.Hom.image_iSup {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {ι : Sort u_1} (s : ι → X.Opens) : (opensFunctor f).obj (⨆ (i : ι), s i) = ⨆ (i : ι), (opensFunctor f).obj (s i)

theorem AlgebraicGeometry.Scheme.Hom.image_iSup₂ {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {ι : Sort u_1} {κ : ι → Sort u_2} (s : (i : ι) → κ i → X.Opens) : (opensFunctor f).obj (⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), (opensFunctor f).obj (s i j)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_image {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : X.Opens) [IsOpenImmersion f] [IsOpenImmersion g] : (opensFunctor (CategoryTheory.CategoryStruct.comp f g)).obj U = (opensFunctor g).obj ((opensFunctor f).obj U)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.id_image {X : Scheme} (U : X.Opens) : (opensFunctor (CategoryTheory.CategoryStruct.id X)).obj U = U

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inv_image {X Y : Scheme} (e : X ≅ Y) (U : Y.Opens) : (opensFunctor e.inv).obj U = (TopologicalSpace.Opens.map e.hom.base).obj U

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U : X.Opens} {x : ↥X} : f x ∈ (opensFunctor f).obj U ↔ x ∈ U

@[deprecated AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Hom.map_mem_image_iff {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U : X.Opens} {x : ↥X} : f x ∈ (opensFunctor f).obj U ↔ x ∈ U

Alias of AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_opensRange {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (TopologicalSpace.Opens.map f.base).obj (opensRange f) = ⊤

instance AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : CategoryTheory.IsIso (app f ((opensFunctor f).obj U))

theorem AlgebraicGeometry.Scheme.Hom.isIso_app {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (V : Y.Opens) (hV : V ≤ opensRange f) : CategoryTheory.IsIso (app f V)

def AlgebraicGeometry.Scheme.Hom.appIso {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj U)) ≅ X.presheaf.obj (Opposite.op U)

The isomorphism Γ(Y, f(U)) ≅ Γ(X, U) induced by an open immersion f : X ⟶ Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (appIso f V).inv = CategoryTheory.CategoryStruct.comp (appIso f U).inv (Y.presheaf.map ((opensFunctor f).op.map i))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (appIso f V).inv h) = CategoryTheory.CategoryStruct.comp (appIso f U).inv (CategoryTheory.CategoryStruct.comp (Y.presheaf.map ((opensFunctor f).op.map i)) h)

theorem AlgebraicGeometry.Scheme.Hom.appIso_hom {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : (appIso f U).hom = CategoryTheory.CategoryStruct.comp (app f ((opensFunctor f).obj U)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

theorem AlgebraicGeometry.Scheme.Hom.appIso_hom' {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : (appIso f U).hom = appLE f ((opensFunctor f).obj U) U ⋯

A variant of appIso_hom that uses Hom.appLE.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (app f U) (appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (app f U) (CategoryTheory.CategoryStruct.comp (appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.app_invApp' {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ opensRange f) : CategoryTheory.CategoryStruct.comp (app f U) (appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

A variant of app_invApp that gives an eqToHom instead of homOfLE.

theorem AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ opensRange f) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (app f U) (CategoryTheory.CategoryStruct.comp (appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

A variant of app_invApp that gives an eqToHom instead of homOfLE.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : CategoryTheory.CategoryStruct.comp (appIso f U).inv (app f ((opensFunctor f).obj U)) = X.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ((opensFunctor f).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (appIso f U).inv (CategoryTheory.CategoryStruct.comp (app f ((opensFunctor f).obj U)) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) (x : ↑(X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (app f ((opensFunctor f).obj U))) ((CategoryTheory.ConcreteCategory.hom (appIso f U).inv) x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (appLE f U V e) (appIso f V).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (appLE f U V e) (CategoryTheory.CategoryStruct.comp (appIso f V).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (appIso f V).inv) ((CategoryTheory.ConcreteCategory.hom (appLE f U V e)) x) = (CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((opensFunctor f).obj U)) : CategoryTheory.CategoryStruct.comp (appIso f U).inv (appLE f ((opensFunctor f).obj U) V e) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {U V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((opensFunctor f).obj U)) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (appIso f U).inv (CategoryTheory.CategoryStruct.comp (appLE f ((opensFunctor f).obj U) V e) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : X.Opens) : CategoryTheory.CategoryStruct.comp (appIso f U).inv (CategoryTheory.CategoryStruct.comp (app f ((opensFunctor f).obj U)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.id_appIso {X : Scheme} (U : X.Opens) : appIso (CategoryTheory.CategoryStruct.id X) U = CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_appIso {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] (U : X.Opens) : appIso (CategoryTheory.CategoryStruct.comp f g) U = CategoryTheory.Functor.mapIso Z.presheaf (CategoryTheory.eqToIso ⋯).op ≪≫ appIso g ((opensFunctor f).obj U) ≪≫ appIso f U

def AlgebraicGeometry.IsOpenImmersion.opensEquiv {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : X.Opens ≃ { U : Y.Opens // U ≤ Scheme.Hom.opensRange f }

The open sets of an open subscheme corresponds to the open sets containing in the image.

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : { U : Y.Opens // U ≤ Scheme.Hom.opensRange f }) : (opensEquiv f).symm U = (TopologicalSpace.Opens.map f.base).obj ↑U

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : ↑((opensEquiv f) U) = (Scheme.Hom.opensFunctor f).obj U

instance AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway {R : CommRingCat} (f : ↑R) : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

@[deprecated AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.basic_open_isOpenImmersion {R : CommRingCat} (f : ↑R) : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Alias of AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway.

instance AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap {R : Type u_1} [CommRing R] (f : R) : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

theorem AlgebraicGeometry.IsOpenImmersion.of_isLocalization {R S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (f : R) [IsLocalization.Away f S] : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))

theorem AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset {X : Scheme} {x : ↥X} {U : X.Opens} (hxU : x ∈ U) : ∃ (R : CommRingCat) (f : Spec R ⟶ X), IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

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

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace {X : PresheafedSpace CommRingCat} (Y : Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toScheme Y f).toLocallyRingedSpace = toLocallyRingedSpace Y.toLocallyRingedSpace f

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom {X : PresheafedSpace CommRingCat} (Y : Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : toScheme Y f ⟶ Y

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom {X : PresheafedSpace CommRingCat} (Y : Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : (toSchemeHom Y f).toPshHom = f

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion {X : PresheafedSpace CommRingCat} (Y : Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f] : AlgebraicGeometry.IsOpenImmersion (toSchemeHom Y f)

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq {X Y : Scheme} (H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace) : X = Y

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme {X Y : Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : toScheme Y f.toPshHom = X

def AlgebraicGeometry.Scheme.restrict {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : Scheme

The restriction of a Scheme along an open embedding.

theorem AlgebraicGeometry.Scheme.restrict_carrier {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h).toPresheafedSpace = U

@[simp]

theorem AlgebraicGeometry.Scheme.restrict_presheaf_obj {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (X.restrict h).presheaf.obj X✝ = X.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop X✝)))

theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.restrict h).toPresheafedSpace = X.restrict h

def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X

The canonical map from the restriction to the subspace.

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (Hom.toLRSHom (X.ofRestrict h)).base = f

theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↥X)ᵒᵖ) : (Hom.toLRSHom (X.ofRestrict h)).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_app {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) : Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op

instance AlgebraicGeometry.IsOpenImmersion.ofRestrict {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (X.ofRestrict h)

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_appLE {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) (W : (X.restrict h).Opens) (e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V) : Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_appIso {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U✝ : (X.restrict h).Opens) : Hom.appIso (X.ofRestrict h) U✝ = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((Hom.opensFunctor (X.ofRestrict h)).obj U✝)))

@[simp]

theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : Scheme) {f : U ⟶ { carrier := ↥X, str := X.instTopologicalSpaceCarrierCarrier }} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ) (i : V ⟶ W) : (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[instance 100]

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

theorem AlgebraicGeometry.IsOpenImmersion.isIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] [CategoryTheory.Epi f.base] : CategoryTheory.IsIso f

@[deprecated AlgebraicGeometry.IsOpenImmersion.isIso (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.IsOpenImmersion.isIso.

theorem AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap {X Y : Scheme} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑f) [∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)] : IsOpenImmersion f

@[deprecated AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.of_stalk_iso {X Y : Scheme} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑f) [∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)] : IsOpenImmersion f

Alias of AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap.

instance AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) : CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

theorem AlgebraicGeometry.IsOpenImmersion.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g] [IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)] : IsOpenImmersion f

instance AlgebraicGeometry.IsOpenImmersion.instHasOfPostcompPropertyScheme : IsOpenImmersion.HasOfPostcompProperty IsOpenImmersion

theorem AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap {X Y : Scheme} {f : X ⟶ Y} : IsOpenImmersion f ↔ Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

@[deprecated AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso {X Y : Scheme} {f : X ⟶ Y} : IsOpenImmersion f ↔ Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

Alias of AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap.

theorem AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ IsOpenImmersion f ∧ CategoryTheory.Epi f.base

@[deprecated AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base (since := "2025-10-07")]

theorem AlgebraicGeometry.isIso_iff_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ IsOpenImmersion f ∧ CategoryTheory.Epi f.base

Alias of AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base.

theorem AlgebraicGeometry.isIso_iff_isIso_stalkMap {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.base ∧ ∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

@[deprecated AlgebraicGeometry.isIso_iff_isIso_stalkMap (since := "2025-10-07")]

theorem AlgebraicGeometry.isIso_iff_stalk_iso {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.base ∧ ∀ (x : ↥X), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)

Alias of AlgebraicGeometry.isIso_iff_isIso_stalkMap.

def AlgebraicGeometry.IsOpenImmersion.isoRestrict {X Z : Scheme} (f : X ⟶ Z) [H : IsOpenImmersion f] : X ≅ Z.restrict ⋯

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

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

theorem AlgebraicGeometry.IsOpenImmersion.le_monomorphisms : IsOpenImmersion ≤ CategoryTheory.MorphismProperty.monomorphisms Scheme

instance AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace {X Z : Scheme} (f : X ⟶ Z) [H : IsOpenImmersion f] : LocallyRingedSpace.IsOpenImmersion (Scheme.forgetToLocallyRingedSpace.map f)

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp Scheme.forgetToLocallyRingedSpace)

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left' {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan f g).comp Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan f g).comp Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan g f).comp Scheme.forgetToLocallyRingedSpace)

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right' {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan g f).comp Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan g f).comp Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

instance AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfLeft {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) Scheme.forgetToLocallyRingedSpace

instance AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfRight {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f) Scheme.forgetToLocallyRingedSpace

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) Scheme.forgetToLocallyRingedSpace

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1 {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) Scheme.forgetToLocallyRingedSpace

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

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

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

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

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

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) Scheme.forgetToTop

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) Scheme.forgetToTop

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) Scheme.forget

instance AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1 {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) Scheme.forget

theorem AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) = ↑((TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f))

@[deprecated AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) = ↑((TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f))

Alias of AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd.

theorem AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : opensRange (CategoryTheory.Limits.pullback.snd f g) = (TopologicalSpace.Opens.map g.base).obj (opensRange f)

@[deprecated AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.snd f g) = (TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f)

Alias of AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd.

theorem AlgebraicGeometry.IsOpenImmersion.range_pullbackFst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.Limits.pullback.fst g f) = ↑((TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f))

@[deprecated AlgebraicGeometry.IsOpenImmersion.range_pullbackFst (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.Limits.pullback.fst g f) = ↑((TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f))

Alias of AlgebraicGeometry.IsOpenImmersion.range_pullbackFst.

theorem AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : opensRange (CategoryTheory.Limits.pullback.fst g f) = (TopologicalSpace.Opens.map g.base).obj (opensRange f)

@[deprecated AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.fst g f) = (TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f)

Alias of AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst.

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f) = Set.range ⇑f ∩ Set.range ⇑g

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) g) = Set.range ⇑g ∩ Set.range ⇑f

theorem AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback {X Y U V : Scheme} {f : X ⟶ Y} {f' : U ⟶ V} {iU : U ⟶ X} {iV : V ⟶ Y} [IsOpenImmersion iV] [IsOpenImmersion iU] (H : CategoryTheory.IsPullback f' iU iV f) (W : V.Opens) : (Scheme.Hom.opensFunctor iU).obj ((TopologicalSpace.Opens.map f'.base).obj W) = (TopologicalSpace.Opens.map f.base).obj ((Scheme.Hom.opensFunctor iV).obj W)

def AlgebraicGeometry.IsOpenImmersion.lift {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑g ⊆ Set.range ⇑f) : Y ⟶ X

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

@[simp]

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

@[simp]

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

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

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

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

theorem AlgebraicGeometry.IsOpenImmersion.isPullback_lift_id {X U Y : Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [IsOpenImmersion g] (H : Set.range ⇑f ⊆ Set.range ⇑g) : CategoryTheory.IsPullback (lift g f H) (CategoryTheory.CategoryStruct.id X) g f

def AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) : X ≅ Y

Two open immersions with equal range are isomorphic.

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) : CategoryTheory.CategoryStruct.comp (isoOfRangeEq f g e).hom g = f

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assoc {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) {Z✝ : Scheme} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (isoOfRangeEq f g e).hom (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) : CategoryTheory.CategoryStruct.comp (isoOfRangeEq f g e).inv f = g

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) {Z✝ : Scheme} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (isoOfRangeEq f g e).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux {X Y U : Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : IsOpenImmersion g] (V : U.Opens) : (TopologicalSpace.Opens.map f.base).obj V = (TopologicalSpace.Opens.map fg.base).obj ((Scheme.Hom.opensFunctor g).obj V)

theorem AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq {X Y U : Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : IsOpenImmersion g] (V : U.Opens) : Scheme.Hom.app f V = CategoryTheory.CategoryStruct.comp (Scheme.Hom.appIso g V).inv (CategoryTheory.CategoryStruct.comp (Scheme.Hom.app fg ((Scheme.Hom.opensFunctor g).obj V)) (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op))

The fg argument is to avoid nasty stuff about dependent types.

theorem AlgebraicGeometry.IsOpenImmersion.lift_app {X Y U : Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [IsOpenImmersion f] (H : Set.range ⇑g ⊆ Set.range ⇑f) (V : U.Opens) : Scheme.Hom.app (lift f g H) V = CategoryTheory.CategoryStruct.comp (Scheme.Hom.appIso f V).inv (CategoryTheory.CategoryStruct.comp (Scheme.Hom.app g ((Scheme.Hom.opensFunctor f).obj V)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

theorem AlgebraicGeometry.IsOpenImmersion.isPullback {U V X Y : Scheme} (g : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) (f : X ⟶ Y) [IsOpenImmersion iU] [IsOpenImmersion iV] (H : CategoryTheory.CategoryStruct.comp iU f = CategoryTheory.CategoryStruct.comp g iV) (H' : (TopologicalSpace.Opens.map f.base).obj (Scheme.Hom.opensRange iV) = Scheme.Hom.opensRange iU) : CategoryTheory.IsPullback g iU iV f

noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ≅ Y.presheaf.obj (Opposite.op (Scheme.Hom.opensRange f ⊓ U))

If f is an open immersion X ⟶ Y, the global sections of X are naturally isomorphic to the sections of Y over the image of f.

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_inv {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : (ΓIso f U).inv = Scheme.Hom.appLE f (Scheme.Hom.opensRange f ⊓ U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) (ΓIso f U).inv = Scheme.Hom.app f U

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) (CategoryTheory.CategoryStruct.comp (ΓIso f U).inv h) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f U) h

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) (x : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appLE f (Scheme.Hom.opensRange f ⊓ U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f U)) x

theorem AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f U) (ΓIso f U).hom = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (Scheme.Hom.opensRange f ⊓ U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f U) (CategoryTheory.CategoryStruct.comp (ΓIso f U).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) (x : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (ΓIso f U).hom) ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f U)) x) = (CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x

@[deprecated AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom (since := "2025-10-07")]

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f U) (ΓIso f U).hom = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

Alias of AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom.

noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIsoTop {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : X.presheaf.obj (Opposite.op ⊤) ≅ Y.presheaf.obj (Opposite.op (Scheme.Hom.opensRange f))

Given an open immersion f : U ⟶ X, the isomorphism between global sections of U and the sections of X at the image of f.

instance AlgebraicGeometry.IsOpenImmersion.instLift {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] (H' : Set.range ⇑g ⊆ Set.range ⇑f) [IsOpenImmersion g] : IsOpenImmersion (lift f g H')

theorem AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (hf : Scheme.Hom.opensRange f = ⊤) : CategoryTheory.IsIso f

instance AlgebraicGeometry.isOpenImmersion_isStableUnderComposition : IsOpenImmersion.IsStableUnderComposition

instance AlgebraicGeometry.isOpenImmersion_respectsIso : IsOpenImmersion.RespectsIso

instance AlgebraicGeometry.isOpenImmersion_isMultiplicative : IsOpenImmersion.IsMultiplicative

instance AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange : IsOpenImmersion.IsStableUnderBaseChange

theorem AlgebraicGeometry.Scheme.image_basicOpen {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) : (Hom.opensFunctor f).obj (X.basicOpen r) = Y.basicOpen ((CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).inv) r)

theorem AlgebraicGeometry.Scheme.image_zeroLocus {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑f '' X.zeroLocus s = Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f

noncomputable def AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [IsOpenImmersion g] (p : ↥P) (x : ↥X := fst p) (hx : fst p = x := by cat_disch) : CategoryTheory.Arrow.mk (Hom.stalkMap f x) ≅ CategoryTheory.Arrow.mk (Hom.stalkMap snd p)

If

  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

is a pullback square and g is an open immersion, then the stalk map induced by snd at p is isomorphic to the stalk map of f at fst p.