DimensionShifting

📁 Source: Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean

Statistics

Metric	Count
Definitions projectiveShortComplex	1
Theorems shortExact_projectiveShortComplex, instFreeCarrierX₂ModuleCatProjectiveShortComplex, postcomp_extClass_surjective_of_projective_X₂, precomp_extClass_surjective_of_projective_X₂	4
Total	5

ModuleCat

Definitions

Name	Category	Theorems
projectiveShortComplex 📖	CompOp	2 math math: shortExact_projectiveShortComplex, instFreeCarrierX₂ModuleCatProjectiveShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shortExact_projectiveShortComplex 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact ModuleCat CommRing.toRing moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive projectiveShortComplex	—	LinearMap.shortExact_shortComplexKer RingHomInvPair.ids Module.Basis.constr_apply LinearEquiv.map_zero Finsupp.mapRange_single equivShrink_symm_one Finsupp.sum_single_index zero_smul one_smul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFreeCarrierX₂ModuleCatProjectiveShortComplex 📖	mathematical	—	Module.Free ModuleCat.carrier CommRing.toRing CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.projectiveShortComplex CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Shrink Shrink.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.module Shrink.instModule Semiring.toModule	—	Module.Free.finsupp Module.Free.Module.free_shrink Module.Free.self
postcomp_extClass_surjective_of_projective_X₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	CategoryTheory.Abelian.Ext ModuleCat.abelian instHasExtModuleCatOfSmall CategoryTheory.ShortComplex.X₃ CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₁ DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Abelian.Ext.instAddCommGroup AddMonoidHom.instFunLike CategoryTheory.Abelian.Ext.postcomp CategoryTheory.ShortComplex.ShortExact.extClass	—	instHasExtModuleCatOfSmall CategoryTheory.Abelian.Ext.covariant_sequence_exact₁ CategoryTheory.Abelian.Ext.eq_zero_of_injective add_zero
precomp_extClass_surjective_of_projective_X₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	CategoryTheory.Abelian.Ext ModuleCat.abelian instHasExtModuleCatOfSmall CategoryTheory.ShortComplex.X₁ CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instAddCommSemigroup DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Abelian.Ext.instAddCommGroup AddMonoidHom.instFunLike CategoryTheory.Abelian.Ext.precomp CategoryTheory.ShortComplex.ShortExact.extClass add_comm	—	instHasExtModuleCatOfSmall CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃ CategoryTheory.Abelian.Ext.eq_zero_of_projective zero_add add_comm

---

← Back to Index