Documentation Verification Report

ZeroObjects

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

Statistics

Metric	Count
Definitions `HasZeroObject`, `uniqueFrom`, `uniqueTo`, `zero'`, `zeroIsInitial`, `zeroIsTerminal`, `zeroIsoInitial`, `zeroIsoIsInitial`, `zeroIsoIsTerminal`, `zeroIsoTerminal`, `IsZero`, `from_`, `isInitial`, `isTerminal`, `iso`, `isoIsInitial`, `isoIsTerminal`, `isoZero`, `retract`, `to_`	20
Theorems `isZero`, `isZero_iff`, `isZero_iff`, `from_zero_ext`, `from_zero_ext_iff`, `hasInitial`, `hasTerminal`, `initialMonoClass`, `instEpi`, `instMono`, `instSubsingletonIsoOfNat`, `to_zero_ext`, `to_zero_ext_iff`, `zero`, `zero_to_zero_isIso`, `epi`, `eq_from`, `eq_of_src`, `eq_of_tgt`, `eq_to`, `from_eq`, `hasZeroObject`, `isIso`, `mono`, `obj`, `of_full_of_faithful_of_isZero`, `of_iso`, `op`, `to_eq`, `unique_from`, `unique_to`, `unop`, `hasZeroObject_op`, `hasZeroObject_pUnit`, `hasZeroObject_unop`, `isZero_zero`	36
Total	56

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `obj`	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category`	—	`CategoryTheory.Limits.IsZero.eq_of_src` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.IsZero.eq_of_tgt`
`isZero_iff` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category` `obj`	—	`CategoryTheory.Limits.IsZero.obj` `isZero`

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero_iff` 📖	mathematical	—	`CategoryTheory.Limits.IsZero`	—	`CategoryTheory.Limits.IsZero.of_iso`

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`HasZeroObject` 📖	CompData	35 math math: `CategoryTheory.ObjectProperty.SerreClassLocalization.hasZeroObject`, `CategoryTheory.instHasZeroObjectOppositeShift`, `DerivedCategory.instHasZeroObject`, `hasZeroObject_of_hasTerminal_object`, `AddCommGrpCat.hasZeroObject`, `CategoryTheory.instHasZeroObjectMon`, `CategoryTheory.instHasZeroObjectAddMon`, `CategoryTheory.Functor.hasZeroObject_of_additive`, `CategoryTheory.DifferentialObject.hasZeroObject`, `IsZero.hasZeroObject`, `CategoryTheory.ShortComplex.Exact.hasZeroObject`, `CategoryTheory.Grp.instHasZeroObject`, `CategoryTheory.GradedObject.hasZeroObject`, `ModuleCat.instHasZeroObject`, `HomotopyCategory.instHasZeroObject`, `AddGrpCat.hasZeroObject`, `GrpCat.instHasZeroObject`, `SemiNormedGrp.hasZeroObject`, `CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero`, `CategoryTheory.instHasZeroObjectPullbackShift`, `CategoryTheory.NonPreadditiveAbelian.has_zero_object`, `hasZeroObject_op`, `SemiNormedGrp₁.hasZeroObject`, `hasZeroObject_pUnit`, `CategoryTheory.Localization.instHasZeroObjectLocalization`, `CategoryTheory.Localization.instHasZeroObjectLocalization'`, `CommGrpCat.instHasZeroObject`, `HasZeroObject.instFunctor`, `hasZeroObject_unop`, `HomologicalComplex.instHasZeroObject`, `Rep.instHasZeroObject`, `hasZeroObject_of_hasFiniteBiproducts`, `SemimoduleCat.instHasZeroObject`, `CategoryTheory.Abelian.hasZeroObject`, `hasZeroObject_of_hasInitial_object`
`IsZero` 📖	CompData	176 math math: `CategoryTheory.ShortComplex.HomologyData.exact_iff`, `HomologicalComplex.exactAt_iff_isZero_homology`, `IsColimit.isZero_pt`, `AddCommGrpCat.isZero_iff_subsingleton`, `CategoryTheory.ObjectProperty.instIsSerreClassIsZero`, `CategoryTheory.Functor.isZero`, `HomologicalComplex.isZero_single_obj_X`, `CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁`, `HomologicalComplex.isZero_single_obj_homology`, `CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H`, `CochainComplex.isStrictlyLE_iff`, `CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj`, `ModuleCat.isZero_iff_subsingleton`, `IsZero.op`, `HomologicalComplex.isZero_stupidTrunc_X`, `HomotopyCategory.isZero_quotient_obj_iff`, `DerivedCategory.isLE_iff`, `CommGrpCat.isZero_of_subsingleton`, `DerivedCategory.isZero_of_isGE`, `KernelFork.IsLimit.isZero_of_mono`, `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le'`, `isZero_kernel_of_mono`, `CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE`, `CategoryTheory.Functor.mem_homologicalKernel_iff`, `CommGrpCat.isZero_iff_subsingleton`, `CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isZero₁₃`, `CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms`, `SemimoduleCat.isZero_iff_subsingleton`, `CategoryTheory.ShortComplex.isZero_homology_of_isZero_X₂`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint`, `HomologicalComplex.isZero_zero`, `CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le`, `CategoryTheory.ShortComplex.ShortExact.isIso_g_iff`, `CategoryTheory.Abelian.Preradical.isRadical_iff_isZero`, `IsTerminal.isZero`, `CategoryTheory.Injective.isZero_under`, `CategoryTheory.ShortComplex.Exact.condition`, `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le'`, `GrpCat.isZero_of_subsingleton`, `isIsoZero_iff_source_target_isZero`, `CategoryTheory.isZero_Tor'_succ_of_projective`, `CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂`, `isZero_zero`, `CategoryTheory.ShortComplex.RightHomologyData.exact_iff`, `CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_obj_obj`, `HomologicalComplex.IsStrictlySupported.isZero`, `DerivedCategory.isZero_of_isLE`, `HomologicalComplex.isZero_double_X`, `HomologicalComplex.isZero_stupidTrunc_iff`, `CochainComplex.isStrictlyGE_iff`, `SemiNormedGrp.isZero_of_subsingleton`, `IsZero.of_mono_zero`, `AddGrpCat.isZero_iff_subsingleton`, `CochainComplex.isZero_of_isStrictlyLE`, `IsZero.of_mono`, `HasZeroObject.zero`, `CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero`, `CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff`, `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le`, `CategoryTheory.ShortComplex.exact_iff_isZero_homology`, `CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant`, `CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGT_obj`, `IsZero.obj`, `CategoryTheory.Functor.zero_obj`, `CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE`, `HomologicalComplex.extend.isZero_X`, `CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant`, `CategoryTheory.Functor.map_isZero`, `CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃`, `CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁`, `IsInitial.isZero`, `CategoryTheory.Preadditive.epi_iff_isZero_cokernel`, `HomologicalComplex.isZero_extend_X`, `TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZero`, `CategoryTheory.Functor.isZero_iff`, `CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant`, `CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁`, `IsZero.of_epi`, `CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂`, `isZero_cokernel_of_epi`, `CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms`, `CategoryTheory.Simple.not_isZero`, `CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ`, `CategoryTheory.Triangulated.TStructure.isZero`, `CategoryTheory.Preadditive.mono_iff_isZero_kernel'`, `CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLE_obj`, `AddCommGrpCat.isZero_of_subsingleton`, `AddGrpCat.isZero_of_subsingleton`, `CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff`, `HomologicalComplex.IsStrictlySupportedOutside.isZero`, `DerivedCategory.isGE_iff`, `CochainComplex.mappingCone.isZero_X_iff`, `CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isIso₃`, `CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint`, `SemimoduleCat.isZero_of_subsingleton`, `isZero_groupCohomology_succ_of_subsingleton`, `IsZero.of_iso`, `Rep.isZero_Tor_succ_of_projective`, `CategoryTheory.ShortComplex.ShortExact.isIso_f_iff`, `CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros`, `CochainComplex.isZero_of_isStrictlyGE`, `CategoryTheory.ShortComplex.exact_iff_isZero_leftHomology`, `CategoryTheory.Iso.isZero_iff`, `IsZero.iff_isSplitEpi_eq_zero`, `CategoryTheory.Preadditive.mono_iff_isZero_kernel`, `CategoryTheory.Pretriangulated.Triangle.isZero₂_iff`, `CategoryTheory.ObjectProperty.exists_prop_of_containsZero`, `HomologicalComplex.isZero_extend_X'`, `CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj`, `CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff`, `SemimoduleCat.isZero_of_iff_subsingleton`, `CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint`, `CategoryTheory.Abelian.SpectralObject.isZero_opcycles`, `CategoryTheory.Injective.exists_presentation`, `IsZero.of_mono_eq_zero`, `CategoryTheory.projectiveDimension_eq_bot_iff`, `CategoryTheory.Biprod.isIso_inl_iff_isZero`, `GrpCat.isZero_iff_subsingleton`, `IsZero.of_full_of_faithful_of_isZero`, `CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero`, `HomotopyCategory.mem_subcategoryAcyclic_iff`, `CategoryTheory.ObjectProperty.SerreClassLocalization.isZero_obj_iff`, `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso`, `CochainComplex.isZero_of_isGE`, `CategoryTheory.Preadditive.epi_iff_isZero_cokernel'`, `HomologicalComplex.isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside`, `isZero_Ext_succ_of_projective`, `CategoryTheory.injectiveDimension_eq_bot_iff`, `CategoryTheory.ShortComplex.LeftHomologyData.exact_iff`, `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le`, `biprod_isZero_iff`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms`, `CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero`, `IsZero.of_epi_zero`, `CategoryTheory.JointlyReflectIsomorphisms.isZero_iff`, `SemiNormedGrp₁.isZero_of_subsingleton`, `AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty`, `CategoryTheory.Pretriangulated.Triangle.isZero₃_iff`, `CategoryTheory.ShortComplex.exact_iff_isZero_rightHomology`, `CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isZero₂₃`, `IsZero.iff_id_eq_zero`, `HomologicalComplex.isZero_X_of_isStrictlySupported`, `CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj`, `CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂`, `IsZero.iff_isSplitMono_eq_zero`, `CategoryTheory.ShortComplex.Exact.isZero_X₂`, `IsLimit.isZero_pt`, `CategoryTheory.ShortComplex.Exact.isZero_X₂_iff`, `CategoryTheory.Pretriangulated.Triangle.isZero₁_iff`, `CategoryTheory.Abelian.SpectralObject.isZero_cycles`, `CategoryTheory.Triangulated.TStructure.isZero_truncLE_obj_of_isGE`, `CategoryTheory.Abelian.Radical.isZero`, `HomologicalComplex.ExactAt.isZero_homology`, `CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant`, `CokernelCofork.IsColimit.isZero_of_epi`, `CategoryTheory.Abelian.Preradical.isIso_toColon_iff`, `CategoryTheory.hasInjectiveDimensionLT_zero_iff_isZero`, `CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isZero₁₂`, `IsZero.of_epi_eq_zero`, `CategoryTheory.ObjectProperty.ContainsZero.exists_zero`, `CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ`, `isZero_groupHomology_succ_of_subsingleton`, `IsZero.unop`, `CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂`, `CategoryTheory.ShortComplex.HomologyData.exact_iff'`, `CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁`, `CategoryTheory.isZero_Tor_succ_of_projective`, `CategoryTheory.ObjectProperty.instContainsZeroIsZeroOfHasZeroObject`, `AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace`, `CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso`, `HomologicalComplex.isZero_single_comp_eval`, `CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le`, `ModuleCat.isZero_of_subsingleton`, `ModuleCat.isZero_of_iff_subsingleton`, `CochainComplex.isZero_of_isLE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasZeroObject_op` 📖	mathematical	—	`HasZeroObject` `Opposite` `CategoryTheory.Category.opposite`	—	`IsZero.op` `isZero_zero`
`hasZeroObject_pUnit` 📖	mathematical	—	`HasZeroObject` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Discrete.instSubsingletonDiscreteHom`
`hasZeroObject_unop` 📖	mathematical	—	`HasZeroObject`	—	`IsZero.unop` `isZero_zero`
`isZero_zero` 📖	mathematical	—	`IsZero` `HasZeroObject.zero'`	—	`HasZeroObject.zero`

CategoryTheory.Limits.HasZeroObject

Definitions

Name	Category	Theorems
`uniqueFrom` 📖	CompOp	—
`uniqueTo` 📖	CompOp	—
`zero'` 📖	CompOp	118 math math: `CategoryTheory.Limits.zero_of_from_zero`, `CategoryTheory.Triangulated.TStructure.instIsGEOfNat`, `CategoryTheory.BicartesianSq.of_is_biproduct₁`, `CategoryTheory.Triangulated.TStructure.instIsLEOfNat`, `CategoryTheory.Limits.monoFactorisationZero_I`, `CategoryTheory.IsPushout.of_is_bilimit'`, `CategoryTheory.instHasProjectiveDimensionLTOfNatNat`, `HomologicalComplex.instIsStrictlySupportedOfNat`, `CategoryTheory.Limits.hasBinaryCoproduct_zero_left`, `zeroIsoIsInitial_inv`, `CategoryTheory.IsPushout.zero_top`, `CategoryTheory.zero_map`, `CategoryTheory.Limits.monoFactorisationZero_e`, `CategoryTheory.IsPullback.inr_fst`, `CategoryTheory.Limits.isoZeroOfEpiZero_hom`, `CategoryTheory.Injective.instHasLiftingPropertyOfMono`, `CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι`, `zeroIsoTerminal_inv`, `CategoryTheory.IsPullback.zero_top`, `zero_to_zero_isIso`, `CategoryTheory.ShortComplex.Splitting.leftHomologyData_H`, `CategoryTheory.Limits.isZero_zero`, `zeroIsoTerminal_hom`, `CategoryTheory.IsPushout.inl_snd'`, `CategoryTheory.BicartesianSq.of_has_biproduct₂`, `CategoryTheory.Functor.instAdditiveOfNat`, `CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H`, `CategoryTheory.Limits.monoFactorisationZero_m`, `CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom`, `CategoryTheory.IsPushout.zero_bot`, `CategoryTheory.IsPushout.zero_left`, `CategoryTheory.Limits.inr_zeroCoprodIso_hom`, `CategoryTheory.Limits.cokernel.zeroCokernelCofork_pt`, `CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst`, `CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd`, `instSubsingletonIsoOfNat`, `CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃`, `CategoryTheory.Pretriangulated.contractibleTriangle_mor₂`, `CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃`, `CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv`, `CategoryTheory.Limits.zero_of_to_zero`, `CategoryTheory.Functor.zero_obj`, `CategoryTheory.Limits.id_zero`, `CategoryTheory.IsPushout.inr_fst`, `CategoryTheory.Pretriangulated.contractible_distinguished₂`, `CategoryTheory.IsPullback.inl_snd`, `CategoryTheory.IsPushout.of_hasBinaryCoproduct`, `CategoryTheory.IsPullback.of_hasBinaryProduct`, `CategoryTheory.Limits.prodZeroIso_hom`, `CategoryTheory.projective_iff_llp_epimorphisms_zero`, `zeroIsoIsTerminal_hom`, `CategoryTheory.Functor.mapZeroObject_inv`, `CategoryTheory.Limits.coprodZeroIso_inv`, `CategoryTheory.Limits.zeroProdIso_hom`, `CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot`, `CategoryTheory.Limits.hasBinaryCoproduct_zero_right`, `CategoryTheory.Injective.zero_injective`, `CategoryTheory.ShortComplex.Splitting.leftHomologyData_π`, `CategoryTheory.IsPullback.zero_left`, `CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π`, `CategoryTheory.Pretriangulated.contractibleTriangle_obj₃`, `CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom`, `CategoryTheory.IsPushout.of_isBilimit`, `CategoryTheory.Limits.kernel.zeroKernelFork_pt`, `CategoryTheory.IsPushout.inr_fst'`, `CategoryTheory.Limits.isoZeroOfMonoZero_inv`, `CategoryTheory.instHasInjectiveDimensionLTOfNatNat`, `CategoryTheory.IsPullback.of_hasBinaryBiproduct`, `CategoryTheory.IsPushout.inl_snd`, `CategoryTheory.IsPullback.of_is_bilimit'`, `CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst`, `zeroIsoInitial_inv`, `CategoryTheory.IsPullback.inl_snd'`, `CategoryTheory.IsPullback.of_has_biproduct`, `CategoryTheory.Limits.prodZeroIso_iso_inv_snd`, `CategoryTheory.Subobject.bot_eq_zero`, `CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι`, `CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom`, `CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv`, `CategoryTheory.IsPullback.zero_bot`, `CategoryTheory.Projective.zero_projective`, `CategoryTheory.IsPullback.zero_right`, `CategoryTheory.Pretriangulated.contractibleTriangle_mor₃`, `CategoryTheory.Limits.isoZeroOfEpiZero_inv`, `CategoryTheory.Limits.zeroProdIso_inv_snd`, `CategoryTheory.IsPushout.of_hasBinaryBiproduct`, `CategoryTheory.BicartesianSq.of_is_biproduct₂`, `CategoryTheory.Triangulated.instNonemptyOctahedron`, `CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd`, `CategoryTheory.BicartesianSq.of_has_biproduct₁`, `CategoryTheory.ObjectProperty.prop_zero`, `CategoryTheory.IsPullback.of_isBilimit`, `zeroIsoIsInitial_hom`, `CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top`, `CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv`, `instMono`, `CategoryTheory.IsPushout.zero_right`, `CategoryTheory.Limits.isoZeroOfMonoZero_hom`, `CategoryTheory.ShortComplex.exact_iff_homology_iso_zero`, `instEpi`, `CategoryTheory.IsPushout.of_has_biproduct`, `CategoryTheory.Projective.instHasLiftingPropertyOfEpi`, `CategoryTheory.Limits.hasBinaryProduct_zero_right`, `zeroIsoIsTerminal_inv`, `CategoryTheory.Limits.hasBinaryProduct_zero_left`, `CategoryTheory.Limits.hasPullback_over_zero`, `CategoryTheory.IsPullback.inr_fst'`, `CategoryTheory.Limits.hasPushout_over_zero`, `CategoryTheory.ShortComplex.Splitting.rightHomologyData_H`, `CategoryTheory.Pretriangulated.contractible_distinguished₁`, `CategoryTheory.injective_iff_rlp_monomorphisms_zero`, `CategoryTheory.Functor.mapZeroObject_hom`, `CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H`, `CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom`, `zeroIsoInitial_hom`, `CategoryTheory.Limits.inr_coprodZeroIso_hom`, `CategoryTheory.Limits.zeroCoprodIso_inv`, `CategoryTheory.ShortComplex.Splitting.homologyData_iso`
`zeroIsInitial` 📖	CompOp	—
`zeroIsTerminal` 📖	CompOp	—
`zeroIsoInitial` 📖	CompOp	2 math math: `zeroIsoInitial_inv`, `zeroIsoInitial_hom`
`zeroIsoIsInitial` 📖	CompOp	2 math math: `zeroIsoIsInitial_inv`, `zeroIsoIsInitial_hom`
`zeroIsoIsTerminal` 📖	CompOp	2 math math: `zeroIsoIsTerminal_hom`, `zeroIsoIsTerminal_inv`
`zeroIsoTerminal` 📖	CompOp	2 math math: `zeroIsoTerminal_inv`, `zeroIsoTerminal_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`from_zero_ext` 📖	—	—	—	—	`CategoryTheory.Limits.IsZero.eq_of_src` `CategoryTheory.Limits.isZero_zero`
`from_zero_ext_iff` 📖	—	—	—	—	`from_zero_ext`
`hasInitial` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial`	—	`CategoryTheory.Limits.hasInitial_of_unique` `Unique.instSubsingleton`
`hasTerminal` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal`	—	`CategoryTheory.Limits.hasTerminal_of_unique` `Unique.instSubsingleton`
`initialMonoClass` 📖	mathematical	—	`CategoryTheory.Limits.InitialMonoClass`	—	`CategoryTheory.Limits.InitialMonoClass.of_isInitial` `instMono`
`instEpi` 📖	mathematical	—	`CategoryTheory.Epi` `zero'`	—	`from_zero_ext`
`instMono` 📖	mathematical	—	`CategoryTheory.Mono` `zero'`	—	`to_zero_ext`
`instSubsingletonIsoOfNat` 📖	mathematical	—	`CategoryTheory.Iso` `zero'`	—	`CategoryTheory.Iso.ext` `to_zero_ext`
`to_zero_ext` 📖	—	—	—	—	`CategoryTheory.Limits.IsZero.eq_of_tgt` `CategoryTheory.Limits.isZero_zero`
`to_zero_ext_iff` 📖	—	—	—	—	`to_zero_ext`
`zero` 📖	mathematical	—	`CategoryTheory.Limits.IsZero`	—	—
`zero_to_zero_isIso` 📖	mathematical	—	`CategoryTheory.IsIso` `zero'`	—	`Unique.instSubsingleton` `CategoryTheory.IsIso.id`

CategoryTheory.Limits.IsZero

Definitions

Name	Category	Theorems
`from_` 📖	CompOp	2 math math: `from_eq`, `eq_from`
`isInitial` 📖	CompOp	—
`isTerminal` 📖	CompOp	—
`iso` 📖	CompOp	2 math math: `CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃`, `CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃`
`isoIsInitial` 📖	CompOp	—
`isoIsTerminal` 📖	CompOp	—
`isoZero` 📖	CompOp	—
`retract` 📖	CompOp	—
`to_` 📖	CompOp	2 math math: `eq_to`, `to_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.Epi`	—	`eq_of_src`
`eq_from` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`from_`	—	`Unique.eq_default` `unique_from`
`eq_of_src` 📖	—	`CategoryTheory.Limits.IsZero`	—	—	`eq_to`
`eq_of_tgt` 📖	—	`CategoryTheory.Limits.IsZero`	—	—	`eq_from`
`eq_to` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`to_`	—	`Unique.eq_default` `unique_to`
`from_eq` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`from_`	—	`eq_from`
`hasZeroObject` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.Limits.HasZeroObject`	—	—
`isIso` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.IsIso`	—	`eq_of_src`
`mono` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.Mono`	—	`eq_of_tgt`
`obj` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.isZero` `CategoryTheory.Limits.isZero_zero` `of_iso`
`of_full_of_faithful_of_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor.obj`	`CategoryTheory.Limits.IsZero`	—	`unique_to` `unique_from`
`of_iso` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.Limits.IsZero`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_inv` `eq_of_src` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_hom` `eq_of_tgt`
`op` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`CategoryTheory.Limits.IsZero` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op`	—	`eq_of_tgt` `eq_of_src`
`to_eq` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`to_`	—	`eq_to`
`unique_from` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`Unique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`unique_to` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`Unique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`unop` 📖	mathematical	`CategoryTheory.Limits.IsZero` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.Limits.IsZero` `Opposite.unop`	—	`eq_of_tgt` `eq_of_src`

---

← Back to Index