English
The cokernel cofork is a colimit; i.e., cokerφ satisfies the universal property of a cokernel in TopModuleCat(R).
Русский
Кокernel кофоркум является колимитом, то есть cokerφ удовлетворяет универсальному свойству кокernel в TopModuleCat(R).
LaTeX
$$IsColimit (CokernelCofork.ofπ (cokerπ φ) ...)$$
Lean4
/-- `TopModuleCat.coker` is indeed the cokernel in `TopModuleCat R`. -/
def isColimitCoker : IsColimit (CokernelCofork.ofπ (cokerπ φ) (comp_cokerπ φ)) :=
isColimitAux (.ofπ (cokerπ φ) (comp_cokerπ φ))
(fun s ↦
ofHom <|
{ toLinearMap :=
(LinearMap.range φ.hom).liftQ s.π.hom.toLinearMap
(LinearMap.range_le_ker_iff.mpr <|
show (φ ≫ s.π).hom.toLinearMap = 0 by rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero])
cont := Continuous.quotient_lift s.π.hom.2 _ })
(fun s ↦ rfl) (fun s m h ↦ by dsimp at h ⊢; rw [← cancel_epi (cokerπ φ), h]; rfl)
