cokernelOrderHom — Mathlib

English

Cokernels define an order-reversing map from subobjects of X to subobjects of op X, i.e. a contravariant order-preserving assignment between Subobject X and Subobject(op X).

Русский

Коканалии задают отображение обратного порядка от подобъектов X к подобъектам(op X).

LaTeX

$$$\mathrm{cokernelOrderHom}[HasCokernels](X) : \mathrm{Subobject}(X) \to^{\mathrm{ord}} \mathrm{Subobject}(\mathrm{op} \, X)^{\mathrm{op}}$$$

Lean4

/-- Taking cokernels is an order-reversing map from the subobjects of `X` to the quotient objects
of `X`. -/
@[simps]
def cokernelOrderHom [HasCokernels C] (X : C) : Subobject X →o (Subobject (op X))ᵒᵈ
    where
  toFun :=
    Subobject.lift (fun _ f _ => Subobject.mk (cokernel.π f).op)
      (by
        rintro A B f g hf hg i rfl
        refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)
        ·
          exact
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
                (isCokernelEpiComp (colimit.isColimit _) i.hom rfl)).symm
        ·
          simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
            colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app, coequalizer.cofork_π])
  monotone' :=
    Subobject.ind₂ _ <| by
      intro A B f g hf hg h
      dsimp only [Subobject.lift_mk]
      refine Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_
      · rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
      · exact Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)

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