C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ ((Opens.map f).obj U.unop).op ⟶ ((Opens.map g).obj U.unop).op
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Functor.op (Opens.map f)).obj U ⟶ (Functor.op (Opens.map g)).obj U
dsimp [Functor.op]
case f
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop ⟶ (Opens.map f).obj U.unop
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ ((Opens.map f).obj U.unop).op ⟶ ((Opens.map g).obj U.unop).op
apply Quiver.Hom.op
case f.p
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop = (Opens.map f).obj U.unop
case f
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop ⟶ (Opens.map f).obj U.unop
apply eqToHom
no goals
case f.p
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop = (Opens.map f).obj U.unop
rw [h]
no goals
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (pushforwardEq h ℱ).hom.app U = ℱ.map (id (eqToHom (_ : (Opens.map g).obj U.unop = (Opens.map f).obj U.unop)).op)
simp [pushforwardEq]