Basic

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

Statistics

Metric	Count
Definitions addEquivBiprod, addEquivBiproduct, addEquiv₀, bilinearComp, biprodAddEquiv, biproductAddEquiv, chgUniv, comp, hom, hom', homAddEquiv, homEquiv, homEquiv₀, instAddCommGroup, mk₀, postcomp, precomp, extFunctor, extFunctorObj	19
Theorems addEquivBiprod_apply_fst, addEquivBiprod_apply_snd, addEquivBiprod_symm_apply, addEquiv₀_symm_apply, add_comp, add_hom, bilinearComp_apply_apply, biprodAddEquiv_apply_fst, biprodAddEquiv_apply_snd, biprodAddEquiv_symm_apply, biprod_ext, comp_add, comp_assoc, comp_assoc_of_second_deg_zero, comp_assoc_of_third_deg_zero, comp_hom, comp_mk₀_id, comp_neg, comp_sum, comp_zero, ext, ext_iff, homAddEquiv_apply, homEquiv_chgUniv, homEquiv₀_symm_apply, mk₀_add, mk₀_addEquiv₀_apply, mk₀_bijective, mk₀_comp_mk₀, mk₀_comp_mk₀_assoc, mk₀_eq_zero_iff, mk₀_hom, mk₀_homEquiv₀_apply, mk₀_id_comp, mk₀_neg, mk₀_sum, mk₀_zero, neg_comp, neg_hom, sum_comp, zero_comp, zero_hom, extFunctorObj_map, extFunctorObj_obj_coe, extFunctor_map_app, extFunctor_obj, instAdditiveAddCommGrpCatExtFunctorObj, instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, standard, hasExt_iff, hasExt_iff_small_ext, hasExt_of_hasDerivedCategory, instSmallHomDerivedCategoryObjSingleFunctorOfHasExt	53
Total	72

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasExt_iff 📖	mathematical	—	HasExt Small Quiver.Hom DerivedCategory CategoryStruct.toQuiver Category.toCategoryStruct DerivedCategory.instCategory Functor.obj DerivedCategory.singleFunctor shiftFunctor Int.instAddMonoid DerivedCategory.instHasShiftInt	—	categoryWithHomology_of_abelian Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Localization.hasSmallLocalizedShiftedHom_iff DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp small_congr le_or_gt Functor.IsEquivalence.full instIsEquivalenceShiftFunctor Functor.IsEquivalence.faithful cancel_mono mono_of_strongMono instStrongMonoOfIsRegularMono instIsRegularMonoOfIsSplitMono Functor.instIsSplitMonoApp IsSplitMono.of_iso Iso.isIso_inv cancel_epi epi_of_effectiveEpi instEffectiveEpiOfIsIso NatIso.hom_app_isIso CochainComplex.isStrictlyLE_shift CochainComplex.instIsStrictlyLEObjIntSingleFunctor CochainComplex.isStrictlyGE_shift CochainComplex.instIsStrictlyGEObjIntSingleFunctor DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE Countable.toSmall Finite.to_countable Finite.of_subsingleton
hasExt_iff_small_ext 📖	mathematical	HasExt	Small Abelian.Ext	—	small_congr IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing CanLift.prf instCanLiftIntNatCastLeOfNat
hasExt_of_hasDerivedCategory 📖	mathematical	—	HasExt	—	hasExt_iff instSmallHomOfLocallySmall locallySmall_of_univLE UnivLE.self
instSmallHomDerivedCategoryObjSingleFunctorOfHasExt 📖	mathematical	HasExt	Small Quiver.Hom DerivedCategory CategoryStruct.toQuiver Category.toCategoryStruct DerivedCategory.instCategory Functor.obj DerivedCategory.singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd categoryWithHomology_of_abelian Abelian.hasZeroObject Localization.hasSmallLocalizedShiftedHom_iff DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp small_of_injective neg_add_cancel

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
extFunctor 📖	CompOp	3 math math: extFunctor_obj, extFunctor_map_app, instAdditiveOppositeFunctorAddCommGrpCatExtFunctor
extFunctorObj 📖	CompOp	5 math math: extFunctorObj_obj_coe, extFunctorObj_map, instAdditiveAddCommGrpCatExtFunctorObj, extFunctor_obj, extFunctor_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extFunctorObj_map 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Functor.map AddCommGrpCat AddCommGrpCat.instCategory extFunctorObj AddCommGrpCat.ofHom Ext Ext.instAddCommGroup Ext.postcomp Ext.mk₀	—	—
extFunctorObj_obj_coe 📖	mathematical	CategoryTheory.HasExt	AddCommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat AddCommGrpCat.instCategory extFunctorObj Ext	—	—
extFunctor_map_app 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.NatTrans.app AddCommGrpCat AddCommGrpCat.instCategory extFunctorObj Opposite.unop CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category extFunctor AddCommGrpCat.ofHom Ext Ext.instAddCommGroup AddMonoidHom.mk' AddCommGroup.toAddGroup AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Ext.comp Ext.mk₀ Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
extFunctor_obj 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category extFunctor extFunctorObj Opposite.unop	—	—
instAdditiveAddCommGrpCatExtFunctorObj 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Functor.Additive AddCommGrpCat AddCommGrpCat.instCategory toPreadditive AddCommGrpCat.instPreadditive extFunctorObj	—	Ext.postcomp.congr_simp Ext.mk₀_add map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
instAdditiveOppositeFunctorAddCommGrpCatExtFunctor 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Functor.Additive Opposite CategoryTheory.Functor AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.instPreadditiveOpposite toPreadditive CategoryTheory.functorCategoryPreadditive AddCommGrpCat.instPreadditive extFunctor	—	CategoryTheory.NatTrans.ext' AddCommGrpCat.hom_ext AddMonoidHom.ext Ext.comp.congr_simp Ext.mk₀_add Ext.add_comp AddMonoidHom.mk'.congr_simp

CategoryTheory.Abelian.Ext

Definitions

Name	Category	Theorems
addEquivBiprod 📖	CompOp	3 math math: addEquivBiprod_symm_apply, addEquivBiprod_apply_snd, addEquivBiprod_apply_fst
addEquivBiproduct 📖	CompOp	—
addEquiv₀ 📖	CompOp	2 math math: mk₀_addEquiv₀_apply, addEquiv₀_symm_apply
bilinearComp 📖	CompOp	1 math math: bilinearComp_apply_apply
biprodAddEquiv 📖	CompOp	5 math math: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, biprodAddEquiv_apply_fst, biprodAddEquiv_symm_apply, biprodAddEquiv_apply_snd
biproductAddEquiv 📖	CompOp	—
chgUniv 📖	CompOp	1 math math: homEquiv_chgUniv
comp 📖	CompOp	43 math math: comp_sum, add_comp, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, zero_comp, preadditiveYoneda_homologySequenceδ_singleTriangle_apply, sum_comp, CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, mk₀_id_comp, comp_zero, comp_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, comp_add, preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, comp_assoc_of_second_deg_zero, singleFunctor_map_comp_hom, mk₀_comp_mk₀_assoc, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, smul_comp, comp_mk₀_id, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, hom_comp_singleFunctor_map_shift, bilinearComp_apply_apply, neg_comp, CategoryTheory.Abelian.extFunctor_map_app, CategoryTheory.ShortComplex.ShortExact.comp_extClass, biprodAddEquiv_apply_fst, comp_smul, mk₀_comp_mk₀, bilinearCompOfLinear_apply_apply, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, smul_eq_comp_mk₀, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, addEquivBiprod_symm_apply, addEquivBiprod_apply_snd, biprodAddEquiv_symm_apply, addEquivBiprod_apply_fst, comp_neg, biprodAddEquiv_apply_snd, CategoryTheory.ShortComplex.ShortExact.extClass_comp, comp_assoc_of_third_deg_zero, comp_hom
hom 📖	CompOp	18 math math: preadditiveYoneda_homologySequenceδ_singleTriangle_apply, smul_hom, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, mk₀_hom, preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.ShortComplex.ShortExact.extClass_hom, singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, mapExactFunctor_hom, hom_comp_singleFunctor_map_shift, homAddEquiv_apply, add_hom, zero_hom, CategoryTheory.InjectiveResolution.extMk_hom, ext_iff, neg_hom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, comp_hom
hom' 📖	CompOp	—
homAddEquiv 📖	CompOp	3 math math: homLinearEquiv_apply, homAddEquiv_apply, homLinearEquiv_symm_apply
homEquiv 📖	CompOp	1 math math: homEquiv_chgUniv
homEquiv₀ 📖	CompOp	2 math math: homEquiv₀_symm_apply, mk₀_homEquiv₀_apply
instAddCommGroup 📖	CompOp	102 math math: comp_sum, add_comp, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, homLinearEquiv_apply, zero_comp, precomp_mk₀_injective_of_epi, mk₀_addEquiv₀_apply, sum_comp, contravariant_sequence_exact₁', CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, smul_hom, eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, comp_zero, CategoryTheory.ProjectiveResolution.sub_extMk, mk₀_neg, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, mapExactFunctor_zero, postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, contravariant_sequence_exact₂', CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, comp_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.Abelian.extFunctorObj_map, covariant_sequence_exact₁', mk₀_smul, covariant_sequence_exact₃', CategoryTheory.InjectiveResolution.add_extMk, CategoryTheory.Functor.mapExtLinearMap_coe, CategoryTheory.InjectiveResolution.extMk_zero, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, precomp_extClass_surjective_of_projective_X₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, smul_comp, mk₀_add, CategoryTheory.ProjectiveResolution.add_extMk, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, bilinearComp_apply_apply, CategoryTheory.InjectiveResolution.extMk_eq_zero_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.Functor.mapExactFunctor_smul, neg_comp, CategoryTheory.Abelian.extFunctor_map_app, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.Functor.mapExtAddHom_apply, homAddEquiv_apply, mk₀_sum, CategoryTheory.ShortComplex.ShortExact.comp_extClass, biprodAddEquiv_apply_fst, add_hom, comp_smul, covariant_sequence_exact₂', zero_hom, mono_postcomp_mk₀_of_mono, mk₀_zero, CategoryTheory.ProjectiveResolution.extMk_zero, CategoryTheory.InjectiveResolution.sub_extMk, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, bilinearCompOfLinear_apply_apply, CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff, mono_precomp_mk₀_of_epi, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, mapExactFunctor_add, smul_eq_comp_mk₀, addEquiv₀_symm_apply, neg_hom, ModuleCat.finite_ext, eq_zero_of_projective, mk₀_eq_zero_iff, postcomp_mk₀_injective_of_mono, eq_zero_of_hasProjectiveDimensionLT, CategoryTheory.InjectiveResolution.neg_extMk, mk₀_linearEquiv₀_apply, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, addEquivBiprod_symm_apply, CategoryTheory.Functor.mapExtAddHom_coe, contravariant_sequence_exact₃', linearEquiv₀_symm_apply, addEquivBiprod_apply_snd, CategoryTheory.hasProjectiveDimensionLT_iff, homLinearEquiv_symm_apply, biprodAddEquiv_symm_apply, CategoryTheory.ProjectiveResolution.neg_extMk, addEquivBiprod_apply_fst, comp_neg, biprodAddEquiv_apply_snd, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.ShortComplex.ShortExact.extClass_comp, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.hasInjectiveDimensionLT_iff, eq_zero_of_injective, CategoryTheory.Functor.mapExtLinearMap_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg
mk₀ 📖	CompOp	52 math math: CategoryTheory.InjectiveResolution.extMk_comp_mk₀, precomp_mk₀_injective_of_epi, mk₀_addEquiv₀_apply, contravariant_sequence_exact₁', CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, mk₀_id_comp, mk₀_neg, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, mk₀_hom, contravariant_sequence_exact₂', CategoryTheory.Abelian.extFunctorObj_map, covariant_sequence_exact₁', mk₀_smul, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, covariant_sequence_exact₃', singleFunctor_map_comp_hom, mk₀_comp_mk₀_assoc, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, mk₀_add, comp_mk₀_id, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, hom_comp_singleFunctor_map_shift, CategoryTheory.Abelian.extFunctor_map_app, covariant_sequence_exact₃, mk₀_sum, CategoryTheory.ShortComplex.ShortExact.comp_extClass, biprodAddEquiv_apply_fst, covariant_sequence_exact₂', mono_postcomp_mk₀_of_mono, mk₀_zero, mk₀_comp_mk₀, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, mono_precomp_mk₀_of_epi, smul_eq_comp_mk₀, addEquiv₀_symm_apply, mk₀_eq_zero_iff, postcomp_mk₀_injective_of_mono, mk₀_linearEquiv₀_apply, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, mk₀_bijective, addEquivBiprod_symm_apply, contravariant_sequence_exact₃', linearEquiv₀_symm_apply, contravariant_sequence_exact₁, homEquiv₀_symm_apply, addEquivBiprod_apply_snd, biprodAddEquiv_symm_apply, addEquivBiprod_apply_fst, mk₀_homEquiv₀_apply, biprodAddEquiv_apply_snd, CategoryTheory.ShortComplex.ShortExact.extClass_comp
postcomp 📖	CompOp	7 math math: postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.Abelian.extFunctorObj_map, covariant_sequence_exact₁', covariant_sequence_exact₃', covariant_sequence_exact₂', mono_postcomp_mk₀_of_mono, postcomp_mk₀_injective_of_mono
precomp 📖	CompOp	6 math math: precomp_mk₀_injective_of_epi, contravariant_sequence_exact₁', contravariant_sequence_exact₂', precomp_extClass_surjective_of_projective_X₂, mono_precomp_mk₀_of_epi, contravariant_sequence_exact₃'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquivBiprod_apply_fst 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddEquiv CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquivBiprod comp mk₀ CategoryTheory.Limits.biprod.fst	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
addEquivBiprod_apply_snd 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddEquiv CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquivBiprod comp mk₀ CategoryTheory.Limits.biprod.snd	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
addEquivBiprod_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts Prod.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm addEquivBiprod comp mk₀ CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
addEquiv₀_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive instAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm addEquiv₀ mk₀	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
add_comp 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.add_comp
add_hom 📖	mathematical	CategoryTheory.HasExt	hom CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts zero_add comp_add mk₀_comp_mk₀_assoc comp.congr_simp CategoryTheory.Limits.biprod.lift_fst mk₀_id_comp CategoryTheory.Limits.biprod.lift_snd biprod_ext ext CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Limits.BinaryBicone.inl_snd mk₀_zero zero_comp add_zero comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom Equiv.apply_symm_apply CategoryTheory.ShiftedHom.comp_add DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.mk₀_id_comp CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveSingleFunctor CategoryTheory.ShiftedHom.mk₀_zero CategoryTheory.ShiftedHom.zero_comp CategoryTheory.Limits.BinaryBicone.inr_fst CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.Functor.map_comp
bilinearComp_apply_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddMonoidHom CategoryTheory.Abelian.Ext AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AddMonoidHom.instFunLike AddMonoidHom.instAddCommGroup bilinearComp comp	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
biprodAddEquiv_apply_fst 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddEquiv CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike biprodAddEquiv comp mk₀ CategoryTheory.Limits.biprod.inl	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
biprodAddEquiv_apply_snd 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddEquiv CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike biprodAddEquiv comp mk₀ CategoryTheory.Limits.biprod.inr	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
biprodAddEquiv_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts Prod.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm biprodAddEquiv comp mk₀ CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts
biprod_ext 📖	—	CategoryTheory.HasExt comp CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts mk₀ CategoryTheory.Limits.biprod.inl zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Limits.biprod.inr	—	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts zero_add ext_iff CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveSingleFunctor CategoryTheory.Limits.PreservesBinaryBiproducts.preserves CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts CategoryTheory.Limits.PreservesFiniteBiproducts.preserves CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive Finite.of_fintype comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀_comp
comp_add 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.comp_add DerivedCategory.instAdditiveShiftFunctorInt
comp_assoc 📖	mathematical	CategoryTheory.HasExt	comp	—	CategoryTheory.Localization.SmallShiftedHom.comp_assoc CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject
comp_assoc_of_second_deg_zero 📖	mathematical	CategoryTheory.HasExt	comp add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid zero_add	—	comp_assoc add_zero zero_add
comp_assoc_of_third_deg_zero 📖	mathematical	CategoryTheory.HasExt	comp add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	comp_assoc add_zero
comp_hom 📖	mathematical	CategoryTheory.HasExt	hom comp CategoryTheory.ShiftedHom.comp DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor	—	CategoryTheory.Localization.SmallShiftedHom.equiv_comp CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CategoryTheory.Abelian.hasZeroObject
comp_mk₀_id 📖	mathematical	CategoryTheory.HasExt	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	ext add_zero comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.comp_mk₀_id
comp_neg 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.comp_neg DerivedCategory.instAdditiveShiftFunctorInt
comp_sum 📖	mathematical	CategoryTheory.HasExt	comp Finset.sum CategoryTheory.Abelian.Ext AddCommGroup.toAddCommMonoid instAddCommGroup Finset.univ	—	map_sum AddMonoidHom.instAddMonoidHomClass
comp_zero 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.comp_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveShiftFunctorInt
ext 📖	—	CategoryTheory.HasExt hom	—	—	Equiv.injective
ext_iff 📖	mathematical	CategoryTheory.HasExt	hom	—	ext
homAddEquiv_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor EquivLike.toFunLike AddEquiv.instEquivLike homAddEquiv hom	—	—
homEquiv_chgUniv 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor EquivLike.toFunLike Equiv.instEquivLike homEquiv chgUniv	—	CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CategoryTheory.Abelian.hasZeroObject
homEquiv₀_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv₀ mk₀	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
mk₀_add 📖	mathematical	CategoryTheory.HasExt	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.Ext instAddCommGroup	—	ext mk₀_hom CategoryTheory.Functor.map_add DerivedCategory.instAdditiveSingleFunctor CategoryTheory.Preadditive.add_comp
mk₀_addEquiv₀_apply 📖	mathematical	CategoryTheory.HasExt	mk₀ DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive EquivLike.toFunLike AddEquiv.instEquivLike addEquiv₀	—	Equiv.left_inv
mk₀_bijective 📖	mathematical	CategoryTheory.HasExt	Function.Bijective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.Ext mk₀	—	DerivedCategory.instFullSingleFunctor DerivedCategory.instFaithfulSingleFunctor CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero Equiv.injective Equiv.apply_symm_apply CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀ CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CategoryTheory.Abelian.hasZeroObject Equiv.bijective
mk₀_comp_mk₀ 📖	mathematical	CategoryTheory.HasExt	comp mk₀ zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	ext zero_add comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_comp
mk₀_comp_mk₀_assoc 📖	mathematical	CategoryTheory.HasExt	comp mk₀ zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	zero_add mk₀_comp_mk₀ comp_assoc
mk₀_eq_zero_iff 📖	mathematical	CategoryTheory.HasExt	mk₀ CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	AddEquiv.map_eq_zero_iff
mk₀_hom 📖	mathematical	CategoryTheory.HasExt	hom mk₀ CategoryTheory.ShiftedHom.mk₀ DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Functor.map	—	CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀ CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CategoryTheory.Abelian.hasZeroObject
mk₀_homEquiv₀_apply 📖	mathematical	CategoryTheory.HasExt	mk₀ DFunLike.coe Equiv CategoryTheory.Abelian.Ext Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike homEquiv₀	—	Equiv.left_inv
mk₀_id_comp 📖	mathematical	CategoryTheory.HasExt	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	ext zero_add comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.mk₀_id_comp
mk₀_neg 📖	mathematical	CategoryTheory.HasExt	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.Ext instAddCommGroup	—	ext mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_neg DerivedCategory.instAdditiveSingleFunctor CategoryTheory.ShiftedHom.mk₀_neg
mk₀_sum 📖	mathematical	CategoryTheory.HasExt	mk₀ Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive Finset.univ CategoryTheory.Abelian.Ext instAddCommGroup	—	map_sum AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
mk₀_zero 📖	mathematical	CategoryTheory.HasExt	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ext mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveSingleFunctor CategoryTheory.ShiftedHom.mk₀_zero
neg_comp 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.neg_comp
neg_hom 📖	mathematical	CategoryTheory.HasExt	hom CategoryTheory.Abelian.Ext NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor	—	AddLeftCancelSemigroup.toIsLeftCancelAdd add_hom add_neg_cancel zero_hom
sum_comp 📖	mathematical	CategoryTheory.HasExt	comp Finset.sum CategoryTheory.Abelian.Ext AddCommGroup.toAddCommMonoid instAddCommGroup Finset.univ	—	map_sum AddMonoidHom.instAddMonoidHomClass
zero_comp 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.ShiftedHom.zero_comp
zero_hom 📖	mathematical	CategoryTheory.HasExt	hom CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms DerivedCategory.instPreadditive CategoryTheory.shiftFunctor	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveSingleFunctor CategoryTheory.Limits.isZero_zero zero_add comp_zero comp_hom CategoryTheory.ShiftedHom.comp_zero DerivedCategory.instAdditiveShiftFunctorInt

CategoryTheory.HasExt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
standard 📖	mathematical	—	CategoryTheory.HasExt	—	CategoryTheory.hasExt_of_hasDerivedCategory

---

← Back to Index