[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T → ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
intro hT
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ (∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)) → IsLocallySurjective T
[PROOFSTEP]
intro hT
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
⊢ ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
intro x g
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
g : (forget C).obj ((stalkFunctor C x).obj 𝒢)
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = g
[PROOFSTEP]
obtain ⟨U, hxU, t, rfl⟩ := 𝒢.germ_exist x g
[GOAL]
case mp.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
rcases hT U t x hxU with
  ⟨V, ι, ⟨s, h_eq⟩, hxV⟩
    -- Then the germ of s maps to g.
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
use ℱ.germ ⟨x, hxV⟩ s
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
⊢ ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
convert stalkFunctor_map_germ_apply V ⟨x, hxV⟩ T s using 1
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
e_1✝ :
  (forget C).obj ((stalkFunctor C x).obj 𝒢) =
    (forget C).obj (Limits.colim.obj ((OpenNhds.inclusion ↑{ val := x, property := hxV }).op ⋙ 𝒢))
⊢ ↑(germ 𝒢 { val := x, property := hxU }) t =
    ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑{ val := x, property := hxV }).op ⋙ 𝒢)
          (op { obj := V, property := (_ : ↑{ val := x, property := hxV } ∈ V) }))
      (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
simpa [h_eq] using (germ_res_apply 𝒢 ι ⟨x, hxV⟩ t).symm
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
⊢ IsLocallySurjective T
[PROOFSTEP]
intro U t x hxU
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
set t_x := 𝒢.germ ⟨x, hxU⟩ t with ht_x
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
[GOAL]
case mpr.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
s_x : (forget C).obj ((stalkFunctor C x).obj ℱ)
hs_x : ↑((stalkFunctor C x).map T) s_x = t_x
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x
[GOAL]
case mpr.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
have key_W :=
  𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
    convert hs_x using 1
    symm
    convert stalkFunctor_map_germ_apply _ _ _ s
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
⊢ ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s) = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
convert hs_x using 1
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
e_1✝ :
  (fun x_1 => (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxV })) (↑(NatTrans.app T (op V)) s) =
    (fun x_1 => (forget C).obj ((stalkFunctor C x).obj 𝒢)) (↑(germ ℱ { val := x, property := hxV }) s)
⊢ ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s) =
    ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s)
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
e_1✝ :
  (fun x_1 => (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxV })) (↑(NatTrans.app T (op V)) s) =
    (fun x_1 => (forget C).obj ((stalkFunctor C x).obj 𝒢)) (↑(germ ℱ { val := x, property := hxV }) s)
⊢ ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) =
    ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
convert stalkFunctor_map_germ_apply _ _ _ s
[GOAL]
case mpr.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
key_W : ∃ W _m iU iV, ↑(𝒢.map iU.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map iV.op) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
refine' ⟨W, hWU, ⟨ℱ.map hWV.op s, _⟩, hxW⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ↑(NatTrans.app T (op W)) (↑(ℱ.map hWV.op) s) = ↑(𝒢.map hWU.op) t
[PROOFSTEP]
convert h_eq using 1
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ↑(NatTrans.app T (op W)) (↑(ℱ.map hWV.op) s) = ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
simp only [← comp_apply, T.naturality]
