Lean4
/-- An effective epi which has a kernel pair is a regular epi. -/
noncomputable instance regularEpiOfEffectiveEpi {B X : C} (f : X ⟶ B) [HasPullback f f] [EffectiveEpi f] : RegularEpi f
where
W := pullback f f
left := pullback.fst f f
right := pullback.snd f f
w := pullback.condition
isColimit :=
{ desc := fun s ↦
EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦
(by
simp only [Cofork.app_one_eq_π]
rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
simp)
fac := by
intro s j
have :=
EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦
(by
simp only [Cofork.app_one_eq_π]
rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
simp)
simp only [Functor.const_obj_obj, Cofork.app_one_eq_π] at this
cases j with
| zero => simp [this]
| one => simp [this]
uniq := fun _ _ h ↦ EffectiveEpi.uniq f _ _ _ (h WalkingParallelPair.one) }
