Restriction of Schemes and Morphisms

Main definition

• AlgebraicGeometry.Scheme.restrict: The restriction of a scheme along an open embedding. The map X.restrict f ⟶ X is AlgebraicGeometry.Scheme.ofRestrict. U : X.Opens has a coercion to Scheme and U.ι is a shorthand for X.restrict U.open_embedding : U ⟶ X.
• AlgebraicGeometry.morphismRestrict: The restriction of X ⟶ Y to X ∣_ᵤ f ⁻¹ᵁ U ⟶ Y ∣_ᵤ U.

def AlgebraicGeometry.Scheme.Opens.toScheme {X : Scheme} (U : X.Opens) : Scheme

Open subset of a scheme as a scheme.

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.Opens.instCoeOut {X : Scheme} : CoeOut X.Opens Scheme

def AlgebraicGeometry.Scheme.Opens.ι {X : Scheme} (U : X.Opens) : ↑U ⟶ X

The restriction of a scheme to an open subset.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_apply {X : Scheme} (U : X.Opens) (x : ↥U) : U.ι x = ↑x

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

theorem AlgebraicGeometry.Scheme.Opens.ι_base_apply {X : Scheme} (U : X.Opens) (x : ↥U) : U.ι x = ↑x

Alias of AlgebraicGeometry.Scheme.Opens.ι_apply.

instance AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι {X : Scheme} (U : X.Opens) : IsOpenImmersion U.ι

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.Opens.instCanonicallyOverToScheme {X : Scheme} (U : X.Opens) : (↑U).CanonicallyOver X

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.over_def {X : Scheme} (U : X.Opens) : ↑U ↘ X = U.ι

instance AlgebraicGeometry.Scheme.Opens.instIsOverι {X : Scheme} (U : X.Opens) : Hom.IsOver U.ι X

theorem AlgebraicGeometry.Scheme.Opens.toScheme_carrier {X : Scheme} (U : X.Opens) : ↥↑U = ↑↑U

theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj {X : Scheme} (U : X.Opens) (V : (↑U).Opens) : (↑U).presheaf.obj (Opposite.op V) = X.presheaf.obj (Opposite.op ((Hom.opensFunctor U.ι).obj V))

theorem AlgebraicGeometry.Scheme.Opens.forall_toScheme {X : Scheme} {U : X.Opens} {P : ↥↑U → Prop} : (∀ (x : ↥↑U), P x) ↔ ∀ (x : ↥X) (hx : x ∈ U), P ⟨x, hx⟩

theorem AlgebraicGeometry.Scheme.Opens.exists_toScheme {X : Scheme} {U : X.Opens} {P : ↥↑U → Prop} : (∃ (x : ↥↑U), P x) ↔ ∃ (x : ↥X) (hx : x ∈ U), P ⟨x, hx⟩

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map {X : Scheme} (U : X.Opens) {V W : (TopologicalSpace.Opens ↥↑U)ᵒᵖ} (i : V ⟶ W) : (↑U).presheaf.map i = X.presheaf.map ((Hom.opensFunctor U.ι).map i.unop).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_app {X : Scheme} (U V : X.Opens) : Hom.app U.ι V = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_appTop {X : Scheme} (U : X.Opens) : Hom.appTop U.ι = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_appLE {X : Scheme} (U V : X.Opens) (W : (↑U).Opens) (e : W ≤ (TopologicalSpace.Opens.map U.ι.base).obj V) : Hom.appLE U.ι V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_appIso {X : Scheme} (U : X.Opens) (V : (↑U).Opens) : Hom.appIso U.ι V = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((Hom.opensFunctor U.ι).obj V)))

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.opensRange_ι {X : Scheme} (U : X.Opens) : Hom.opensRange U.ι = U

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.range_ι {X : Scheme} (U : X.Opens) : Set.range ⇑U.ι = ↑U

theorem AlgebraicGeometry.Scheme.Opens.ι_image_top {X : Scheme} (U : X.Opens) : (Hom.opensFunctor U.ι).obj ⊤ = U

theorem AlgebraicGeometry.Scheme.Opens.ι_image_le {X : Scheme} (U : X.Opens) (W : (↑U).Opens) : (Hom.opensFunctor U.ι).obj W ≤ U

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_preimage_self {X : Scheme} (U : X.Opens) : (TopologicalSpace.Opens.map U.ι.base).obj U = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff {X : Scheme} (U : X.Opens) {x : ↥U} {V : (↑U).Opens} : ↑x ∈ (Hom.opensFunctor U.ι).obj V ↔ x ∈ V

instance AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme {X : Scheme} (U : X.Opens) : CategoryTheory.IsIso (Hom.appLE U.ι U ⊤ ⋯)

theorem AlgebraicGeometry.Scheme.Opens.ι_app_self {X : Scheme} (U : X.Opens) : Hom.app U.ι U = X.presheaf.map (CategoryTheory.eqToHom ⋯).op

theorem AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom {X : Scheme} (U : X.Opens) {V W : (↑U).Opens} (e : (Hom.opensFunctor U.ι).obj V = (Hom.opensFunctor U.ι).obj W) : X.presheaf.map (CategoryTheory.eqToHom e).op = (↑U).presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.nonempty_iff {X : Scheme} (U : X.Opens) : Nonempty ↥↑U ↔ (↑U).Nonempty

def AlgebraicGeometry.Scheme.Opens.topIso {X : Scheme} (U : X.Opens) : (↑U).presheaf.obj (Opposite.op ⊤) ≅ X.presheaf.obj (Opposite.op U)

The global sections of the restriction is isomorphic to the sections on the open set.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.topIso_inv {X : Scheme} (U : X.Opens) : U.topIso.inv = X.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.topIso_hom {X : Scheme} (U : X.Opens) : U.topIso.hom = X.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Opens.stalkIso {X : Scheme} (U : X.Opens) (x : ↥U) : (↑U).presheaf.stalk x ≅ X.presheaf.stalk ↑x

The stalks of an open subscheme are isomorphic to the stalks of the original scheme.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom {X : Scheme} (U : X.Opens) {V : (↑U).Opens} (x : ↥U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) (U.stalkIso x).hom = X.presheaf.germ ((Hom.opensFunctor U.ι).obj V) ↑x ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc {X : Scheme} (U : X.Opens) {V : (↑U).Opens} (x : ↥U) (hx : x ∈ V) {Z : CommRingCat} (h : X.presheaf.stalk ↑x ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) (CategoryTheory.CategoryStruct.comp (U.stalkIso x).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((Hom.opensFunctor U.ι).obj V) ↑x ⋯) h

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv {X : Scheme} (U : X.Opens) (V : (↑U).Opens) (x : ↥U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((Hom.opensFunctor U.ι).obj V) ↑x ⋯) (U.stalkIso x).inv = (↑U).presheaf.germ V x hx

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc {X : Scheme} (U : X.Opens) (V : (↑U).Opens) (x : ↥U) (hx : x ∈ V) {Z : CommRingCat} (h : (↑U).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((Hom.opensFunctor U.ι).obj V) ↑x ⋯) (CategoryTheory.CategoryStruct.comp (U.stalkIso x).inv h) = CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) h

theorem AlgebraicGeometry.Scheme.Opens.stalkIso_inv {X : Scheme} (U : X.Opens) (x : ↥U) : (U.stalkIso x).inv = Hom.stalkMap U.ι x

def AlgebraicGeometry.Scheme.openCoverOfIsOpenCover {s : Type u_1} (X : Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) : X.OpenCover

If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f {s : Type u_1} (X : Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s) : (X.openCoverOfIsOpenCover U hU).f i = (U i).ι

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X {s : Type u_1} (X : Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s) : (X.openCoverOfIsOpenCover U hU).X i = ↑(U i)

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_I₀ {s : Type u_1} (X : Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) : (X.openCoverOfIsOpenCover U hU).I₀ = s

@[deprecated AlgebraicGeometry.Scheme.openCoverOfIsOpenCover (since := "2025-09-30")]

def AlgebraicGeometry.Scheme.openCoverOfISupEqTop {s : Type u_1} (X : Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) : X.OpenCover

Alias of AlgebraicGeometry.Scheme.openCoverOfIsOpenCover.

---

If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

def AlgebraicGeometry.opensRestrict {X : Scheme} (U : X.Opens) : (↑U).Opens ≃ { V : X.Opens // V ≤ U }

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

@[simp]

theorem AlgebraicGeometry.coe_opensRestrict_symm_apply {X : Scheme} (U : X.Opens) (a✝ : { V : X.Opens // V ≤ U }) : ↑((opensRestrict U).symm a✝) = ⇑U.ι ⁻¹' ↑↑((Equiv.subtypeEquivProp ⋯).symm a✝)

@[simp]

theorem AlgebraicGeometry.coe_opensRestrict_apply_coe {X : Scheme} (U : X.Opens) (a✝ : (↑U).Opens) : ↑↑((opensRestrict U) a✝) = (fun (a : ↥↑U) => ↑a) '' ↑a✝

@[implicit_reducible]

instance AlgebraicGeometry.ΓRestrictAlgebra {X : Scheme} (U : X.Opens) : Algebra ↑(X.presheaf.obj (Opposite.op ⊤)) ↑((↑U).presheaf.obj (Opposite.op ⊤))

theorem AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen' {X : Scheme} (U : X.Opens) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))) : (Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) r)

A variant where r is first mapped into Γ(X, U) before taking the basic open.

@[deprecated AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen' (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.map_basicOpen {X : Scheme} (U : X.Opens) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))) : (Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) r)

Alias of AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen'.

---

A variant where r is first mapped into Γ(X, U) before taking the basic open.

theorem AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen {X : Scheme} (U : X.Opens) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))) : (Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen r

theorem AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv {X : Scheme} (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : (Hom.opensFunctor U.ι).obj ((↑U).basicOpen ((CategoryTheory.ConcreteCategory.hom U.topIso.inv) r)) = X.basicOpen r

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

theorem AlgebraicGeometry.Scheme.map_basicOpen_map {X : Scheme} (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : (Hom.opensFunctor U.ι).obj ((↑U).basicOpen ((CategoryTheory.ConcreteCategory.hom U.topIso.inv) r)) = X.basicOpen r

Alias of AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme {X : Scheme} {U : X.Opens} {V : (↑U).Opens} {r : ↑((↑U).presheaf.obj (Opposite.op V))} {x : ↥U} : x ∈ (↑U).basicOpen r ↔ ↑x ∈ X.basicOpen r

noncomputable def AlgebraicGeometry.Scheme.homOfLE (X : Scheme) {U V : X.Opens} (e : U ≤ V) : ↑U ⟶ ↑V

If U ≤ V, then U is also a subscheme of V.

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_ι (X : Scheme) {U V : X.Opens} (e : U ≤ V) : CategoryTheory.CategoryStruct.comp (X.homOfLE e) V.ι = U.ι

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_ι_assoc (X : Scheme) {U V : X.Opens} (e : U ≤ V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.homOfLE e) (CategoryTheory.CategoryStruct.comp V.ι h) = CategoryTheory.CategoryStruct.comp U.ι h

instance AlgebraicGeometry.instIsOverHomOfLE {X : Scheme} {U V : X.Opens} (h : U ≤ V) : Scheme.Hom.IsOver (X.homOfLE h) X

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_rfl (X : Scheme) (U : X.Opens) : X.homOfLE ⋯ = CategoryTheory.CategoryStruct.id ↑U

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_homOfLE (X : Scheme) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W) : CategoryTheory.CategoryStruct.comp (X.homOfLE e₁) (X.homOfLE e₂) = X.homOfLE ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc (X : Scheme) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W) {Z : Scheme} (h : ↑W ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.homOfLE e₁) (CategoryTheory.CategoryStruct.comp (X.homOfLE e₂) h) = CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h

theorem AlgebraicGeometry.Scheme.homOfLE_base {X : Scheme} {U V : X.Opens} (e : U ≤ V) : (X.homOfLE e).base = (TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (CategoryTheory.homOfLE e)

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_apply {X : Scheme} {U V : X.Opens} (e : U ≤ V) (x : ↥U) : ↑((X.homOfLE e) x) = ↑x

theorem AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image {X : Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens) : (Hom.opensFunctor U.ι).obj ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W) ≤ (Hom.opensFunctor V.ι).obj W

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_app {X : Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens) : Hom.app (X.homOfLE e) W = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.homOfLE_appLE {X : Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens) (W' : (↑U).Opens) (e' : W' ≤ (TopologicalSpace.Opens.map (X.homOfLE e).base).obj W) : Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.Scheme.homOfLE_appTop {X : Scheme} {U V : X.Opens} (e : U ≤ V) : Hom.appTop (X.homOfLE e) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

instance AlgebraicGeometry.instIsOpenImmersionHomOfLE (X : Scheme) {U V : X.Opens} (e : U ≤ V) : IsOpenImmersion (X.homOfLE e)

@[simp]

theorem AlgebraicGeometry.Scheme.opensRange_homOfLE {X : Scheme} {U V : X.Opens} (e : U ≤ V) : Hom.opensRange (X.homOfLE e) = (TopologicalSpace.Opens.map V.ι.base).obj U

noncomputable def AlgebraicGeometry.Scheme.Opens.iSupOpenCover {J : Type u_1} {X : Scheme} (U : J → X.Opens) : (↑(⨆ (i : J), U i)).OpenCover

The open cover of ⋃ Vᵢ by Vᵢ.

noncomputable def AlgebraicGeometry.Scheme.restrictFunctor (X : Scheme) : CategoryTheory.Functor X.Opens (CategoryTheory.Over X)

The functor taking open subsets of X to open subschemes of X.

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left (X : Scheme) (U : X.Opens) : (X.restrictFunctor.obj U).left = ↑U

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom (X : Scheme) (U : X.Opens) : (X.restrictFunctor.obj U).hom = U.ι

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left (X : Scheme) {U V : X.Opens} (i : U ⟶ V) : (X.restrictFunctor.map i).left = X.homOfLE ⋯

noncomputable def AlgebraicGeometry.Scheme.restrictFunctorΓ {X : Scheme} : X.restrictFunctor.op.comp ((CategoryTheory.Over.forget X).op.comp Γ) ≅ X.presheaf

The functor that restricts to open subschemes and then takes global section is isomorphic to the structure sheaf.

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app {X : Scheme} (X✝ : X.Opensᵒᵖ) : restrictFunctorΓ.hom.app X✝ = X.presheaf.map (CategoryTheory.eqToHom ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app {X : Scheme} (X✝ : X.Opensᵒᵖ) : restrictFunctorΓ.inv.app X✝ = X.presheaf.map (CategoryTheory.eqToHom ⋯)

noncomputable def AlgebraicGeometry.Scheme.restrictRestrictComm (X : Scheme) (U V : X.Opens) : ↑((TopologicalSpace.Opens.map U.ι.base).obj V) ≅ ↑((TopologicalSpace.Opens.map V.ι.base).obj U)

X ∣_ U ∣_ V is isomorphic to X ∣_ V ∣_ U

noncomputable def AlgebraicGeometry.Scheme.Hom.isoImage {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : ↑U ≅ ↑((opensFunctor f).obj U)

If f : X ⟶ Y is an open immersion, then for any U : X.Opens, we have the isomorphism U ≅ f ''ᵁ U.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : CategoryTheory.CategoryStruct.comp (isoImage f U).hom ((opensFunctor f).obj U).ι = CategoryTheory.CategoryStruct.comp U.ι f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoImage f U).hom (CategoryTheory.CategoryStruct.comp ((opensFunctor f).obj U).ι h) = CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : CategoryTheory.CategoryStruct.comp (isoImage f U).inv (CategoryTheory.CategoryStruct.comp U.ι f) = ((opensFunctor f).obj U).ι

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoImage f U).inv (CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp f h)) = CategoryTheory.CategoryStruct.comp ((opensFunctor f).obj U).ι h

noncomputable def AlgebraicGeometry.Scheme.Hom.isoOpensRange {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : X ≅ ↑(opensRange f)

If f : X ⟶ Y is an open immersion, then X is isomorphic to its image in Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoOpensRange f).hom (opensRange f).ι = f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOpensRange f).hom (CategoryTheory.CategoryStruct.comp (opensRange f).ι h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (isoOpensRange f).inv f = (opensRange f).ι

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOpensRange f).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (opensRange f).ι h

def AlgebraicGeometry.Scheme.topIso (X : Scheme) : ↑⊤ ≅ X

(⊤ : X.Opens) as a scheme is isomorphic to X.

@[simp]

theorem AlgebraicGeometry.Scheme.topIso_hom (X : Scheme) : X.topIso.hom = ⊤.ι

@[simp]

theorem AlgebraicGeometry.Scheme.toIso_inv_ι (X : Scheme) : CategoryTheory.CategoryStruct.comp X.topIso.inv ⊤.ι = CategoryTheory.CategoryStruct.id X

@[simp]

theorem AlgebraicGeometry.Scheme.toIso_inv_ι_assoc (X : Scheme) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp X.topIso.inv (CategoryTheory.CategoryStruct.comp ⊤.ι h) = h

@[simp]

theorem AlgebraicGeometry.Scheme.ι_toIso_inv (X : Scheme) : CategoryTheory.CategoryStruct.comp ⊤.ι X.topIso.inv = CategoryTheory.CategoryStruct.id ↑⊤

@[simp]

theorem AlgebraicGeometry.Scheme.ι_toIso_inv_assoc (X : Scheme) {Z : Scheme} (h : ↑⊤ ⟶ Z) : CategoryTheory.CategoryStruct.comp ⊤.ι (CategoryTheory.CategoryStruct.comp X.topIso.inv h) = h

noncomputable def AlgebraicGeometry.Scheme.isoOfEq (X : Scheme) {U V : X.Opens} (e : U = V) : ↑U ≅ ↑V

If U = V, then X ∣_ U is isomorphic to X ∣_ V.

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfEq_hom_ι (X : Scheme) {U V : X.Opens} (e : U = V) : CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom V.ι = U.ι

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc (X : Scheme) {U V : X.Opens} (e : U = V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom (CategoryTheory.CategoryStruct.comp V.ι h) = CategoryTheory.CategoryStruct.comp U.ι h

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfEq_inv_ι (X : Scheme) {U V : X.Opens} (e : U = V) : CategoryTheory.CategoryStruct.comp (X.isoOfEq e).inv U.ι = V.ι

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfEq_inv_ι_assoc (X : Scheme) {U V : X.Opens} (e : U = V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.isoOfEq e).inv (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp V.ι h

theorem AlgebraicGeometry.Scheme.isoOfEq_hom (X : Scheme) {U V : X.Opens} (e : U = V) : (X.isoOfEq e).hom = X.homOfLE ⋯

theorem AlgebraicGeometry.Scheme.isoOfEq_inv (X : Scheme) {U V : X.Opens} (e : U = V) : (X.isoOfEq e).inv = X.homOfLE ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfEq_rfl (X : Scheme) (U : X.Opens) : X.isoOfEq ⋯ = CategoryTheory.Iso.refl ↑U

noncomputable def AlgebraicGeometry.Scheme.Hom.preimageIso {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) : ↑((TopologicalSpace.Opens.map f.base).obj U) ≅ ↑U

The restriction of an isomorphism onto an open set.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (preimageIso f U).hom U.ι = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (preimageIso f U).hom (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (preimageIso f U).inv (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f) = U.ι

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (preimageIso f U).inv (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι (CategoryTheory.CategoryStruct.comp f h)) = CategoryTheory.CategoryStruct.comp U.ι h

noncomputable def AlgebraicGeometry.Scheme.Opens.isoOfLE {X : Scheme} {U V : X.Opens} (hUV : U ≤ V) : ↑((TopologicalSpace.Opens.map V.ι.base).obj U) ≅ ↑U

If U ≤ V are opens of X, the restriction of U to V is isomorphic to U.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι {X : Scheme} {U V : X.Opens} (hUV : U ≤ V) : CategoryTheory.CategoryStruct.comp (isoOfLE hUV).hom U.ι = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι V.ι

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc {X : Scheme} {U V : X.Opens} (hUV : U ≤ V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOfLE hUV).hom (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι (CategoryTheory.CategoryStruct.comp V.ι h)

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι {X : Scheme} {U V : X.Opens} (hUV : U ≤ V) : CategoryTheory.CategoryStruct.comp (isoOfLE hUV).inv (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι V.ι) = U.ι

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc {X : Scheme} {U V : X.Opens} (hUV : U ≤ V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOfLE hUV).inv (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι (CategoryTheory.CategoryStruct.comp V.ι h)) = CategoryTheory.CategoryStruct.comp U.ι h

noncomputable def AlgebraicGeometry.basicOpenIsoSpecAway {R : CommRingCat} (f : ↑R) : ↑(PrimeSpectrum.basicOpen f) ≅ Spec (CommRingCat.of (Localization.Away f))

For f : R, D(f) as an open subscheme of Spec R is isomorphic to Spec R[1/f].

theorem AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE {R : CommRingCat} (f g x : ↑R) (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (basicOpenIsoSpecAway x).inv ((Spec R).homOfLE ⋯) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g))) (basicOpenIsoSpecAway f).inv

theorem AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc {R : CommRingCat} (f g x : ↑R) (hx : x = f * g) {Z : Scheme} (h : ↑(PrimeSpectrum.basicOpen f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (basicOpenIsoSpecAway x).inv (CategoryTheory.CategoryStruct.comp ((Spec R).homOfLE ⋯) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g))) (CategoryTheory.CategoryStruct.comp (basicOpenIsoSpecAway f).inv h)

noncomputable def AlgebraicGeometry.pullbackRestrictIsoRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.Limits.pullback f U.ι ≅ ↑((TopologicalSpace.Opens.map f.base).obj U)

Given a morphism f : X ⟶ Y and an open set U ⊆ Y, we have X ×[Y] U ≅ X |_{f ⁻¹ U}

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).inv (CategoryTheory.Limits.pullback.fst f U.ι) = ((TopologicalSpace.Opens.map f.base).obj U).ι

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f U.ι) h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι h

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).hom ((TopologicalSpace.Opens.map f.base).obj U).ι = CategoryTheory.Limits.pullback.fst f U.ι

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).hom (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f U.ι) h

noncomputable def AlgebraicGeometry.morphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : ↑((TopologicalSpace.Opens.map f.base).obj U) ⟶ ↑U

The restriction of a morphism X ⟶ Y onto X |_{f ⁻¹ U} ⟶ Y |_ U.

def AlgebraicGeometry.«term_∣__» : Lean.TrailingParserDescr

the notation for restricting a morphism of scheme to an open subset of the target scheme

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).hom (f ∣_ U) = CategoryTheory.Limits.pullback.snd f U.ι

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : Scheme} (h : ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackRestrictIsoRestrict f U).hom (CategoryTheory.CategoryStruct.comp (f ∣_ U) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f U.ι) h

@[simp]

theorem AlgebraicGeometry.morphismRestrict_ι {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (f ∣_ U) U.ι = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f

@[simp]

theorem AlgebraicGeometry.morphismRestrict_ι_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι (CategoryTheory.CategoryStruct.comp f h)

theorem AlgebraicGeometry.isPullback_morphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.IsPullback (f ∣_ U) ((TopologicalSpace.Opens.map f.base).obj U).ι U.ι f

theorem AlgebraicGeometry.isPullback_opens_inf_le {X : Scheme} {U V W : X.Opens} (hU : U ≤ W) (hV : V ≤ W) : CategoryTheory.IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

theorem AlgebraicGeometry.isPullback_opens_inf {X : Scheme} (U V : X.Opens) : CategoryTheory.IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) U.ι V.ι

@[simp]

theorem AlgebraicGeometry.morphismRestrict_id {X : Scheme} (U : X.Opens) : CategoryTheory.CategoryStruct.id X ∣_ U = CategoryTheory.CategoryStruct.id ↑((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X).base).obj U)

theorem AlgebraicGeometry.morphismRestrict_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↥Z) : CategoryTheory.CategoryStruct.comp f g ∣_ U = CategoryTheory.CategoryStruct.comp (f ∣_ (TopologicalSpace.Opens.map g.base).obj U) (g ∣_ U)

instance AlgebraicGeometry.instIsIsoSchemeMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) : CategoryTheory.IsIso (f ∣_ U)

@[simp]

theorem AlgebraicGeometry.morphismRestrict_base_coe {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥↑((TopologicalSpace.Opens.map f.base).obj U)) : ↑((f ∣_ U) x) = f ↑x

theorem AlgebraicGeometry.morphismRestrict_base {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : ⇑(f ∣_ U) = U.carrier.restrictPreimage ⇑f

theorem AlgebraicGeometry.image_morphismRestrict_preimage {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : TopologicalSpace.Opens ↥↑U) : (Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V) = (TopologicalSpace.Opens.map f.base).obj ((Scheme.Hom.opensFunctor U.ι).obj V)

theorem AlgebraicGeometry.morphismRestrict_app {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens) : Scheme.Hom.app (f ∣_ U) V = CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f ((Scheme.Hom.opensFunctor U.ι).obj V)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

theorem AlgebraicGeometry.morphismRestrict_appTop {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : Scheme.Hom.appTop (f ∣_ U) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f ((Scheme.Hom.opensFunctor U.ι).obj ⊤)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

@[simp]

theorem AlgebraicGeometry.morphismRestrict_app' {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : TopologicalSpace.Opens ↥↑U) : Scheme.Hom.app (f ∣_ U) V = Scheme.Hom.appLE f ((Scheme.Hom.opensFunctor U.ι).obj V) ((Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V)) ⋯

@[simp]

theorem AlgebraicGeometry.morphismRestrict_appLE {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens) (W : (↑((TopologicalSpace.Opens.map f.base).obj U)).Opens) (e : W ≤ (TopologicalSpace.Opens.map (f ∣_ U).base).obj V) : Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f ((Scheme.Hom.opensFunctor U.ι).obj V) ((Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj W) ⋯

@[deprecated AlgebraicGeometry.morphismRestrict_appTop (since := "2025-10-14")]

theorem AlgebraicGeometry.Γ_map_morphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : Scheme.Hom.appTop (f ∣_ U) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.app f ((Scheme.Hom.opensFunctor U.ι).obj ⊤)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

Alias of AlgebraicGeometry.morphismRestrict_appTop.

noncomputable def AlgebraicGeometry.morphismRestrictOpensRange {X Y U : Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [IsOpenImmersion g] : CategoryTheory.Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.snd f g)

Restricting a morphism onto the image of an open immersion is isomorphic to the base change along the immersion.

noncomputable def AlgebraicGeometry.morphismRestrictEq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) : CategoryTheory.Arrow.mk (f ∣_ U) ≅ CategoryTheory.Arrow.mk (f ∣_ V)

The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.

noncomputable def AlgebraicGeometry.morphismRestrictRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens) : CategoryTheory.Arrow.mk (f ∣_ U ∣_ V) ≅ CategoryTheory.Arrow.mk (f ∣_ (Scheme.Hom.opensFunctor U.ι).obj V)

Restricting a morphism twice is isomorphic to one restriction.

noncomputable def AlgebraicGeometry.morphismRestrictRestrictBasicOpen {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (r : ↑(Y.presheaf.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (f ∣_ U ∣_ (↑U).basicOpen ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op)) r)) ≅ CategoryTheory.Arrow.mk (f ∣_ Y.basicOpen r)

Restricting a morphism twice onto a basic open set is isomorphic to one restriction.

noncomputable def AlgebraicGeometry.morphismRestrictStalkMap {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥↑((TopologicalSpace.Opens.map f.base).obj U)) : CategoryTheory.Arrow.mk (Scheme.Hom.stalkMap (f ∣_ U) x) ≅ CategoryTheory.Arrow.mk (Scheme.Hom.stalkMap f ↑x)

The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.

instance AlgebraicGeometry.instIsOpenImmersionMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) [IsOpenImmersion f] : IsOpenImmersion (f ∣_ U)

noncomputable def AlgebraicGeometry.Scheme.Hom.resLE {X Y : Scheme} (f : X.Hom Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : ↑V ⟶ ↑U

The restriction of a morphism f : X ⟶ Y to open sets on the source and target.

theorem AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} : resLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯ = f ∣_ U

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_id {X : Scheme} {V V' : X.Opens} (i : V ≤ V') : resLE (CategoryTheory.CategoryStruct.id X) V' V i = X.homOfLE i

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_ι {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (resLE f U V e) U.ι = CategoryTheory.CategoryStruct.comp V.ι f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_ι_assoc {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (resLE f U V e) (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.CategoryStruct.comp f h)

theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : Scheme} (g : Y ⟶ Z) {W : Z.Opens} (e' : U ≤ (TopologicalSpace.Opens.map g.base).obj W) : CategoryTheory.CategoryStruct.comp (resLE f U V e) (resLE g W U e') = resLE (CategoryTheory.CategoryStruct.comp f g) W V ⋯

theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : Scheme} (g : Y ⟶ Z) {W : Z.Opens} (e' : U ≤ (TopologicalSpace.Opens.map g.base).obj W) {Z✝ : Scheme} (h : ↑W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (resLE f U V e) (CategoryTheory.CategoryStruct.comp (resLE g W U e') h) = CategoryTheory.CategoryStruct.comp (resLE (CategoryTheory.CategoryStruct.comp f g) W V ⋯) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_resLE {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V' ≤ V) : CategoryTheory.CategoryStruct.comp (X.homOfLE i) (resLE f U V e) = resLE f U V' ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_resLE_assoc {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V' ≤ V) {Z : Scheme} (h : ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.homOfLE i) (CategoryTheory.CategoryStruct.comp (resLE f U V e) h) = CategoryTheory.CategoryStruct.comp (resLE f U V' ⋯) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_map {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U ≤ U') : CategoryTheory.CategoryStruct.comp (resLE f U V e) (Y.homOfLE i) = resLE f U' V ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_map_assoc {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U ≤ U') {Z : Scheme} (h : ↑U' ⟶ Z) : CategoryTheory.CategoryStruct.comp (resLE f U V e) (CategoryTheory.CategoryStruct.comp (Y.homOfLE i) h) = CategoryTheory.CategoryStruct.comp (resLE f U' V ⋯) h

theorem AlgebraicGeometry.Scheme.Hom.resLE_congr {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (e₁ : U = U') (e₂ : V = V') (P : CategoryTheory.MorphismProperty Scheme) : P (resLE f U V e) ↔ P (resLE f U' V' ⋯)

theorem AlgebraicGeometry.Scheme.Hom.resLE_preimage {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) : (TopologicalSpace.Opens.map (resLE f U V e).base).obj O = (TopologicalSpace.Opens.map V.ι.base).obj ((TopologicalSpace.Opens.map f.base).obj ((opensFunctor U.ι).obj O))

theorem AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens) : W ≤ (TopologicalSpace.Opens.map (resLE f U V e).base).obj O ↔ (opensFunctor V.ι).obj W ≤ (TopologicalSpace.Opens.map f.base).obj ((opensFunctor U.ι).obj O)

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

theorem AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens) : W ≤ (TopologicalSpace.Opens.map (resLE f U V e).base).obj O ↔ (opensFunctor V.ι).obj W ≤ (TopologicalSpace.Opens.map f.base).obj ((opensFunctor U.ι).obj O)

Alias of AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.resLE_app_top {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : app (resLE f U V e) ⊤ = CategoryTheory.CategoryStruct.comp U.topIso.hom (CategoryTheory.CategoryStruct.comp (appLE f U V e) V.topIso.inv)

theorem AlgebraicGeometry.Scheme.Hom.resLE_appLE {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens) (e' : W ≤ (TopologicalSpace.Opens.map (resLE f U V e).base).obj O) : appLE (resLE f U V e) O W e' = appLE f ((opensFunctor U.ι).obj O) ((opensFunctor V.ι).obj W) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_resLE_apply {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↥V) : ↑((resLE f U V e) x) = f ↑x

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

theorem AlgebraicGeometry.Scheme.Hom.coe_resLE_base {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↥V) : ↑((resLE f U V e) x) = f ↑x

Alias of AlgebraicGeometry.Scheme.Hom.coe_resLE_apply.

noncomputable def AlgebraicGeometry.Scheme.Hom.resLEStalkMap {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↥V) : CategoryTheory.Arrow.mk (stalkMap (resLE f U V e) x) ≅ CategoryTheory.Arrow.mk (stalkMap f ↑x)

The stalk map of f.resLE U V at x : V is the stalk map of f at x.

noncomputable def AlgebraicGeometry.arrowResLEAppIso {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e)) ≅ CategoryTheory.Arrow.mk (Scheme.Hom.appLE f U V e)

f.resLE U V induces f.appLE U V on global sections.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_resLE {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) : CategoryTheory.IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

noncomputable def AlgebraicGeometry.Scheme.OpenCover.restrict {X : Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : (↑U).OpenCover

The restriction of an open cover to an open subset.

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_I₀ {X : Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : (𝒰.restrict U).I₀ = 𝒰.I₀

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_X {X : Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x✝ : 𝒰.I₀) : (𝒰.restrict U).X x✝ = ↑((TopologicalSpace.Opens.map (𝒰.f x✝).base).obj U)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_f {X : Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x✝ : 𝒰.I₀) : (𝒰.restrict U).f x✝ = 𝒰.f x✝ ∣_ U