Opposite

📁 Source: Mathlib/CategoryTheory/Abelian/Opposite.lean

Statistics

Metric	Count
Definitions cokernelOpOp, cokernelOpUnop, cokernelUnopOp, cokernelUnopUnop, imageOpOp, imageOpUnop, imageUnopOp, imageUnopUnop, instAbelianOpposite, kernelOpOp, kernelOpUnop, kernelUnopOp, kernelUnopUnop	13
Theorems π_op, π_unop, cokernelOpOp_hom, cokernelOpOp_inv, cokernelOpUnop_hom, cokernelOpUnop_inv, cokernelUnopOp_hom, cokernelUnopOp_inv, cokernelUnopUnop_hom, cokernelUnopUnop_inv, factorThruImage_comp_imageUnopOp_inv, imageUnopOp_hom_comp_image_ι, imageUnopOp_inv_comp_op_factorThruImage, image_ι_op_comp_imageUnopOp_hom, ι_op, ι_unop, kernelOpOp_hom, kernelOpOp_inv, kernelOpUnop_hom, kernelOpUnop_inv, kernelUnopOp_hom, kernelUnopOp_inv, kernelUnopUnop_hom, kernelUnopUnop_inv	24
Total	37

CategoryTheory

Definitions

Name	Category	Theorems
cokernelOpOp 📖	CompOp	2 math math: cokernelOpOp_hom, cokernelOpOp_inv
cokernelOpUnop 📖	CompOp	3 math math: cokernel.π_op, cokernelOpUnop_inv, cokernelOpUnop_hom
cokernelUnopOp 📖	CompOp	3 math math: cokernelUnopOp_hom, cokernel.π_unop, cokernelUnopOp_inv
cokernelUnopUnop 📖	CompOp	2 math math: cokernelUnopUnop_inv, cokernelUnopUnop_hom
imageOpOp 📖	CompOp	1 math math: imageToKernel_op
imageOpUnop 📖	CompOp	—
imageUnopOp 📖	CompOp	4 math math: image_ι_op_comp_imageUnopOp_hom, factorThruImage_comp_imageUnopOp_inv, imageUnopOp_hom_comp_image_ι, imageUnopOp_inv_comp_op_factorThruImage
imageUnopUnop 📖	CompOp	1 math math: imageToKernel_unop
instAbelianOpposite 📖	CompOp	34 math math: kernelUnopOp_inv, ShortComplex.SnakeInput.op_δ, imageToKernel_unop, cokernelUnopUnop_inv, kernelOpUnop_hom, ShortComplex.SnakeInput.op_L₂, ShortComplex.SnakeInput.op_v₁₂, imageToKernel_op, cokernelOpOp_hom, image_ι_op_comp_imageUnopOp_hom, kernelUnopUnop_inv, kernelOpUnop_inv, cokernelUnopOp_hom, cokernel.π_unop, factorThruImage_comp_imageUnopOp_inv, ShortComplex.SnakeInput.op_L₀, kernelUnopOp_hom, cokernel.π_op, cokernelOpUnop_inv, kernel.ι_unop, ShortComplex.SnakeInput.op_L₃, kernelUnopUnop_hom, ShortComplex.SnakeInput.op_v₂₃, ShortComplex.SnakeInput.op_v₀₁, cokernelUnopUnop_hom, imageUnopOp_hom_comp_image_ι, cokernelOpUnop_hom, kernel.ι_op, ShortComplex.SnakeInput.op_L₁, kernelOpOp_inv, cokernelUnopOp_inv, kernelOpOp_hom, imageUnopOp_inv_comp_op_factorThruImage, cokernelOpOp_inv
kernelOpOp 📖	CompOp	3 math math: imageToKernel_op, kernelOpOp_inv, kernelOpOp_hom
kernelOpUnop 📖	CompOp	3 math math: kernelOpUnop_hom, kernelOpUnop_inv, kernel.ι_op
kernelUnopOp 📖	CompOp	3 math math: kernelUnopOp_inv, kernelUnopOp_hom, kernel.ι_unop
kernelUnopUnop 📖	CompOp	3 math math: imageToKernel_unop, kernelUnopUnop_inv, kernelUnopUnop_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernelOpOp_hom 📖	mathematical	—	Iso.hom Opposite Category.opposite Limits.cokernel Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite Limits.kernel Limits.HasKernels.has_limit Abelian.has_kernels cokernelOpOp Limits.cokernel.desc Limits.kernel.ι	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelOpOp_inv 📖	mathematical	—	Iso.inv Opposite Category.opposite Limits.cokernel Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite Limits.kernel Limits.HasKernels.has_limit Abelian.has_kernels cokernelOpOp Opposite.unop Limits.kernel.lift Quiver.Hom.unop Limits.cokernel.π	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelOpUnop_hom 📖	mathematical	—	Iso.hom Opposite.unop Limits.cokernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite Limits.kernel Limits.HasKernels.has_limit Abelian.has_kernels cokernelOpUnop Limits.kernel.lift Quiver.Hom.unop Limits.cokernel.π	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelOpUnop_inv 📖	mathematical	—	Iso.inv Opposite.unop Limits.cokernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite Limits.kernel Limits.HasKernels.has_limit Abelian.has_kernels cokernelOpUnop Quiver.Hom.unop Limits.cokernel.desc Limits.kernel.ι	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelUnopOp_hom 📖	mathematical	—	Iso.hom Opposite Category.opposite Opposite.op Limits.cokernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.kernel Limits.hasZeroMorphismsOpposite Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite cokernelUnopOp Limits.kernel.lift Quiver.Hom.op Limits.cokernel.π	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelUnopOp_inv 📖	mathematical	—	Iso.inv Opposite Category.opposite Opposite.op Limits.cokernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.kernel Limits.hasZeroMorphismsOpposite Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite cokernelUnopOp Quiver.Hom.op Limits.cokernel.desc Limits.kernel.ι	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelUnopUnop_hom 📖	mathematical	—	Iso.hom Limits.cokernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.kernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite cokernelUnopUnop Limits.cokernel.desc Limits.kernel.ι	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
cokernelUnopUnop_inv 📖	mathematical	—	Iso.inv Limits.cokernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.kernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite cokernelUnopUnop Opposite.op Limits.kernel.lift Quiver.Hom.op Limits.cokernel.π	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.HasKernels.has_limit Abelian.has_kernels
factorThruImage_comp_imageUnopOp_inv 📖	mathematical	—	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Limits.image Category.opposite Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations instAbelianOpposite Opposite.op Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Limits.factorThruImage Iso.inv imageUnopOp Quiver.Hom.op Limits.image.ι	—	Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations Iso.comp_inv_eq image_ι_op_comp_imageUnopOp_hom
imageUnopOp_hom_comp_image_ι 📖	mathematical	—	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Opposite.op Limits.image Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations Category.opposite instAbelianOpposite Iso.hom imageUnopOp Limits.image.ι Quiver.Hom.op Limits.factorThruImage	—	Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations cancel_epi op_epi_of_mono Limits.instMonoι image_ι_op_comp_imageUnopOp_hom Limits.image.fac
imageUnopOp_inv_comp_op_factorThruImage 📖	mathematical	—	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Limits.image Category.opposite Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations instAbelianOpposite Opposite.op Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Iso.inv imageUnopOp Quiver.Hom.op Limits.factorThruImage Limits.image.ι	—	Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations Iso.inv_comp_eq imageUnopOp_hom_comp_image_ι
image_ι_op_comp_imageUnopOp_hom 📖	mathematical	—	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Opposite.op Opposite.unop Limits.image Quiver.Hom.unop CategoryStruct.toQuiver Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations Category.opposite instAbelianOpposite Quiver.Hom.op Limits.image.ι Iso.hom imageUnopOp Limits.factorThruImage	—	Limits.HasImages.has_image Limits.hasImages_of_hasStrongEpiMonoFactorisations Abelian.instHasStrongEpiMonoFactorisations cokernel.π_unop Limits.hasCokernel_epi_comp Limits.hasCokernel_comp_iso Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels Abelian.coimageIsoImage'_hom Category.assoc Abelian.imageIsoImage_hom_comp_image_ι Limits.kernel.lift_ι Limits.cokernelIsoOfEq_hom_comp_desc_assoc Limits.cokernel.π_desc_assoc Limits.cokernel.π_desc IsIso.id IsIso.inv_id Category.id_comp
kernelOpOp_hom 📖	mathematical	—	Iso.hom Opposite Category.opposite Limits.kernel Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite Limits.cokernel Limits.HasCokernels.has_colimit Abelian.has_cokernels kernelOpOp Opposite.unop Limits.cokernel.desc Quiver.Hom.unop Limits.kernel.ι	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelOpOp_inv 📖	mathematical	—	Iso.inv Opposite Category.opposite Limits.kernel Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite Limits.cokernel Limits.HasCokernels.has_colimit Abelian.has_cokernels kernelOpOp Limits.kernel.lift Limits.cokernel.π	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelOpUnop_hom 📖	mathematical	—	Iso.hom Opposite.unop Limits.kernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite Limits.cokernel Limits.HasCokernels.has_colimit Abelian.has_cokernels kernelOpUnop Quiver.Hom.unop Limits.kernel.lift Limits.cokernel.π	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelOpUnop_inv 📖	mathematical	—	Iso.inv Opposite.unop Limits.kernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels instAbelianOpposite Limits.cokernel Limits.HasCokernels.has_colimit Abelian.has_cokernels kernelOpUnop Limits.cokernel.desc Quiver.Hom.unop Limits.kernel.ι	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelUnopOp_hom 📖	mathematical	—	Iso.hom Opposite Category.opposite Opposite.op Limits.kernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels Limits.cokernel Limits.hasZeroMorphismsOpposite Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite kernelUnopOp Quiver.Hom.op Limits.kernel.lift Limits.cokernel.π	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelUnopOp_inv 📖	mathematical	—	Iso.inv Opposite Category.opposite Opposite.op Limits.kernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels Limits.cokernel Limits.hasZeroMorphismsOpposite Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite kernelUnopOp Limits.cokernel.desc Quiver.Hom.op Limits.kernel.ι	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelUnopUnop_hom 📖	mathematical	—	Iso.hom Limits.kernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels Limits.cokernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite kernelUnopUnop Opposite.op Limits.cokernel.desc Quiver.Hom.op Limits.kernel.ι	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels
kernelUnopUnop_inv 📖	mathematical	—	Iso.inv Limits.kernel Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasKernels.has_limit Abelian.has_kernels Limits.cokernel Opposite Category.opposite Limits.hasZeroMorphismsOpposite Limits.HasCokernels.has_colimit Abelian.has_cokernels instAbelianOpposite kernelUnopUnop Limits.kernel.lift Limits.cokernel.π	—	Limits.HasKernels.has_limit Abelian.has_kernels Limits.HasCokernels.has_colimit Abelian.has_cokernels

CategoryTheory.cokernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
π_op 📖	mathematical	—	Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Limits.cokernel Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Quiver.Hom.op CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.instAbelianOpposite CategoryTheory.Limits.cokernel.π CategoryTheory.CategoryStruct.comp Opposite.unop CategoryTheory.Limits.kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom CategoryTheory.cokernelOpUnop CategoryTheory.Limits.kernel.ι CategoryTheory.eqToHom Opposite.unop_op	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels Opposite.unop_op CategoryTheory.Category.comp_id CategoryTheory.Limits.kernel.lift_ι
π_unop 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Quiver.Hom.unop CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op CategoryTheory.Limits.kernel CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.instAbelianOpposite CategoryTheory.Iso.hom CategoryTheory.cokernelUnopOp CategoryTheory.Limits.kernel.ι CategoryTheory.eqToHom Opposite.op_unop	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels Opposite.op_unop CategoryTheory.Category.comp_id CategoryTheory.Limits.kernel.lift_ι

CategoryTheory.kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_op 📖	mathematical	—	Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Opposite.op Quiver.Hom.op CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.instAbelianOpposite CategoryTheory.Limits.kernel.ι CategoryTheory.CategoryStruct.comp Opposite.unop CategoryTheory.eqToHom Opposite.unop_op CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π CategoryTheory.Iso.inv CategoryTheory.kernelOpUnop	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels Opposite.unop_op CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Category.id_comp
ι_unop 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Opposite.unop Quiver.Hom.unop CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.ι CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op CategoryTheory.eqToHom Opposite.op_unop CategoryTheory.Limits.cokernel CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.instAbelianOpposite CategoryTheory.Limits.cokernel.π CategoryTheory.Iso.inv CategoryTheory.kernelUnopOp	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels Opposite.op_unop CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Category.id_comp

---

← Back to Index