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. X ∣_ᵤ U is the notation for restricting onto an open set, and ιOpens U is a shorthand for X.restrict U.open_embedding : X ∣_ᵤ U ⟶ X.
• AlgebraicGeometry.morphism_restrict: The restriction of X ⟶ Y to X ∣_ᵤ f ⁻¹ᵁ U ⟶ Y ∣_ᵤ U.

def AlgebraicGeometry.«term_⁻¹ᵁ_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def AlgebraicGeometry.«term_⁻¹ᵁ_» : Lean.TrailingParserDescr

f ⁻¹ᵁ U is notation for (Opens.map f.1.base).obj U, the preimage of an open set U under f.

Equations

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

def AlgebraicGeometry.«term_∣_ᵤ_» : Lean.TrailingParserDescr

X ∣_ᵤ U is notation for X.restrict U.openEmbedding, the restriction of X to an open set U of X.

Equations

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

def AlgebraicGeometry.«term_∣_ᵤ_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.ιOpens {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X ∣_ᵤ U ⟶ X

The restriction of a scheme to an open subset.

Equations

• AlgebraicGeometry.Scheme.ιOpens U = AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion U))

theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app_self {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion U))).val.c.app (Opposite.op U) = X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj (Opposite.op ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).toPrefunctor.obj U)).unop = U)).op

theorem AlgebraicGeometry.Scheme.eq_restrict_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {V : TopologicalSpace.Opens ↥U} {W : TopologicalSpace.Opens ↥U} (e : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V = (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj W) : X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom e).op = (X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : V = W)).op

instance AlgebraicGeometry.ΓRestrictAlgebra {X : AlgebraicGeometry.Scheme} {Y : TopCat} {f : Y ⟶ ↑X.toPresheafedSpace} (hf : OpenEmbedding ⇑f) : Algebra ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op X)) ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X hf)))

Equations

• AlgebraicGeometry.ΓRestrictAlgebra hf = RingHom.toAlgebra (AlgebraicGeometry.Scheme.Γ.toPrefunctor.map (AlgebraicGeometry.Scheme.ofRestrict X hf).op)

theorem AlgebraicGeometry.Scheme.map_basicOpen' (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (r : ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op (X ∣_ᵤ U)))) : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ((X ∣_ᵤ U).basicOpen r) = X.basicOpen ((X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : U = (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ⊤)).op) r)

theorem AlgebraicGeometry.Scheme.map_basicOpen (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (r : ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op (X ∣_ᵤ U)))) : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ((X ∣_ᵤ U).basicOpen r) = X.basicOpen r

theorem AlgebraicGeometry.Scheme.map_basicOpen_map (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (r : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ((X ∣_ᵤ U).basicOpen ((X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ⊤ = U)).op) r)) = X.basicOpen r

def AlgebraicGeometry.Scheme.restrictFunctor (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : ((AlgebraicGeometry.Scheme.restrictFunctor X).toPrefunctor.obj U).left = X ∣_ᵤ U

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : U ⟶ V) : ((AlgebraicGeometry.Scheme.restrictFunctor X).toPrefunctor.map i).left = AlgebraicGeometry.IsOpenImmersion.lift (AlgebraicGeometry.Scheme.ιOpens V) (AlgebraicGeometry.Scheme.ιOpens U) (_ : Set.range ⇑(AlgebraicGeometry.Scheme.ιOpens U).val.base ⊆ Set.range ⇑(AlgebraicGeometry.Scheme.ιOpens V).val.base)

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

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

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

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : U ⟶ V) (W : TopologicalSpace.Opens ↥V) : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj (((AlgebraicGeometry.Scheme.restrictFunctor X).toPrefunctor.map i).left⁻¹ᵁ W) ≤ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion V))).toPrefunctor.obj W

theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : U ⟶ V) (W : TopologicalSpace.Opens ↥V) : ((AlgebraicGeometry.Scheme.restrictFunctor X).toPrefunctor.map i).left.val.c.app (Opposite.op W) = X.presheaf.toPrefunctor.map (CategoryTheory.homOfLE (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj (((AlgebraicGeometry.Scheme.restrictFunctor X).toPrefunctor.map i).left⁻¹ᵁ W) ≤ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion V))).toPrefunctor.obj W)).op

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app (X : AlgebraicGeometry.Scheme) (X : (TopologicalSpace.Opens ↑↑X✝.toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Scheme.restrictFunctorΓ X✝).inv.app X = X✝.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : Opposite.op X.unop = Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion X.unop))).toPrefunctor.obj ⊤)))

@[simp]

theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app (X : AlgebraicGeometry.Scheme) (X : (TopologicalSpace.Opens ↑↑X✝.toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Scheme.restrictFunctorΓ X✝).hom.app X = X✝.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion X.unop))).toPrefunctor.obj ⊤) = Opposite.op X.unop))

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

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

Equations

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

noncomputable def AlgebraicGeometry.Scheme.restrictRestrictComm (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X ∣_ᵤ U ∣_ᵤ AlgebraicGeometry.Scheme.ιOpens U⁻¹ᵁ V ≅ X ∣_ᵤ V ∣_ᵤ AlgebraicGeometry.Scheme.ιOpens V⁻¹ᵁ 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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) : X ∣_ᵤ U ∣_ᵤ V ≅ X ∣_ᵤ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V

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

Equations

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

theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict_assoc (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.restrictRestrict X U V).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens V) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens U) h)

@[simp]

theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.restrictRestrict X U V).hom (AlgebraicGeometry.Scheme.ιOpens ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens V) (AlgebraicGeometry.Scheme.ιOpens U)

theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict_assoc (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.restrictRestrict X U V).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens V) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens U) h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V)) h

@[simp]

theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.restrictRestrict X U V).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens V) (AlgebraicGeometry.Scheme.ιOpens U)) = AlgebraicGeometry.Scheme.ιOpens ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V)

noncomputable def AlgebraicGeometry.Scheme.restrictIsoOfEq (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (e : U = V) : X ∣_ᵤ U ≅ X ∣_ᵤ V

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

Equations

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

@[inline, reducible]

noncomputable abbrev AlgebraicGeometry.Scheme.restrictMapIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : X ∣_ᵤ f⁻¹ᵁ U ≅ Y ∣_ᵤ U

The restriction of an isomorphism onto an open set.

Equations

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

def AlgebraicGeometry.pullbackRestrictIsoRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.ιOpens U) ≅ X ∣_ᵤ f⁻¹ᵁ U

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

Equations

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

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion (f⁻¹ᵁ U)))) h

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv CategoryTheory.Limits.pullback.fst = AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion (f⁻¹ᵁ U)))

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens (f⁻¹ᵁ U)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h

@[simp]

theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom (AlgebraicGeometry.Scheme.ιOpens (f⁻¹ᵁ U)) = CategoryTheory.Limits.pullback.fst

def AlgebraicGeometry.morphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : X ∣_ᵤ f⁻¹ᵁ U ⟶ Y ∣_ᵤ 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

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 : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : Y ∣_ᵤ U ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom (CategoryTheory.CategoryStruct.comp (f ∣_ U) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h

@[simp]

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

theorem AlgebraicGeometry.morphismRestrict_ι_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens U) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens (f⁻¹ᵁ U)) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.morphismRestrict_ι {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (f ∣_ U) (AlgebraicGeometry.Scheme.ιOpens U) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ιOpens (f⁻¹ᵁ U)) f

theorem AlgebraicGeometry.isPullback_morphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.IsPullback (f ∣_ U) (AlgebraicGeometry.Scheme.ιOpens (f⁻¹ᵁ U)) (AlgebraicGeometry.Scheme.ιOpens U) f

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 ∣_ g⁻¹ᵁ U) (g ∣_ U)

instance AlgebraicGeometry.instIsIsoSchemeInstCategorySchemeRestrictObjOpensαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensTopCatToQuiverToCategoryStructInstTopCatLargeCategoryToPrefunctorToTopCatObjToPrefunctorMapBaseValInclusionOpenEmbeddingMorphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.IsIso (f ∣_ U)

Equations

• (_ : CategoryTheory.IsIso (f ∣_ U)) = (_ : CategoryTheory.IsIso (f ∣_ U))

theorem AlgebraicGeometry.morphismRestrict_base_coe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (x : (CategoryTheory.forget TopCat).toPrefunctor.obj ↑(X ∣_ᵤ f⁻¹ᵁ U).toLocallyRingedSpace.toSheafedSpace.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 : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : ⇑(f ∣_ U).val.base = Set.restrictPreimage U.carrier ⇑f.val.base

theorem AlgebraicGeometry.image_morphismRestrict_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (V : TopologicalSpace.Opens ↥U) : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion (f⁻¹ᵁ U)))).toPrefunctor.obj ((f ∣_ U)⁻¹ᵁ V) = f⁻¹ᵁ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V

theorem AlgebraicGeometry.morphismRestrict_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (V : TopologicalSpace.Opens ↥U) : (f ∣_ U).val.c.app (Opposite.op V) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V))) (X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion (f⁻¹ᵁ U)))).toPrefunctor.obj ((f ∣_ U)⁻¹ᵁ V) = f⁻¹ᵁ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V)).op)

theorem AlgebraicGeometry.Γ_map_morphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : AlgebraicGeometry.Scheme.Γ.toPrefunctor.map (f ∣_ U).op = CategoryTheory.CategoryStruct.comp (Y.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : U = (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ⊤)).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op U)) (X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion (f⁻¹ᵁ U)))).toPrefunctor.obj ⊤ = f⁻¹ᵁ U)).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

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 : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (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 (_ : CategoryTheory.Arrow.mk (f ∣_ U) = CategoryTheory.Arrow.mk (f ∣_ V))

def AlgebraicGeometry.morphismRestrictRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(Y ∣_ᵤ U).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) : CategoryTheory.Arrow.mk (f ∣_ U ∣_ V) ≅ CategoryTheory.Arrow.mk (f ∣_ (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.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 : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (r : ↑(Y.presheaf.toPrefunctor.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (f ∣_ U ∣_ (Y ∣_ᵤ U).basicOpen ((Y.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ⇑(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ⊤ = U)).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 : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (x : ↑↑(X ∣_ᵤ f⁻¹ᵁ U).toLocallyRingedSpace.toSheafedSpace.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.instIsOpenImmersionRestrictObjOpensαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensTopCatToQuiverToCategoryStructInstTopCatLargeCategoryToPrefunctorToTopCatObjToPrefunctorMapBaseValInclusionOpenEmbeddingMorphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsOpenImmersion (f ∣_ U)

Equations

• (_ : AlgebraicGeometry.IsOpenImmersion (f ∣_ U)) = (_ : AlgebraicGeometry.IsOpenImmersion (f ∣_ U))