case cover_preserve
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward (functor hf) S ∈
        GrothendieckTopology.sieves (Opens.grothendieckTopology ↑Y) ((functor hf).obj U)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) (functor hf)
constructor
case cover_preserve.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ (forget TopCat).map f x ∈ U_1
case cover_preserve
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward (functor hf) S ∈
        GrothendieckTopology.sieves (Opens.grothendieckTopology ↑Y) ((functor hf).obj U)
rintro U S hU _ ⟨x, hx, rfl⟩
case cover_preserve.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ (forget TopCat).map f x ∈ U_1
case cover_preserve.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ (forget TopCat).map f x ∈ U_1
obtain ⟨V, i, hV, hxV⟩ := hU x hx
no goals
case cover_preserve.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ (forget TopCat).map f x ∈ U_1
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩