ExactFunctor

📁 Source: Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean

Statistics

Metric	Count
Definitions	0
Theorems exact_tfae, preservesEpimorphisms_of_preserves_shortExact_right, preservesFiniteColimits_iff_forall_exact_map_and_epi, preservesFiniteColimits_of_preservesHomology, preservesFiniteColimits_tfae, preservesFiniteLimits_iff_forall_exact_map_and_mono, preservesFiniteLimits_of_preservesHomology, preservesFiniteLimits_tfae, preservesMonomorphisms_of_preserves_shortExact_left	9
Total	9

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_tfae 📖	mathematical	—	List.TFAE PreservesHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive preservesZeroMorphisms_of_additive CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.PreservesFiniteColimits	—	preservesZeroMorphisms_of_additive List.TFAE.out preservesFiniteLimits_tfae CategoryTheory.ShortComplex.ShortExact.exact CategoryTheory.ShortComplex.ShortExact.mono_f preservesFiniteColimits_tfae CategoryTheory.ShortComplex.ShortExact.epi_g CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.zero_comp CategoryTheory.ShortComplex.exact_iff_mono map_zero CategoryTheory.Limits.comp_zero CategoryTheory.ShortComplex.exact_iff_epi preservesFiniteLimits_of_preservesHomology CategoryTheory.Abelian.has_finite_products CategoryTheory.Abelian.has_kernels preservesFiniteColimits_of_preservesHomology CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Abelian.has_cokernels CategoryTheory.ShortComplex.Exact.map PreservesHomology.preservesLeftHomologyOf preservesHomologyOfExact PreservesHomology.preservesRightHomologyOf List.tfae_of_cycle
preservesEpimorphisms_of_preserves_shortExact_right 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map preservesZeroMorphisms_of_additive CategoryTheory.Epi obj CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ map CategoryTheory.ShortComplex.g	PreservesEpimorphisms	—	preservesZeroMorphisms_of_additive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ShortComplex.exact_kernel CategoryTheory.Limits.equalizer.ι_mono
preservesFiniteColimits_iff_forall_exact_map_and_epi 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map preservesZeroMorphisms_of_additive CategoryTheory.Epi obj CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ map CategoryTheory.ShortComplex.g	—	List.TFAE.out preservesZeroMorphisms_of_additive preservesFiniteColimits_tfae
preservesFiniteColimits_of_preservesHomology 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits	—	preservesZeroMorphisms_of_additive PreservesHomology.preservesCokernel CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels CategoryTheory.Limits.IsZero.iff_id_eq_zero map_id CategoryTheory.Limits.id_zero map_zero preservesFiniteColimits_of_preservesCokernels
preservesFiniteColimits_tfae 📖	mathematical	—	List.TFAE CategoryTheory.Limits.PreservesFiniteColimits	—	preservesZeroMorphisms_of_additive preservesEpimorphisms_of_preserves_shortExact_right CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.image_ι_comp_eq_zero CategoryTheory.ShortComplex.zero map_comp CategoryTheory.Abelian.image.fac CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono map_epi CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.IsIso.id CategoryTheory.instMonoId CategoryTheory.ShortComplex.exact_iff_exact_image_ι CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.ShortComplex.exact_cokernel CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory preservesFiniteColimits_of_preservesCokernels CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Abelian.hasCoequalizers CategoryTheory.Abelian.hasZeroObject CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit List.tfae_of_cycle
preservesFiniteLimits_iff_forall_exact_map_and_mono 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map preservesZeroMorphisms_of_additive CategoryTheory.Mono obj CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ map CategoryTheory.ShortComplex.f	—	List.TFAE.out preservesZeroMorphisms_of_additive preservesFiniteLimits_tfae
preservesFiniteLimits_of_preservesHomology 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits	—	preservesZeroMorphisms_of_additive PreservesHomology.preservesKernel CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Preadditive.hasEqualizers_of_hasKernels CategoryTheory.Limits.IsZero.iff_id_eq_zero map_id CategoryTheory.Limits.id_zero map_zero preservesFiniteLimits_of_preservesKernels
preservesFiniteLimits_tfae 📖	mathematical	—	List.TFAE CategoryTheory.Limits.PreservesFiniteLimits	—	preservesZeroMorphisms_of_additive preservesMonomorphisms_of_preserves_shortExact_left CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.comp_coimage_π_eq_zero CategoryTheory.ShortComplex.zero CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id map_comp CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.cokernel.π_desc CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono CategoryTheory.instEpiId CategoryTheory.IsIso.id map_mono CategoryTheory.Abelian.instMonoFactorThruCoimage CategoryTheory.ShortComplex.exact_iff_exact_coimage_π CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.comp_zero CategoryTheory.ShortComplex.exact_kernel CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory preservesFiniteLimits_of_preservesKernels CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Abelian.has_finite_products CategoryTheory.Abelian.hasEqualizers CategoryTheory.Abelian.hasZeroObject CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit List.tfae_of_cycle
preservesMonomorphisms_of_preserves_shortExact_left 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map preservesZeroMorphisms_of_additive CategoryTheory.Mono obj CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ map CategoryTheory.ShortComplex.f	PreservesMonomorphisms	—	preservesZeroMorphisms_of_additive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.ShortComplex.exact_cokernel CategoryTheory.Limits.coequalizer.π_epi

---

← Back to Index