[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (𝟙 X.toSheafedSpace) x)
[PROOFSTEP]
erw [PresheafedSpace.stalkMap.id]
[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (𝟙 (PresheafedSpace.stalk X.toPresheafedSpace x))
[PROOFSTEP]
apply isLocalRingHom_id
[GOAL]
X✝ : LocallyRingedSpace
X Y Z : LocallyRingedSpace
f : Hom X Y
g : Hom Y Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (f.val ≫ g.val) x)
[PROOFSTEP]
erw [PresheafedSpace.stalkMap.comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y Z : LocallyRingedSpace
f : Hom X Y
g : Hom Y Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap g.val (↑f.val.base x) ≫ PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
exact @isLocalRingHom_comp _ _ _ _ _ _ _ _ (f.2 _) (g.2 _)
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (𝟙 X ≫ f).val = f.val
[PROOFSTEP]
simp [comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (f ≫ 𝟙 Y).val = f.val
[PROOFSTEP]
simp [comp]
[GOAL]
X : LocallyRingedSpace
x✝³ x✝² x✝¹ x✝ : LocallyRingedSpace
f : x✝³ ⟶ x✝²
g : x✝² ⟶ x✝¹
h : x✝¹ ⟶ x✝
⊢ ((f ≫ g) ≫ h).val = (f ≫ g ≫ h).val
[PROOFSTEP]
simp [comp]
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X.toSheafedSpace ⟶ Y.toSheafedSpace
inst✝ : IsIso f
x : ↑↑X.toPresheafedSpace
⊢ IsLocalRingHom (PresheafedSpace.stalkMap (SheafedSpace.forgetToPresheafedSpace.map f) x)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
⊢ ∀ (x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace),
    LocalRing ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
intro x
[GOAL]
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace
⊢ LocalRing ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
apply @RingEquiv.localRing _ _ _ (X.localRing (f x))
[GOAL]
case e
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ toTopCat X
h : OpenEmbedding ↑f
x : ↑↑(SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace
⊢ ↑(Presheaf.stalk X.presheaf (↑f x)) ≃+*
    ↑(Presheaf.stalk (SheafedSpace.restrict X.toSheafedSpace h).toPresheafedSpace.presheaf x)
[PROOFSTEP]
exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv
[GOAL]
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s) =
    RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s)
[PROOFSTEP]
ext x
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s)) ↔
    x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s)) →
    x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
rintro ⟨⟨y, hyU⟩, hy : IsUnit _, rfl : y = _⟩
[GOAL]
case h.h.mp.intro.mk.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hyU : ↑f.val.base x ∈ U
hy : IsUnit (↑(Presheaf.germ (toRingedSpace Y).toPresheafedSpace.presheaf { val := ↑f.val.base x, property := hyU }) s)
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s))
[PROOFSTEP]
erw [RingedSpace.mem_basicOpen _ _ ⟨x, show x ∈ (Opens.map f.1.base).obj U from hyU⟩, ←
  PresheafedSpace.stalkMap_germ_apply]
[GOAL]
case h.h.mp.intro.mk.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hyU : ↑f.val.base x ∈ U
hy : IsUnit (↑(Presheaf.germ (toRingedSpace Y).toPresheafedSpace.presheaf { val := ↑f.val.base x, property := hyU }) s)
⊢ IsUnit
    (↑(PresheafedSpace.stalkMap f.val ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) })
      (↑(Presheaf.germ Y.presheaf
            { val := ↑f.val.base ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) },
              property :=
                (_ :
                  ↑{ val := x, property := (_ : x ∈ (Opens.map f.val.base).obj U) } ∈ (Opens.map f.val.base).obj U) })
        s))
[PROOFSTEP]
exact (PresheafedSpace.stalkMap f.1 _).isUnit_map hy
[GOAL]
case h.h.mpr
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) (↑(NatTrans.app f.val.c (op U)) s)) →
    x ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s))
[PROOFSTEP]
rintro ⟨y, hy : IsUnit _, rfl⟩
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy : IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf y) (↑(NatTrans.app f.val.c (op U)) s))
⊢ ↑y ∈ ↑((Opens.map f.val.base).obj (RingedSpace.basicOpen (toRingedSpace Y) s))
[PROOFSTEP]
erw [RingedSpace.mem_basicOpen _ _ ⟨f.1.base y.1, y.2⟩]
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy : IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf y) (↑(NatTrans.app f.val.c (op U)) s))
⊢ IsUnit (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s)
[PROOFSTEP]
erw [← PresheafedSpace.stalkMap_germ_apply] at hy 
[GOAL]
case h.h.mpr.intro.intro
X✝ : LocallyRingedSpace
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑(toTopCat Y)
s : ↑(Y.presheaf.obj (op U))
y : { x // x ∈ (Opens.map f.val.base).obj U }
hy :
  IsUnit
    (↑(PresheafedSpace.stalkMap f.val ↑y)
      (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s))
⊢ IsUnit (↑(Presheaf.germ Y.presheaf { val := ↑f.val.base ↑y, property := (_ : ↑y ∈ (Opens.map f.val.base).obj U) }) s)
[PROOFSTEP]
exact (isUnit_map_iff (PresheafedSpace.stalkMap f.1 _) _).mp hy
[GOAL]
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ RingedSpace.basicOpen (toRingedSpace X) 0 = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) 0) ↔ x ∈ ↑⊥
[PROOFSTEP]
simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_right,
  exists_eq_right, Opens.coe_bot, Set.mem_empty_iff_false, iff_false, not_exists]
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U),
    ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
[PROOFSTEP]
intros hx
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
[PROOFSTEP]
rw [map_zero, isUnit_zero_iff]
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1
[PROOFSTEP]
change (0 : X.stalk x) ≠ (1 : X.stalk x)
[GOAL]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1
[PROOFSTEP]
exact zero_ne_one
