C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
⊢ Functor.op (Opens.map (𝟙 X)) ⋙ ℱ = ℱ
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
⊢ 𝟙 X _* ℱ = ℱ
unfold pushforwardObj
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
⊢ Functor.op (𝟭 (Opens ↑X)) ⋙ ℱ = ℱ
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
⊢ Functor.op (Opens.map (𝟙 X)) ⋙ ℱ = ℱ
rw [Opens.map_id_eq]
no goals
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
⊢ Functor.op (𝟭 (Opens ↑X)) ⋙ ℱ = ℱ
erw [Functor.id_comp]