hasCokernels — Mathlib

English

If i: F⋙G ≅ 1_C and G ⊣ F, then HasCokernels C.

Русский

Если i: F⋙G ≅ 1_C и G ⊣ F, то существуют коконьелы в C.

LaTeX

$$$\text{HasCokernels}(C)$$$

Lean4

/-- No point making this an instance, as it requires `i` and `adj`. -/
theorem hasCokernels (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) : HasCokernels C :=
  {
    has_colimit {X Y}
      f := by
      have : PreservesColimits G := adj.leftAdjoint_preservesColimits
      have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by simpa using NatIso.naturality_1 i f
      rw [← this]
      haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
      apply Limits.hasCokernel_epi_comp }

Похожие утверждения