[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X : Cᵒᵖ
⊢ map P (𝟙 X) = id'
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X : Cᵒᵖ
x✝ : ↑(obj P X)
⊢ ↑(map P (𝟙 X)) x✝ = ↑id' x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ map P (f ≫ g) = comp (map P g) (map P f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑(obj P X)
⊢ ↑(map P (f ≫ g)) x✝ = ↑(comp (map P g) (map P f)) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R✝ : Cᵒᵖ ⥤ RingCat
P Q R : PresheafOfModules R✝
f : Hom P Q
g : Hom Q R
x✝² : Cᵒᵖ
x✝¹ : ↑(R✝.obj x✝²)
x✝ : ↑(P.presheaf.obj x✝²)
⊢ ↑(NatTrans.app (f.hom ≫ g.hom) x✝²) (x✝¹ • x✝) = x✝¹ • ↑(NatTrans.app (f.hom ≫ g.hom) x✝²) x✝
[PROOFSTEP]
simp [Hom.map_smul]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
f g : P ⟶ Q
w : ∀ (X : Cᵒᵖ), app f X = app g X
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
g : P ⟶ Q
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝, map_smul := map_smul✝ } X = app g X
⊢ { hom := hom✝, map_smul := map_smul✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
⊢ { hom := hom✝¹, map_smul := map_smul✝¹ } = { hom := hom✝, map_smul := map_smul✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_hom
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
⊢ hom✝¹ = hom✝
[PROOFSTEP]
ext X x
[GOAL]
case mk.mk.e_hom.w.h.w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
X : Cᵒᵖ
x : ↑(P.presheaf.obj X)
⊢ ↑(NatTrans.app hom✝¹ X) x = ↑(NatTrans.app hom✝ X) x
[PROOFSTEP]
exact LinearMap.congr_fun (w X) x
