C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f)))
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f)))
haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.inj
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
⊢ {c : Opens ↑X} →
    {d : Opens ↑Y} →
      (d ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c) →
        (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c' ≅ d)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f)))
apply compatiblePreservingOfDownwardsClosed
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
⊢ (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c' ≅ V)
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
⊢ {c : Opens ↑X} →
    {d : Opens ↑Y} →
      (d ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c) →
        (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c' ≅ d)
intro U V i
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range fun x => (forget TopCat).map f x
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
⊢ (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj c' ≅ V)
refine' ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ _⟩
case hF.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
w✝ : (forget TopCat).obj X
left✝ : w✝ ∈ ↑U
h : (forget TopCat).map f w✝ ∈ V.1
⊢ (forget TopCat).map f w✝ ∈ Set.range fun x => (forget TopCat).map f x
case hF
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range fun x => (forget TopCat).map f x
obtain ⟨_, _, rfl⟩ := i.le h
no goals
case hF.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ((forget TopCat).map f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map f))).obj U
w✝ : (forget TopCat).obj X
left✝ : w✝ ∈ ↑U
h : (forget TopCat).map f w✝ ∈ V.1
⊢ (forget TopCat).map f w✝ ∈ Set.range fun x => (forget TopCat).map f x
exact ⟨_, rfl⟩