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 ⇑(CategoryTheory.ConcreteCategory.hom f.base))

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

def AlgebraicGeometry.Scheme.Hom.opensRange {X Y : Scheme} (f : X.Hom 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.Hom Y) [H : IsOpenImmersion f] : ↑f.opensRange = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.opensFunctor {X Y : Scheme} (f : X.Hom 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_''ᵁ_».«delab_app.CategoryTheory.Functor.obj» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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

f ''ᵁ U is notation for the image (as an open set) of U under an open immersion f.

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) : (TopologicalSpace.Opens.map f.base).obj (f.opensFunctor.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_inter {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) : f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U) = f.opensRange ⊓ U

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

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

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

@[simp]

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

@[simp]

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

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

def AlgebraicGeometry.Scheme.Hom.appIso {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) : Y.presheaf.obj (Opposite.op (f.opensFunctor.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.Hom Y) [H : IsOpenImmersion f] {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (f.appIso V).inv = CategoryTheory.CategoryStruct.comp (f.appIso U).inv (Y.presheaf.map (f.opensFunctor.op.map i))

@[simp]

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

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((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.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.app U) (CategoryTheory.CategoryStruct.comp (f.appIso ((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.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ f.opensRange) : CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((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.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ f.opensRange) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.app U) (CategoryTheory.CategoryStruct.comp (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj (f.opensFunctor.obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.appIso U).inv (CategoryTheory.CategoryStruct.comp (f.app (f.opensFunctor.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.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) (x : CategoryTheory.ToType (X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (f.app (f.opensFunctor.obj U))) ((CategoryTheory.ConcreteCategory.hom (f.appIso U).inv) x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) x

@[deprecated AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply (since := "2025-02-11")]

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

Alias of AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply.

@[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 : CategoryTheory.ToType (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

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.basic_open_isOpenImmersion {R : CommRingCat} (f : ↑R) : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) ∧ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⊆ ↑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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.restrict h).toPresheafedSpace = X.restrict h

def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : Scheme) {f : U ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : IsOpenImmersion (X.ofRestrict h)

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_appLE {U : TopCat} (X : Scheme) {f : U ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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 ⟶ TopCat.of ↥X} (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.to_iso {X Y : Scheme} (f : X ⟶ Y) [h : IsOpenImmersion f] [CategoryTheory.Epi f.base] : CategoryTheory.IsIso f

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

instance AlgebraicGeometry.IsOpenImmersion.stalk_iso {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

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

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

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)

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.forget_map_isOpenImmersion {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.forget_preservesOfLeft {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.forget_preservesOfRight {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.pullback_snd_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)

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

instance AlgebraicGeometry.IsOpenImmersion.pullback_to_base {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.forgetToTop_preserves_of_left {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.forgetToTop_preserves_of_right {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_pullback_snd_of_left {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g).base) = ((TopologicalSpace.Opens.map g.base).obj (Scheme.Hom.opensRange f)).carrier

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)

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst g f).base) = ((TopologicalSpace.Opens.map g.base).obj { carrier := Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

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)

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.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f).base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

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.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) g).base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)

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 ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : Y ⟶ X

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] (H' : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z✝ : 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 ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (l : Y ⟶ X) (hl : CategoryTheory.CategoryStruct.comp l f = g) : l = lift f g H'

theorem AlgebraicGeometry.IsOpenImmersion.comp_lift {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : IsOpenImmersion f] {Y' : Scheme} (g' : Y' ⟶ Y) (H✝ : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : 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 ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : 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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : 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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : 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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) {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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) : 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 ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) {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 ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (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))

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 : CategoryTheory.ToType (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.ΓIso_hom_map {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.ΓIso_hom_map_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.ΓIso_hom_map_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) (x : CategoryTheory.ToType (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

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 ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) [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))) : ⇑(CategoryTheory.ConcreteCategory.hom f.base) '' X.zeroLocus s = Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)