case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ PullbackCone.fst (IsPullback.cone h) = 𝟙 X
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ Mono f
obtain ⟨l, h₁, h₂⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit (𝟙 _) (𝟙 _) (by simp [h.w])
case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ PullbackCone.fst (IsPullback.cone h) = 𝟙 X
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁
case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ Mono f
case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
rw [h₁, IsIso.inv_comp_eq, Category.comp_id] at h₂
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
case mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ Mono f
constructor
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
intro Z g₁ g₂ e
case mk.intro.right_cancellation.mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ PullbackCone.fst (IsPullback.cone h)) ≫ f = (l' ≫ PullbackCone.snd (IsPullback.cone h)) ≫ f
⊢ l' ≫ PullbackCone.fst (IsPullback.cone h) = l' ≫ PullbackCone.snd (IsPullback.cone h)
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e
no goals
case mk.intro.right_cancellation.mk.intro
C : Type u
inst✝¹ : Category C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ PullbackCone.fst (IsPullback.cone h)) ≫ f = (l' ≫ PullbackCone.snd (IsPullback.cone h)) ≫ f
⊢ l' ≫ PullbackCone.fst (IsPullback.cone h) = l' ≫ PullbackCone.snd (IsPullback.cone h)
rw [IsPullback.cone_fst, h₂]
no goals
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f
simp [h.w]