@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoRestrict_hom_ofRestrict {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoRestrict f).hom (Z.ofRestrict ⋯) = f

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] {Z✝ : AlgebraicGeometry.Scheme} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoRestrict f).hom (CategoryTheory.CategoryStruct.comp (Z.ofRestrict ⋯) h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Scheme.Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap g (f.base x)) (AlgebraicGeometry.Scheme.Hom.stalkMap f x)

instance AlgebraicGeometry.Scheme.Hom.stalkMap.isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)

theorem AlgebraicGeometry.Scheme.Hom.ext_iff {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) : f = g ↔ ∃ (h_base : f.base = g.base), ∀ (U : Y.Opens), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) = AlgebraicGeometry.Scheme.Hom.app g U

theorem AlgebraicGeometry.Scheme.Hom.comp_c_app {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : (CategoryTheory.CategoryStruct.comp f g).c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (g.c.app (Opposite.op U)) (f.c.app ((TopologicalSpace.Opens.map g.base).op.obj (Opposite.op U)))