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.morphism_restrict: The restriction of X ⟶ Y to X ∣_ᵤ f ⁻¹ᵁ U ⟶ Y ∣_ᵤ U.

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

Open subset of a scheme as a scheme.

Equations

• ↑U = X.restrict ⋯

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

Equations

• AlgebraicGeometry.Scheme.Opens.instCoeOut = { coe := AlgebraicGeometry.Scheme.Opens.toScheme }

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.ι_val_base_apply {X : AlgebraicGeometry.Scheme} (U : X.Opens) (self : ↥U) : U.ι.val.base self = ↑self

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

The restriction of a scheme to an open subset.

Equations

• U.ι = X.ofRestrict ⋯

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

Equations

• ⋯ = ⋯

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} {W : (↑U).Opens} (e : (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V = (AlgebraicGeometry.Scheme.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 : AlgebraicGeometry.Scheme} (U : X.Opens) : Nonempty ↑↑(↑U).toPresheafedSpace ↔ (↑U).Nonempty

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Opens.topIso {X : AlgebraicGeometry.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.

Equations

• U.topIso = CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op

def AlgebraicGeometry.Scheme.Opens.stalkIso {X : AlgebraicGeometry.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.

Equations

• U.stalkIso x = X.restrictStalkIso ⋯ x

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace} (x : ↥V) {Z : CommRingCat} (h : X.presheaf.stalk ↑↑x ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ x) (CategoryTheory.CategoryStruct.comp (U.stalkIso ↑x).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ ⟨↑↑x, ⋯⟩) h

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace} (x : ↥V) : CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ x) (U.stalkIso ↑x).hom = X.presheaf.germ ⟨↑↑x, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_obj {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : ⨆ (i : s), U i = ⊤) (i : s) : (X.openCoverOfSuprEqTop U hU).obj i = ↑(U i)

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_J {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : ⨆ (i : s), U i = ⊤) : (X.openCoverOfSuprEqTop U hU).J = s

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_map {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : ⨆ (i : s), U i = ⊤) (i : s) : (X.openCoverOfSuprEqTop U hU).map i = (U i).ι

def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : ⨆ (i : s), U i = ⊤) : X.OpenCover

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

Equations

• X.openCoverOfSuprEqTop U hU = { J := s, obj := fun (i : s) => ↑(U i), map := fun (i : s) => (U i).ι, f := fun (x : ↑↑X.toPresheafedSpace) => ⋯.choose, covers := ⋯, IsOpen := ⋯ }

@[simp]

theorem AlgebraicGeometry.opensRestrict_apply_coe_coe {X : AlgebraicGeometry.Scheme} (U : X.Opens) : ∀ (a : (↑U).Opens), ↑↑((AlgebraicGeometry.opensRestrict U) a) = ⇑U.ι.val.base '' ↑a

@[simp]

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

def AlgebraicGeometry.opensRestrict {X : AlgebraicGeometry.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.

Equations

• AlgebraicGeometry.opensRestrict U = (AlgebraicGeometry.IsOpenImmersion.opensEquiv U.ι).trans (Equiv.subtypeEquivProp ⋯)

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

Equations

• AlgebraicGeometry.ΓRestrictAlgebra U = RingHom.toAlgebra (AlgebraicGeometry.Scheme.Hom.app U.ι ⊤)

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict_assoc {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U ⟶ V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.restrictFunctor.map i).left (CategoryTheory.CategoryStruct.comp V.ι h) = CategoryTheory.CategoryStruct.comp U.ι h

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (X.restrictFunctor.map i).left V.ι = U.ι

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U ⟶ V) : (X.restrictFunctor.map i).left.val.base = (TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map i

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U ⟶ V) (W : (↑V).Opens) : (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((TopologicalSpace.Opens.map (X.restrictFunctor.map i).left.val.base).obj W) ≤ (AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U ⟶ V) (W : (↑V).Opens) : AlgebraicGeometry.Scheme.Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

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

@[simp]

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

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

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

Equations

• AlgebraicGeometry.Scheme.restrictFunctorΓ = CategoryTheory.NatIso.ofComponents (fun (U : X.Opensᵒᵖ) => CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).symm.op) ⋯

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

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

Equations

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

noncomputable def AlgebraicGeometry.Scheme.restrictRestrict (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) : ↑V ≅ ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)

If V is an open subset of U, then X ∣_ U ∣_ V is isomorphic to X ∣_ V.

Equations

• X.restrictRestrict U V = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.CategoryStruct.comp V.ι U.ι) ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι ⋯

theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict_assoc (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.restrictRestrict U V).hom (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι h) = CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.CategoryStruct.comp U.ι h)

@[simp]

theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) : CategoryTheory.CategoryStruct.comp (X.restrictRestrict U V).hom ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι = CategoryTheory.CategoryStruct.comp V.ι U.ι

theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict_assoc (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.restrictRestrict U V).inv (CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.CategoryStruct.comp U.ι h)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι h

@[simp]

theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) : CategoryTheory.CategoryStruct.comp (X.restrictRestrict U V).inv (CategoryTheory.CategoryStruct.comp V.ι U.ι) = ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι

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

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

Equations

• X.restrictIsoOfEq e = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq U.ι V.ι ⋯

@[reducible, inline]

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

The restriction of an isomorphism onto an open set.

Equations

• AlgebraicGeometry.Scheme.restrictMapIso f U = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.val.base).obj U).ι f) U.ι ⋯

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

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

Equations

• AlgebraicGeometry.pullbackRestrictIsoRestrict f U = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.Limits.pullback.fst f U.ι) ((TopologicalSpace.Opens.map f.val.base).obj U).ι ⋯

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

@[simp]

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

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

@[simp]

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

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

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

Equations

• f ∣_ U = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv (CategoryTheory.Limits.pullback.snd f U.ι)

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

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

Equations

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

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

theorem AlgebraicGeometry.eqToHom_eq_homOfLE {C : Type u_1} [Preorder C] {X : C} {Y : C} (e : X = Y) : CategoryTheory.eqToHom e = CategoryTheory.homOfLE ⋯

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

@[simp]

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

@[simp]

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

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

def AlgebraicGeometry.morphismRestrictOpensRange {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [hg : AlgebraicGeometry.IsOpenImmersion g] : CategoryTheory.Arrow.mk (f ∣_ AlgebraicGeometry.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.

Equations

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

def AlgebraicGeometry.morphismRestrictEq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {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.

Equations

• AlgebraicGeometry.morphismRestrictEq f e = CategoryTheory.eqToIso ⋯

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

Restricting a morphism twice is isomorphic to one restriction.

Equations

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

def AlgebraicGeometry.morphismRestrictRestrictBasicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (r : ↑(Y.presheaf.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (f ∣_ U ∣_ (↑U).basicOpen ((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.

Equations

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

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

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : ∀ (x : 𝒰.J), (𝒰.restrict U).obj x = ↑((TopologicalSpace.Opens.map (𝒰.map x).val.base).obj U)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : ∀ (x : 𝒰.J), (𝒰.restrict U).map x = 𝒰.map x ∣_ U

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.restrict_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) : (𝒰.restrict U).J = 𝒰.J

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

The restriction of an open cover to an open subset.

Equations

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