EnoughInjectives

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

Statistics

Metric	Count
Definitions	0
Theorems eq_zero_of_injective, subsingleton_of_injective, hasExt_of_enoughInjectives, isSplitMono_from_singleFunctor_obj_of_injective, to_singleFunctor_obj_eq_zero_of_injective	5
Total	5

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasExt_of_enoughInjectives 📖	mathematical	—	HasExt	—	hasExt_of_hasDerivedCategory hasExt_iff_small_ext small_congr instSmallHomOfLocallySmall Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.cokernel.condition ShortComplex.exact_of_g_is_cokernel CategoryWithHomology.hasHomology categoryWithHomology_of_abelian Injective.ι_mono Limits.coequalizer.π_epi Abelian.Ext.covariant_sequence_exact₁ Abelian.Ext.eq_zero_of_injective Injective.injective_under add_zero small_of_surjective

CategoryTheory.Abelian.Ext

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_injective 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CochainComplex.isStrictlyGE_of_ge CochainComplex.instIsStrictlyGEObjIntSingleFunctor Equiv.injective zero_hom CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.zero_comp DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective
subsingleton_of_injective 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext	—	eq_zero_of_injective

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSplitMono_from_singleFunctor_obj_of_injective 📖	mathematical	—	CategoryTheory.IsSplitMono CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj singleFunctor CategoryTheory.Abelian.hasZeroObject	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian prev CategoryTheory.Limits.IsZero.eq_of_src isZero_of_isStrictlyGE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono Int.instZeroLEOneClass HomologicalComplex.instHasHomologyObjSingle CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc HomologicalComplex.pOpcyclesIso_inv_hom_id CategoryTheory.Category.comp_id HomologicalComplex.homologyι_naturality HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc HomologicalComplex.pOpcycles_singleObjOpcyclesSelfIso_inv_assoc CategoryTheory.Iso.inv_hom_id_assoc HomologicalComplex.p_opcyclesMap CategoryTheory.mono_comp CategoryTheory.Iso.isIso_inv instIsIsoHomologyMapOfQuasiIsoAt HomologicalComplex.instMonoHomologyι contravariant_lt_of_covariant_le HomologicalComplex.to_single_hom_ext HomologicalComplex.comp_f HomologicalComplex.mkHomToSingle_f HomologicalComplex.id_f CategoryTheory.Injective.comp_factorThru_assoc CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id

DerivedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_singleFunctor_obj_eq_zero_of_injective 📖	mathematical	—	Quiver.Hom DerivedCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.HasZeroMorphisms.zero instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject left_fac_of_isStrictlyGE CochainComplex.instIsStrictlyGEObjIntSingleFunctor CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective QuasiIso.quasiIsoAt CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.hom_inv_id CategoryTheory.Functor.map_comp CategoryTheory.IsSplitMono.id CategoryTheory.Functor.map_id HomologicalComplex.to_single_hom_ext CategoryTheory.Limits.IsZero.eq_of_src CochainComplex.isZero_of_isStrictlyGE CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveCochainComplexIntQ

---

← Back to Index