Exact

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

Statistics

Metric	Count
Definitions Exact, isColimitCoimage, isColimitImage, isLimitImage, isLimitImage'	5
Theorems tfae_epi, tfae_mono, preservesEpimorphisms_of_map_exact, preservesHomology_of_map_exact, preservesHomology_of_preservesEpis_and_kernels, preservesHomology_of_preservesMonos_and_cokernels, preservesMonomorphisms_of_map_exact, reflects_exact_of_faithful, isIso_imageToKernel, isIso_imageToKernel', exact_cokernel, exact_iff_epi_imageToKernel, exact_iff_epi_imageToKernel', exact_iff_exact_coimage_π, exact_iff_exact_image_ι, exact_iff_image_eq_kernel, exact_iff_isIso_imageToKernel, exact_iff_isIso_imageToKernel', exact_iff_of_forks, exact_kernel	20
Total	25

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tfae_epi 📖	mathematical	—	List.TFAE CategoryTheory.Epi Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.Exact CategoryTheory.Limits.comp_zero	—	CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels epi_of_cokernel_π_eq_zero CategoryTheory.cancel_epi CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.ShortComplex.exact_iff_epi hasZeroObject List.tfae_of_cycle
tfae_mono 📖	mathematical	—	List.TFAE CategoryTheory.Mono Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.Exact CategoryTheory.Limits.zero_comp	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels mono_of_kernel_ι_eq_zero CategoryTheory.cancel_mono CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.ShortComplex.exact_iff_mono hasZeroObject List.tfae_of_cycle

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesEpimorphisms_of_map_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map	PreservesEpimorphisms	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.comp_zero List.TFAE.out CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.tfae_epi CategoryTheory.ShortComplex.exact_of_iso CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id map_zero
preservesHomology_of_map_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map	PreservesHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesMonomorphisms_of_map_exact CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero map_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian preservesEpimorphisms_of_map_exact CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp map_epi CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.ShortComplex.exact_of_g_is_cokernel
preservesHomology_of_preservesEpis_and_kernels 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	PreservesHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesHomology_of_map_exact CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Abelian.image_ι_comp_eq_zero CategoryTheory.ShortComplex.zero CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.has_kernels CategoryTheory.Category.comp_id map_comp CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.kernel.lift_ι 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_of_f_is_kernel CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.ShortComplex.exact_iff_exact_image_ι CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
preservesHomology_of_preservesMonos_and_cokernels 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	PreservesHomology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesHomology_of_map_exact CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Abelian.comp_coimage_π_eq_zero CategoryTheory.ShortComplex.zero CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.has_cokernels 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_of_g_is_cokernel CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.ShortComplex.exact_iff_exact_coimage_π CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
preservesMonomorphisms_of_map_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map	PreservesMonomorphisms	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.zero_comp List.TFAE.out CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.tfae_mono CategoryTheory.ShortComplex.exact_of_iso CategoryTheory.Limits.comp_zero map_zero CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
reflects_exact_of_faithful 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian zero_of_map_zero map_comp CategoryTheory.Limits.kernel.condition map_zero CategoryTheory.Limits.cokernel.condition CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
Exact 📖	CompData	179 math math: HomologyData.exact_iff, SnakeInput.exact_C₃_up, SnakeInput.L₀'_exact, Splitting.exact, CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_exact, CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact, exact_iff_of_epi_of_isIso_of_mono, SnakeInput.L₃_exact, groupHomology.H1CoresCoinf_exact, SnakeInput.exact_C₁_up, SnakeInput.L₁_exact, LeftHomologyData.exact_iff_epi_f', exact_iff_iCycles_pOpcycles_zero, exact_iff_kernel_ι_comp_cokernel_π_zero, CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', groupCohomology.mapShortComplex₃_exact, exact_and_mono_f_iff_of_iso, exact_iff_isIso_imageToKernel', DerivedCategory.HomologySequence.exact₂, CategoryTheory.IsPullback.exact_shortComplex', CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_exact, TopCat.Sheaf.exact_iff_stalkFunctor_map_exact, CategoryTheory.Abelian.tfae_epi, SnakeInput.exact_C₂_down, kernelSequence_exact, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_exact, ShortExact.exact, CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact, Module.Flat.lTensor_shortComplex_exact, exact_op_iff, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂', Profinite.NobelingProof.succ_exact, exact_unop_iff, RightHomologyData.exact_iff, exact_iff_exact_image_ι, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_exact, exact_iff_isIso_imageToKernel, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', Module.Flat.iff_rTensor_preserves_shortComplex_exact, CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_exact, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', CochainComplex.homologyMap_exact₃_of_distTriang, CochainComplex.homologyMap_exact₂_of_distTriang, exact_iff_surjective_abToCycles, Module.Flat.iff_lTensor_preserves_shortComplex_exact, exact_iff_of_hasForget, ab_exact_iff_function_exact, exact_cokernel, CategoryTheory.Abelian.SpectralObject.exact₂, Exact.map_of_epi_of_preservesCokernel, groupHomology.mapShortComplex₃_exact, exact_of_g_is_cokernel, LeftHomologyData.exact_map_iff, CochainComplex.homologyMap_exact₁_of_distTriang, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_exact, exact_iff_isZero_homology, HomologicalComplex.exactAt_iff, CategoryTheory.Functor.homologySequence_exact₂, SnakeInput.L₀_exact, exact_iff_of_iso, CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi, Exact.map, ChainComplex.isIso_descOpcycles_iff, exact_kernel, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_exact, Exact.shortExact, exact_iff_epi_toCycles, exact_and_epi_g_iff_g_is_cokernel, exact_iff_exact_toComposableArrows, groupCohomology.mapShortComplex₂_exact, CategoryTheory.JointlyReflectIsomorphisms.exact_iff, SnakeInput.exact_C₂_up, HomologicalComplex.opcycles_right_exact, CategoryTheory.Functor.homologySequence_exact₃, quasiIso_iff_of_zeros', Exact.unop, ModuleCat.uliftFunctor_map_exact, quasiIso_iff_of_zeros, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact, exact_iff_i_p_zero, ab_exact_iff_ker_le_range, ShortExact.moduleCat_exact_iff_function_exact, CategoryTheory.ProjectiveResolution.exact_succ, CochainComplex.isIso_liftCycles_iff, HomologicalComplex.cycles_left_exact, exact_of_iso, SnakeInput.L₁'_exact, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂', CategoryTheory.Limits.colim.exact_mapShortComplex, exact_iff_surjective_moduleCatToCycles, RightHomologyData.exact_iff_mono_g', exact_iff_mono, exact_iff_exact_up_to_refinements, ab_exact_iff, groupHomology.shortComplexH0_exact, exact_iff_isZero_leftHomology, ShortExact.homology_exact₃, HomologyData.exact_iff_i_p_zero, DerivedCategory.HomologySequence.exact₁, CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono, moduleCat_exact_iff_ker_sub_range, moduleCat_exact_iff, CategoryTheory.Abelian.SpectralObject.exact₃, groupHomology.mapShortComplex₂_exact, groupCohomology.mapShortComplex₁_exact, exact_and_epi_g_iff_of_iso, RightHomologyData.exact_map_iff, cokernelSequence_exact, exact_iff_mono_cokernel_desc, exact_and_mono_f_iff_f_is_kernel, CategoryTheory.Functor.map_distinguished_exact, CategoryTheory.ComposableArrows.exact₂_iff, SnakeInput.L₂'_exact, HomologicalComplex.exact_of_degreewise_exact, exact_iff_epi_imageToKernel, groupHomology.H1CoresCoinfOfTrivial_exact, groupHomology.mapShortComplex₁_exact, CategoryTheory.Functor.homologySequence_exact₁, exact_iff_image_eq_kernel, Exact.op, exact_of_f_is_kernel, groupCohomology.H1InfRes_exact, moduleCat_exact_iff_range_eq_ker, exact_iff_epi_kernel_lift, CategoryTheory.ComposableArrows.Exact.exact', LeftHomologyData.exact_iff, CategoryTheory.ProjectiveResolution.exact₀, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_exact, CategoryTheory.IsPushout.exact_shortComplex, CategoryTheory.Abelian.SpectralObject.dCokernelSequence_exact, SnakeInput.exact_C₃_down, CategoryTheory.Functor.IsHomological.exact, QuasiIso.exact_iff, ModuleCat.shortComplex_exact, exact_iff_homology_iso_zero, exact_map_iff_of_faithful, CategoryTheory.Abelian.tfae_mono, exact_iff_mono_fromOpcycles, exact_iff_exact_coimage_π, ModuleCat.localizedModuleFunctor_map_exact, CategoryTheory.InjectiveResolution.exact_succ, exact_iff_isZero_rightHomology, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', groupCohomology.shortComplexH0_exact, exact_iff_of_forks, ShortExact.homology_exact₁, ab_exact_iff_range_eq_ker, CategoryTheory.InjectiveResolution.exact₀, SnakeInput.L₂_exact, SnakeInput.exact_C₁_down, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_exact, CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_exact, CategoryTheory.Abelian.SpectralObject.exact₁, exact_of_isZero_X₂, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, Exact.map_of_mono_of_preservesKernel, Exact.moduleCat_of_range_eq_ker, DerivedCategory.HomologySequence.exact₃, exact_iff_epi, CategoryTheory.exact_f_d, CategoryTheory.exact_d_f, CategoryTheory.Functor.map_distinguished_op_exact, CategoryTheory.ComposableArrows.Exact.exact, exact_iff_epi_imageToKernel', HomologicalComplex.exactAt_iff', HomologyData.exact_iff', Exact.map_of_preservesRightHomologyOf, exact_iff_exact_map_forget₂, Exact.map_of_preservesLeftHomologyOf, CategoryTheory.Functor.reflects_exact_of_faithful, ModuleCat.smulShortComplex_exact, ShortExact.homology_exact₂, HomologicalComplex.exact_iff_degreewise_exact, ShortExact.ab_exact_iff_function_exact, Module.Flat.rTensor_shortComplex_exact, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_cokernel 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π	—	exact_of_g_is_cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
exact_iff_epi_imageToKernel 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Subobject X₂ Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject X₁ f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernelSubobject X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels zero exact_iff_epi_imageToKernel' CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.epimorphisms imageToKernel'_kernelSubobjectIso
exact_iff_epi_imageToKernel' 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Epi CategoryTheory.Limits.image X₁ X₂ f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernel X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel' zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels zero exact_iff_epi_kernel_lift CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.image.fac CategoryTheory.epi_of_epi_fac CategoryTheory.epi_comp CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Preadditive.hasEqualizers_of_hasKernels
exact_iff_exact_coimage_π 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ CategoryTheory.Abelian.coimage X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι f CategoryTheory.Abelian.coimage.π CategoryTheory.Abelian.comp_coimage_π_eq_zero zero	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.comp_coimage_π_eq_zero zero exact_iff_of_epi_of_isIso_of_mono CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.condition CategoryTheory.instEpiId CategoryTheory.IsIso.id CategoryTheory.Abelian.instMonoFactorThruCoimage
exact_iff_exact_image_ι 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.image X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π X₃ CategoryTheory.Abelian.image.ι g CategoryTheory.Abelian.image_ι_comp_eq_zero zero	—	exact_iff_of_epi_of_isIso_of_mono CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.image_ι_comp_eq_zero zero CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.IsIso.id CategoryTheory.instMonoId
exact_iff_image_eq_kernel 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.imageSubobject X₁ X₂ f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernelSubobject X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels zero exact_iff_isIso_imageToKernel CategoryTheory.Subobject.eq_of_comm imageToKernel_arrow Eq.ge CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Category.assoc CategoryTheory.Subobject.ofLE_arrow CategoryTheory.Category.id_comp
exact_iff_isIso_imageToKernel 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject X₂ Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject X₁ f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernelSubobject X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels zero exact_iff_epi_imageToKernel CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory instMonoImageToKernel CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso
exact_iff_isIso_imageToKernel' 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.IsIso CategoryTheory.Limits.image X₁ X₂ f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernel X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel' zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels zero exact_iff_epi_imageToKernel' CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Limits.kernel.lift_mono CategoryTheory.Limits.instMonoι
exact_iff_of_forks 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cocone.pt X₁ f CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels exact_iff_kernel_ι_comp_cokernel_π_zero CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Category.assoc CategoryTheory.Preadditive.IsIso.comp_left_eq_zero CategoryTheory.Iso.isIso_inv CategoryTheory.Preadditive.IsIso.comp_right_eq_zero CategoryTheory.Iso.isIso_hom
exact_kernel 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.ι	—	exact_of_f_is_kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian

CategoryTheory.ShortComplex.Exact

Definitions

Name	Category	Theorems
isColimitCoimage 📖	CompOp	—
isColimitImage 📖	CompOp	—
isLimitImage 📖	CompOp	—
isLimitImage' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_imageToKernel 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernelSubobject CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel CategoryTheory.ShortComplex.zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel
isIso_imageToKernel' 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.IsIso CategoryTheory.Limits.image CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels imageToKernel' CategoryTheory.ShortComplex.zero	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel'

---

← Back to Index