ExtClass

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

Statistics

Metric	Count
Definitions extClass	1
Theorems comp_extClass, comp_extClass_assoc, extClass_comp, extClass_comp_assoc, extClass_hom, instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, ext_mk₀_f_comp_ext_mk₀_g	7
Total	8

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_mk₀_f_comp_ext_mk₀_g 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext.comp X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₂ X₃ CategoryTheory.Abelian.Ext.mk₀ f g zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	zero_add CategoryTheory.Abelian.Ext.mk₀_comp_mk₀ zero CategoryTheory.Abelian.Ext.mk₀_zero

CategoryTheory.ShortComplex.ShortExact

Definitions

Name	Category	Theorems
extClass 📖	CompOp	15 math math: CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, extClass_hom, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', precomp_extClass_surjective_of_projective_X₂, comp_extClass_assoc, comp_extClass, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁, extClass_comp_assoc, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃, extClass_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_extClass 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Abelian.Ext.comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.ShortComplex.g extClass zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.Ext.ext zero_add CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Abelian.Ext.mk₀_hom extClass_hom CategoryTheory.ShiftedHom.mk₀_comp CategoryTheory.Abelian.Ext.zero_hom CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt singleTriangle_distinguished
comp_extClass_assoc 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Abelian.Ext.comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ extClass zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	zero_add CategoryTheory.Abelian.Ext.comp_assoc comp_extClass CategoryTheory.Abelian.Ext.zero_comp
extClass_comp 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Abelian.Ext.comp CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ extClass CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.ShortComplex.f add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.Ext.ext add_zero CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp extClass_hom CategoryTheory.Abelian.Ext.mk₀_hom CategoryTheory.ShiftedHom.comp_mk₀ CategoryTheory.Abelian.Ext.zero_hom CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt singleTriangle_distinguished
extClass_comp_assoc 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Abelian.Ext.comp CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ extClass CategoryTheory.ShortComplex.X₂ CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.ShortComplex.f zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	zero_add CategoryTheory.Abelian.Ext.comp_assoc add_zero extClass_comp CategoryTheory.Abelian.Ext.zero_comp
extClass_hom 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Abelian.Ext.hom CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ extClass singleδ	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Localization.SmallHom.equiv_comp CategoryTheory.Localization.SmallHom.equiv_mkInv CochainComplex.mappingCone.quasiIso_descShortComplex CategoryTheory.Category.assoc DerivedCategory.singleFunctorsPostcompQIso_hom_hom DerivedCategory.singleFunctorsPostcompQIso_inv_hom CategoryTheory.NatTrans.id_app CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁ 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.ShortComplex.X₃ CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup HomologicalComplex.instHasZeroMorphisms CategoryTheory.ShortComplex.map CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.instPreadditive CochainComplex.instAdditiveIntFunctorSingleFunctors CategoryTheory.ShortComplex.X₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.preservesZeroMorphisms_of_additive CochainComplex.instAdditiveIntFunctorSingleFunctors

---

← Back to Index