Ext

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

Statistics

Metric	Count
Definitions Ext, isoExt, linearYonedaObj	3
Theorems linearYonedaObj_X, linearYonedaObj_d, isZero_Ext_succ_of_projective	3
Total	6

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
Ext 📖	CompOp	120 math math: Ext.comp_sum, CategoryTheory.HasProjectiveDimensionLT.subsingleton, Ext.add_comp, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, Ext.homLinearEquiv_apply, Ext.zero_comp, CategoryTheory.HasProjectiveDimensionLT.subsingleton', Ext.subsingleton_of_projective, Ext.precomp_mk₀_injective_of_epi, Ext.mk₀_addEquiv₀_apply, Ext.sum_comp, Ext.contravariant_sequence_exact₁', CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, extFunctorObj_obj_coe, Ext.smul_hom, Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, Ext.comp_zero, CategoryTheory.ProjectiveResolution.sub_extMk, Ext.mk₀_neg, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Ext.mapExactFunctor_zero, postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, Ext.contravariant_sequence_exact₂', CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, Ext.comp_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, extFunctorObj_map, CategoryTheory.projective_iff_subsingleton_ext_one, Ext.covariant_sequence_exact₁', Ext.mk₀_smul, Ext.covariant_sequence_exact₃', CategoryTheory.InjectiveResolution.add_extMk, CategoryTheory.Functor.mapExtLinearMap_coe, CategoryTheory.InjectiveResolution.extMk_zero, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, Ext.homEquiv_chgUniv, precomp_extClass_surjective_of_projective_X₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Ext.smul_comp, CategoryTheory.hasExt_iff_small_ext, Ext.mk₀_add, CategoryTheory.ProjectiveResolution.add_extMk, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, Ext.bilinearComp_apply_apply, CategoryTheory.InjectiveResolution.extMk_eq_zero_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.Functor.mapExactFunctor_smul, Ext.neg_comp, extFunctor_map_app, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.Functor.mapExtAddHom_apply, Ext.homAddEquiv_apply, Ext.mk₀_sum, CategoryTheory.ShortComplex.ShortExact.comp_extClass, Ext.biprodAddEquiv_apply_fst, Ext.add_hom, Ext.comp_smul, Ext.covariant_sequence_exact₂', CategoryTheory.HasInjectiveDimensionLT.subsingleton', Ext.zero_hom, Ext.mono_postcomp_mk₀_of_mono, Ext.mk₀_zero, CategoryTheory.ProjectiveResolution.extMk_zero, CategoryTheory.InjectiveResolution.sub_extMk, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, Ext.bilinearCompOfLinear_apply_apply, CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff, Ext.mono_precomp_mk₀_of_epi, Ext.subsingleton_of_injective, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, Ext.mapExactFunctor_add, Ext.smul_eq_comp_mk₀, Ext.addEquiv₀_symm_apply, Ext.neg_hom, ModuleCat.finite_ext, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, Ext.eq_zero_of_projective, Ext.mk₀_eq_zero_iff, Ext.postcomp_mk₀_injective_of_mono, CategoryTheory.injective_iff_subsingleton_ext_one, Ext.eq_zero_of_hasProjectiveDimensionLT, CategoryTheory.InjectiveResolution.neg_extMk, Ext.mk₀_linearEquiv₀_apply, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, Ext.mk₀_bijective, Ext.addEquivBiprod_symm_apply, CategoryTheory.Functor.mapExtAddHom_coe, Ext.contravariant_sequence_exact₃', Ext.linearEquiv₀_symm_apply, Ext.homEquiv₀_symm_apply, Ext.addEquivBiprod_apply_snd, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, CategoryTheory.hasProjectiveDimensionLT_iff, Ext.homLinearEquiv_symm_apply, Ext.biprodAddEquiv_symm_apply, CategoryTheory.ProjectiveResolution.neg_extMk, Ext.addEquivBiprod_apply_fst, Ext.comp_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, Ext.mk₀_homEquiv₀_apply, Ext.biprodAddEquiv_apply_snd, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.HasInjectiveDimensionLT.subsingleton, CategoryTheory.ShortComplex.ShortExact.extClass_comp, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.hasInjectiveDimensionLT_iff, Ext.eq_zero_of_injective, CategoryTheory.Functor.mapExtLinearMap_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
isoExt 📖	CompOp	—

ChainComplex

Definitions

Name	Category	Theorems
linearYonedaObj 📖	CompOp	5 math math: inhomogeneousCochains.d_eq, linearYonedaObj_d, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, linearYonedaObj_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearYonedaObj_X 📖	mathematical	—	HomologicalComplex.X ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd linearYonedaObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.linearYoneda CategoryTheory.Abelian.toPreadditive Opposite.op ComplexShape.down	—	AddRightCancelSemigroup.toIsRightCancelAdd
linearYonedaObj_d 📖	mathematical	—	HomologicalComplex.d ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd linearYonedaObj ModuleCat.ofHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Abelian.toPreadditive ComplexShape.down CategoryTheory.Preadditive.homGroup CategoryTheory.Linear.homModule Ring.toSemiring CategoryTheory.Linear.leftComp	—	AddRightCancelSemigroup.toIsRightCancelAdd

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_Ext_succ_of_projective 📖	mathematical	—	CategoryTheory.Limits.IsZero ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Ext Opposite.op	—	CategoryTheory.Limits.IsZero.of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.exactAt_iff_isZero_homology HomologicalComplex.exactAt_iff CategoryTheory.ShortComplex.exact_of_isZero_X₂ CategoryTheory.Limits.IsZero.iff_id_eq_zero ModuleCat.hom_ext LinearMap.ext CategoryTheory.Limits.IsZero.eq_of_src HomologicalComplex.isZero_single_obj_X

---

← Back to Index