Theorems · Definition · category theory

CategoryTheory.NonPreadditiveAbelian.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {toHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms C} →
        {toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C} →
          {toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C} →
            {has_zero_object : CategoryTheory.Limits.HasZeroObject C} →
              {has_kernels : CategoryTheory.Limits.HasKernels C} →
                {has_cokernels : CategoryTheory.Limits.HasCokernels C} →
                  {has_finite_products : CategoryTheory.Limits.HasFiniteProducts C} →
                    {has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C} →
                      {toHasZeroMorphisms' : CategoryTheory.Limits.HasZeroMorphisms C} →
                        {toIsNormalMonoCategory' : CategoryTheory.IsNormalMonoCategory C} →
                          {toIsNormalEpiCategory' : CategoryTheory.IsNormalEpiCategory C} →
                            {has_zero_object' : CategoryTheory.Limits.HasZeroObject C} →
                              {has_kernels' : CategoryTheory.Limits.HasKernels C} →
                                {has_cokernels' : CategoryTheory.Limits.HasCokernels C} →
                                  {has_finite_products' : CategoryTheory.Limits.HasFiniteProducts C} →
                                    {has_finite_coproducts' : CategoryTheory.Limits.HasFiniteCoproducts C} →
                                      { toHasZeroMorphisms := toHasZeroMorphisms,
                                            toIsNormalMonoCategory := toIsNormalMonoCategory,
                                            toIsNormalEpiCategory := toIsNormalEpiCategory,
                                            has_zero_object := has_zero_object, has_kernels := has_kernels,
                                            has_cokernels := has_cokernels, has_finite_products := has_finite_products,
                                            has_finite_coproducts := has_finite_coproducts } =
                                          { toHasZeroMorphisms := toHasZeroMorphisms',
                                            toIsNormalMonoCategory := toIsNormalMonoCategory',
                                            toIsNormalEpiCategory := toIsNormalEpiCategory',
                                            has_zero_object := has_zero_object', has_kernels := has_kernels',
                                            has_cokernels := has_cokernels',
                                            has_finite_products := has_finite_products',
                                            has_finite_coproducts := has_finite_coproducts' } →
                                        (toHasZeroMorphisms ≍ toHasZeroMorphisms' → P) → P

Defined in

Mathlib.CategoryTheory.Abelian.NonPreadditive

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms