[GOAL]
X : Scheme
⊢ Continuous fun x => PEmpty.elim x
[PROOFSTEP]
continuity
[GOAL]
X : Scheme
f g : ∅ ⟶ X
⊢ f.val.base = g.val.base
[PROOFSTEP]
ext a
[GOAL]
case w
X : Scheme
f g : ∅ ⟶ X
a : (forget TopCat).obj ↑∅.toPresheafedSpace
⊢ ↑f.val.base a = ↑g.val.base a
[PROOFSTEP]
exact PEmpty.elim a
[GOAL]
X : Scheme
f g : ∅ ⟶ X
a : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app (f.val.c ≫ whiskerRight (eqToHom (_ : (Opens.map f.val.base).op = (Opens.map g.val.base).op)) ∅.presheaf)
      a =
    NatTrans.app g.val.c a
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ IsEmpty PEmpty
[PROOFSTEP]
infer_instance
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsOpenImmersion f
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) IsOpenImmersion.of_stalk_iso
[GOAL]
case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ OpenEmbedding ↑f.val.base
[PROOFSTEP]
apply openEmbedding_of_continuous_injective_open
[GOAL]
case hf.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ Continuous ↑f.val.base
[PROOFSTEP]
continuity
[GOAL]
case hf.h₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ Function.Injective ↑f.val.base
[PROOFSTEP]
rintro (i : X.carrier)
[GOAL]
case hf.h₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
i : ↑↑X.toPresheafedSpace
⊢ ∀ ⦃a₂ : (forget TopCat).obj ↑X.toPresheafedSpace⦄, ↑f.val.base i = ↑f.val.base a₂ → i = a₂
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
case hf.h₃
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsOpenMap ↑f.val.base
[PROOFSTEP]
intro U _
[GOAL]
case hf.h₃
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
⊢ IsOpen (↑f.val.base '' U)
[PROOFSTEP]
convert isOpen_empty (α := Y)
[GOAL]
case h.e'_3.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
⊢ ↑f.val.base '' U = ∅
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
x✝ : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ x✝ ∈ ↑f.val.base '' U ↔ x✝ ∈ ∅
[PROOFSTEP]
rw [Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case h.e'_3.h.h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : Set ((forget TopCat).obj ↑X.toPresheafedSpace)
a✝ : IsOpen U
e_1✝ : (forget TopCat).obj ↑Y.toPresheafedSpace = ↑↑Y.toPresheafedSpace
x✝ : (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ ¬x✝ ∈ ↑f.val.base '' U
[PROOFSTEP]
exact fun x => isEmptyElim (show X.carrier from x.choose)
[GOAL]
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
rintro (i : X.carrier)
[GOAL]
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
i : ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.stalkMap f.val i)
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
⊢ IsIso f
[PROOFSTEP]
haveI : IsEmpty X.carrier := ⟨fun x => isEmptyElim (show Y.carrier from f.1.base x)⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ IsIso f
[PROOFSTEP]
have : Epi f.1.base
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ Epi f.val.base
[PROOFSTEP]
rw [TopCat.epi_iff_surjective]
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ Function.Surjective ↑f.val.base
[PROOFSTEP]
rintro (x : Y.carrier)
[GOAL]
case this
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this : IsEmpty ↑↑X.toPresheafedSpace
x : ↑↑Y.toPresheafedSpace
⊢ ∃ a, ↑f.val.base a = x
[PROOFSTEP]
exact isEmptyElim x
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↑↑Y.toPresheafedSpace
this✝ : IsEmpty ↑↑X.toPresheafedSpace
this : Epi f.val.base
⊢ IsIso f
[PROOFSTEP]
apply IsOpenImmersion.to_iso
[GOAL]
X : Scheme
⊢ IsAffineOpen ⊥
[PROOFSTEP]
convert rangeIsAffineOpenOfOpenImmersion (initial.to X)
[GOAL]
case h.e'_2
X : Scheme
⊢ ⊥ = Scheme.Hom.opensRange (initial.to X)
[PROOFSTEP]
ext
  -- Porting note : added this `erw` to turn LHS to `False`
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
erw [Set.mem_empty_iff_false]
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ False ↔ x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
rw [false_iff_iff]
[GOAL]
case h.e'_2.h.h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ ¬x✝ ∈ ↑(Scheme.Hom.opensRange (initial.to X))
[PROOFSTEP]
exact fun x => isEmptyElim (show (⊥_ Scheme).carrier from x.choose)
[GOAL]
A : Scheme
f : A ⟶ ⊥_ Scheme
⊢ IsIso f
[PROOFSTEP]
infer_instance
