[GOAL]
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ IsOpenImmersion f ↔
    OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ IsOpenImmersion f →
    OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
intro h
[GOAL]
case mp
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
h : IsOpenImmersion f
⊢ OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
exact ⟨h.1, inferInstance⟩
[GOAL]
case mpr
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
⊢ (OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)) →
    IsOpenImmersion f
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mpr.intro
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
h₁ : OpenEmbedding ↑f.val.base
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
⊢ IsOpenImmersion f
[PROOFSTEP]
exact IsOpenImmersion.of_stalk_iso f h₁
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.StableUnderComposition @IsOpenImmersion
[PROOFSTEP]
intro X Y Z f g h₁ h₂
[GOAL]
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h₁ : IsOpenImmersion f
h₂ : IsOpenImmersion g
⊢ IsOpenImmersion (f ≫ g)
[PROOFSTEP]
exact LocallyRingedSpace.IsOpenImmersion.comp f g
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsOpenImmersion
[PROOFSTEP]
apply isOpenImmersion_stableUnderComposition.respectsIso
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (e : X ≅ Y), IsOpenImmersion e.hom
[PROOFSTEP]
intro _ _ _
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
X✝ Y✝ : Scheme
e✝ : X✝ ≅ Y✝
⊢ IsOpenImmersion e✝.hom
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ PropertyIsLocalAtTarget @IsOpenImmersion
[PROOFSTEP]
constructor
[GOAL]
case RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsOpenImmersion
[PROOFSTEP]
exact isOpenImmersion_respectsIso
[GOAL]
case restrict
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Opens ↑↑Y.toPresheafedSpace), IsOpenImmersion f → IsOpenImmersion (f ∣_ U)
[PROOFSTEP]
intros
[GOAL]
case restrict
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
U✝ : Opens ↑↑Y✝.toPresheafedSpace
a✝ : IsOpenImmersion f✝
⊢ IsOpenImmersion (f✝ ∣_ U✝)
[PROOFSTEP]
infer_instance
[GOAL]
case of_openCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Scheme.OpenCover Y), (∀ (i : 𝒰.J), IsOpenImmersion pullback.snd) → IsOpenImmersion f
[PROOFSTEP]
intro X Y f 𝒰 H
[GOAL]
case of_openCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ IsOpenImmersion f
[PROOFSTEP]
rw [isOpenImmersion_iff_stalk]
[GOAL]
case of_openCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ OpenEmbedding ↑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
constructor
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ OpenEmbedding ↑f.val.base
[PROOFSTEP]
apply (openEmbedding_iff_openEmbedding_of_iSup_eq_top 𝒰.iSup_opensRange f.1.base.2).mpr
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ ∀ (i : 𝒰.J),
    OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
intro i
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
have := ((isOpenImmersion_respectsIso.arrow_iso_iff (morphismRestrictOpensRange f (𝒰.map i))).mpr (H i)).1
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
this : OpenEmbedding ↑(Arrow.mk (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i))).hom.val.base
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
erw [Arrow.mk_hom, morphismRestrict_val_base] at this 
[GOAL]
case of_openCover.left
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
i : 𝒰.J
this : OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier ↑f.val.base)
⊢ OpenEmbedding (Set.restrictPreimage (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 i)).carrier f.val.base.toFun)
[PROOFSTEP]
norm_cast
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
intro x
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
have := Arrow.iso_w (morphismRestrictStalkMap f (Scheme.Hom.opensRange (𝒰.map <| 𝒰.f <| f.1.base x)) ⟨x, 𝒰.Covers _⟩)
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  (Arrow.mk
        (PresheafedSpace.stalkMap f.val
          ↑{ val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) })).hom =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      (Arrow.mk
            (PresheafedSpace.stalkMap
              (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) })).hom ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
dsimp only [Arrow.mk_hom] at this 
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso (PresheafedSpace.stalkMap f.val x)
[PROOFSTEP]
rw [this]
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
⊢ IsIso
    ((morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right)
[PROOFSTEP]
haveI : IsOpenImmersion (f ∣_ Scheme.Hom.opensRange (𝒰.map <| 𝒰.f <| f.1.base x)) :=
  (isOpenImmersion_respectsIso.arrow_iso_iff (morphismRestrictOpensRange f (𝒰.map _))).mpr (H _)
[GOAL]
case of_openCover.right
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover Y
H : ∀ (i : 𝒰.J), IsOpenImmersion pullback.snd
x : ↑↑X.toPresheafedSpace
this✝ :
  PresheafedSpace.stalkMap f.val x =
    (morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right
this : IsOpenImmersion (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
⊢ IsIso
    ((morphismRestrictStalkMap f (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
            { val := x,
              property :=
                (_ :
                  ↑f.val.base x ∈
                    Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).inv.left ≫
      PresheafedSpace.stalkMap
          (f ∣_ Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x)))).val
          { val := x,
            property :=
              (_ :
                ↑f.val.base x ∈ Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) } ≫
        (morphismRestrictStalkMap f
              (Scheme.Hom.opensRange (Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))))
              { val := x,
                property :=
                  (_ :
                    ↑f.val.base x ∈
                      Set.range ↑(Scheme.OpenCover.map 𝒰 (Scheme.OpenCover.f 𝒰 (↑f.val.base x))).val.base) }).hom.right)
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X Y S : Scheme) (f : X ⟶ S) (g : Y ⟶ S), IsOpenImmersion g → IsOpenImmersion pullback.fst
[PROOFSTEP]
intro X Y Z f g H
[GOAL]
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion g
⊢ IsOpenImmersion pullback.fst
[PROOFSTEP]
infer_instance
