ShiftedHom

📁 Source: Mathlib/CategoryTheory/Shift/ShiftedHom.lean

Statistics

Metric	Count
Definitions ShiftedHom, comp, homEquiv, map, mk₀	5
Theorems add_comp, comp_add, comp_assoc, comp_map, comp_mk₀, comp_mk₀_id, comp_neg, comp_smul, comp_zero, homEquiv_apply, id_map, map_add, map_comp, map_mk₀, map_smul, map_zero, mk₀_add, mk₀_comp, mk₀_comp_mk₀, mk₀_comp_mk₀_assoc, mk₀_id_comp, mk₀_neg, mk₀_smul, mk₀_zero, neg_comp, smul_comp, zero_comp	27
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
ShiftedHom 📖	CompOp	45 math math: Abelian.Ext.homLinearEquiv_apply, ShiftedHom.neg_comp, ShiftedHom.mk₀_zero, ShiftedHom.opEquiv_symm_add, Abelian.Ext.smul_hom, ShiftedHom.comp_add, Localization.SmallShiftedHom.equiv_comp, ShiftedHom.zero_comp, Abelian.Ext.homEquiv_chgUniv, Localization.SmallShiftedHom.equiv_mk, ShiftedHom.comp_zero, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, ShiftedHom.comp_neg, Abelian.Ext.homAddEquiv_apply, Localization.SmallShiftedHom.equiv_chgUniv, ShiftedHom.comp_smul, Abelian.Ext.add_hom, LocalizerMorphism.equiv_smallShiftedHomMap, ShiftedHom.opEquiv'_symm_apply, ShiftedHom.mk₀_add, Abelian.Ext.zero_hom, Localization.SmallShiftedHom.equiv_shift, ShiftedHom.add_comp, ShiftedHom.opEquiv_symm_apply_comp, ShiftedHom.opEquiv'_symm_add, ShiftedHom.opEquiv'_zero_add_symm, ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, ShiftedHom.homEquiv_apply, ShiftedHom.map_smul, ShiftedHom.opEquiv'_symm_comp, Abelian.Ext.neg_hom, ShiftedHom.map_add, ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv'_apply, Localization.SmallShiftedHom.equiv_mk₀Inv, ShiftedHom.map_zero, Pretriangulated.preadditiveYoneda_shiftMap_apply, ShiftedHom.mk₀_neg, Localization.SmallShiftedHom.equiv_mk₀, Abelian.Ext.homLinearEquiv_symm_apply, Localization.SmallShiftedHom.equiv_apply, ShiftedHom.smul_comp, ShiftedHom.mk₀_smul, ShiftedHom.opEquiv'_add_symm, ShiftedHom.opEquiv_symm_comp

CategoryTheory.ShiftedHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	28 math math: neg_comp, map_comp, comp_add, CategoryTheory.Localization.SmallShiftedHom.equiv_comp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, zero_comp, CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk, comp_mk₀, mk₀_comp, CategoryTheory.ProjectiveResolution.extMk_hom, mk₀_id_comp, comp_zero, mk₀_comp_mk₀, mk₀_comp_mk₀_assoc, comp_mk₀_id, comp_neg, comp_smul, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, add_comp, comp_assoc, opEquiv_symm_apply_comp, opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, CategoryTheory.InjectiveResolution.extMk_hom, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, smul_comp, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, opEquiv_symm_comp, CategoryTheory.Abelian.Ext.comp_hom
homEquiv 📖	CompOp	1 math math: homEquiv_apply
map 📖	CompOp	16 math math: map_comp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Localization.SmallShiftedHom.equiv_mk, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, comp_map, CategoryTheory.InjectiveResolution.extMk_hom, map_smul, map_mk₀, map_add, id_map, map_zero, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom
mk₀ 📖	CompOp	21 math math: mk₀_zero, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk, comp_mk₀, mk₀_comp, CategoryTheory.ProjectiveResolution.extMk_hom, mk₀_id_comp, mk₀_comp_mk₀, mk₀_comp_mk₀_assoc, comp_mk₀_id, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, mk₀_add, homEquiv_apply, CategoryTheory.InjectiveResolution.extMk_hom, map_mk₀, CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv, mk₀_neg, CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, mk₀_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	comp.eq_1 CategoryTheory.Preadditive.add_comp
comp_add 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj	—	comp.eq_1 CategoryTheory.Functor.map_add CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add
comp_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp	—	CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.shiftFunctorAdd'_assoc_inv_app
comp_map 📖	mathematical	—	map CategoryTheory.Functor.comp CategoryTheory.Functor.CommShift.comp CategoryTheory.Functor.obj	—	CategoryTheory.Functor.commShiftIso_comp_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
comp_mk₀ 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor CategoryTheory.Functor.map	—	CategoryTheory.Iso.refl_trans CategoryTheory.shiftFunctorAdd'_zero_add_inv_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id
comp_mk₀_id 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	comp_mk₀ CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
comp_neg 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj	—	comp.eq_1 CategoryTheory.Functor.map_neg CategoryTheory.Preadditive.neg_comp CategoryTheory.Preadditive.comp_neg
comp_smul 📖	mathematical	CategoryTheory.Functor.Linear Ring.toSemiring CategoryTheory.shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	comp.eq_1 CategoryTheory.Functor.map_smul CategoryTheory.Linear.smul_comp CategoryTheory.Linear.comp_smul
comp_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.obj	—	comp.eq_1 CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
homEquiv_apply 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShiftedHom EquivLike.toFunLike Equiv.instEquivLike homEquiv mk₀	—	—
id_map 📖	mathematical	—	map CategoryTheory.Functor.id CategoryTheory.Functor.CommShift.id	—	CategoryTheory.Functor.commShiftIso_id_hom_app CategoryTheory.Category.comp_id
map_add 📖	mathematical	—	map CategoryTheory.ShiftedHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Functor.map_add CategoryTheory.Preadditive.add_comp
map_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	map comp CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.commShiftIso_add' CategoryTheory.Functor.CommShift.isoAdd'_hom_app CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id
map_mk₀ 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	map mk₀ CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Iso.refl_trans CategoryTheory.Functor.map_comp CategoryTheory.Functor.CommShift.commShiftIso_zero CategoryTheory.Functor.CommShift.isoZero_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
map_smul 📖	mathematical	—	map CategoryTheory.ShiftedHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj CategoryTheory.shiftFunctor DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	CategoryTheory.Functor.map_smul CategoryTheory.Linear.smul_comp
map_zero 📖	mathematical	—	map CategoryTheory.ShiftedHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.zero_comp
mk₀_add 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShiftedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Preadditive.add_comp
mk₀_comp 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Iso.refl_trans CategoryTheory.shiftFunctorAdd'_add_zero_inv_app CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc
mk₀_comp_mk₀ 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	mk₀_comp mk₀.eq_1 CategoryTheory.Category.assoc zero_add
mk₀_comp_mk₀_assoc 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	add_zero comp_assoc mk₀_comp_mk₀
mk₀_id_comp 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	comp mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	mk₀_comp CategoryTheory.Category.id_comp
mk₀_neg 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShiftedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Preadditive.neg_comp
mk₀_smul 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SMulZeroClass.toSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule CategoryTheory.ShiftedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Linear.smul_comp
mk₀_zero 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShiftedHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	CategoryTheory.Limits.zero_comp
neg_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	comp.eq_1 CategoryTheory.Preadditive.neg_comp
smul_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj CategoryTheory.shiftFunctor DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	comp.eq_1 CategoryTheory.Linear.smul_comp
zero_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	comp CategoryTheory.ShiftedHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.shiftFunctor	—	comp.eq_1 CategoryTheory.Limits.zero_comp

---

← Back to Index