C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  let_fun this := (_ : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f);
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
⊢ Mono (F.map f)
have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) (_ : 𝟙 (F.obj X) ≫ F.map f = 𝟙 (F.obj X) ≫ F.map f))
⊢ Mono (F.map f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  let_fun this := (_ : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f);
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)
simp_rw [F.map_id] at this
no goals
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) (_ : 𝟙 (F.obj X) ≫ F.map f = 𝟙 (F.obj X) ≫ F.map f))
⊢ Mono (F.map f)
apply PullbackCone.mono_of_isLimitMkIdId _ this