kernelOrderHom — Mathlib

English

Kernels define an order-reversing map from Subobject(op X) to Subobject(X).

Русский

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

LaTeX

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

Lean4

/-- Taking kernels is an order-reversing map from the quotient objects of `X` to the subobjects of
`X`. -/
@[simps]
def kernelOrderHom [HasKernels C] (X : C) : (Subobject (op X))ᵒᵈ →o Subobject X
    where
  toFun :=
    Subobject.lift (fun _ f _ => Subobject.mk (kernel.ι f.unop))
      (by
        rintro A B f g hf hg i rfl
        refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_
        ·
          exact
            IsLimit.conePointUniqueUpToIso (limit.isLimit _)
              (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom rfl)
        · dsimp
          simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp, Fork.ofι_π_app])
  monotone' :=
    Subobject.ind₂ _ <| by
      intro A B f g hf hg h
      dsimp only [Subobject.lift_mk]
      refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_
      · rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
      · exact Quiver.Hom.op_inj (by simp)

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