EnoughProjectives

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

Statistics

Metric	Count
Definitions EnoughProjectives	1
Theorems eq_zero_of_projective, subsingleton_of_projective, hasExt_of_enoughProjectives, isSplitEpi_to_singleFunctor_obj_of_projective, from_singleFunctor_obj_eq_zero_of_projective	5
Total	6

CategoryTheory

Definitions

Name	Category	Theorems
EnoughProjectives 📖	CompData	8 math math: Profinite.instEnoughProjectives, ModuleCat.enoughProjectives, CompHaus.instEnoughProjectives, Injective.instEnoughProjectivesOppositeOfEnoughInjectives, Rep.instEnoughProjectives, Equivalence.enoughProjectives_iff, Projective.Type.enoughProjectives, Injective.enoughProjectives_of_enoughInjectives_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasExt_of_enoughProjectives 📖	mathematical	—	HasExt	—	hasExt_of_hasDerivedCategory hasExt_iff_small_ext small_congr instSmallHomOfLocallySmall Limits.HasKernels.has_limit Abelian.has_kernels Limits.kernel.condition ShortComplex.exact_of_f_is_kernel CategoryWithHomology.hasHomology categoryWithHomology_of_abelian Limits.equalizer.ι_mono Projective.π_epi add_comm Abelian.Ext.contravariant_sequence_exact₃ Abelian.Ext.eq_zero_of_projective Projective.projective_over zero_add small_of_surjective

CategoryTheory.Abelian.Ext

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_projective 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	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.from_singleFunctor_obj_eq_zero_of_projective AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CochainComplex.instIsStrictlyLEObjIntSingleFunctor
subsingleton_of_projective 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext	—	eq_zero_of_projective

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSplitEpi_to_singleFunctor_obj_of_projective 📖	mathematical	—	CategoryTheory.IsSplitEpi 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 next CategoryTheory.Limits.IsZero.eq_of_tgt isZero_of_isStrictlyLE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instZeroLEOneClass HomologicalComplex.instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc HomologicalComplex.iCyclesIso_hom_inv_id_assoc HomologicalComplex.homologyπ_naturality_assoc HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles CategoryTheory.Iso.hom_inv_id_assoc HomologicalComplex.cyclesMap_i CategoryTheory.epi_comp CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ instIsIsoHomologyMapOfQuasiIsoAt HomologicalComplex.from_single_hom_ext HomologicalComplex.comp_f HomologicalComplex.mkHomFromSingle_f HomologicalComplex.id_f CategoryTheory.Projective.factorThru_comp_assoc CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id

DerivedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
from_singleFunctor_obj_eq_zero_of_projective 📖	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 right_fac_of_isStrictlyLE CochainComplex.instIsStrictlyLEObjIntSingleFunctor CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective QuasiIso.quasiIsoAt CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.IsIso.inv_hom_id CategoryTheory.Functor.map_comp CategoryTheory.IsSplitEpi.id CategoryTheory.Functor.map_id HomologicalComplex.from_single_hom_ext CategoryTheory.Limits.IsZero.eq_of_tgt CochainComplex.isZero_of_isStrictlyLE CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveCochainComplexIntQ

---

← Back to Index