Documentation Verification Report

Map

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

Statistics

Metric	Count
Definitions `mapExactFunctor`, `mapExtAddHom`, `mapExtLinearMap`	3
Theorems `mapExactFunctor_add`, `mapExactFunctor_hom`, `mapExactFunctor_zero`, `mapExactFunctor_smul`, `mapExtAddHom_apply`, `mapExtAddHom_coe`, `mapExtLinearMap_apply`, `mapExtLinearMap_coe`, `mapExtLinearMap_toAddMonoidHom`, `instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt`	10
Total	13

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt` 📖	mathematical	`HasExt`	`Localization.HasSmallLocalizedShiftedHom` `HomologicalComplex` `Preadditive.preadditiveHasZeroMorphisms` `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` `categoryWithHomology_of_abelian` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `Functor.obj` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `Functor.comp` `CochainComplex.singleFunctor` `Abelian.hasZeroObject`	—	—

CategoryTheory.Abelian.Ext

Definitions

Name	Category	Theorems
`mapExactFunctor` 📖	CompOp	8 math math: `mapExactFunctor_zero`, `CategoryTheory.Functor.mapExtLinearMap_coe`, `mapExactFunctor_hom`, `CategoryTheory.Functor.mapExactFunctor_smul`, `CategoryTheory.Functor.mapExtAddHom_apply`, `mapExactFunctor_add`, `CategoryTheory.Functor.mapExtAddHom_coe`, `CategoryTheory.Functor.mapExtLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapExactFunctor_add` 📖	mathematical	`CategoryTheory.HasExt`	`mapExactFunctor` `CategoryTheory.Abelian.Ext` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `CategoryTheory.Functor.obj`	—	`ext` `mapExactFunctor_hom` `add_hom` `CategoryTheory.ShiftedHom.map_add` `CategoryTheory.Functor.IsTriangulated.instAdditive` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Preadditive.comp_add`
`mapExactFunctor_hom` 📖	mathematical	`CategoryTheory.HasExt`	`hom` `CategoryTheory.Functor.obj` `mapExactFunctor` `CategoryTheory.CategoryStruct.comp` `DerivedCategory` `CategoryTheory.Category.toCategoryStruct` `DerivedCategory.instCategory` `CategoryTheory.Functor.comp` `DerivedCategory.singleFunctor` `CategoryTheory.Functor.mapDerivedCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `DerivedCategory.instHasShiftInt` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.mapDerivedCategorySingleFunctor` `CategoryTheory.ShiftedHom.map` `CategoryTheory.Functor.instCommShiftDerivedCategoryMapDerivedCategoryInt` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp` `zero_add` `add_zero` `CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap` `CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt` `CategoryTheory.NatTrans.CommShift.of_iso_symm` `CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors` `CategoryTheory.ShiftedHom.comp_mk₀` `CategoryTheory.ShiftedHom.mk₀_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_id`
`mapExactFunctor_zero` 📖	mathematical	`CategoryTheory.HasExt`	`mapExactFunctor` `CategoryTheory.Abelian.Ext` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `CategoryTheory.Functor.obj`	—	`ext` `mapExactFunctor_hom` `zero_hom` `CategoryTheory.ShiftedHom.map_zero` `CategoryTheory.Functor.IsTriangulated.instAdditive` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapExtAddHom` 📖	CompOp	3 math math: `mapExtLinearMap_toAddMonoidHom`, `mapExtAddHom_apply`, `mapExtAddHom_coe`
`mapExtLinearMap` 📖	CompOp	3 math math: `mapExtLinearMap_toAddMonoidHom`, `mapExtLinearMap_coe`, `mapExtLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapExactFunctor_smul` 📖	mathematical	`CategoryTheory.HasExt`	`CategoryTheory.Abelian.Ext.mapExactFunctor` `CategoryTheory.Abelian.Ext` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Abelian.Ext.instAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instModule` `obj`	—	`CategoryTheory.Abelian.Ext.ext` `CategoryTheory.Abelian.Ext.mapExactFunctor_hom` `CategoryTheory.Abelian.Ext.smul_hom` `CategoryTheory.ShiftedHom.map_smul` `instLinearDerivedCategoryMapDerivedCategory` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Linear.comp_smul`
`mapExtAddHom_apply` 📖	mathematical	`CategoryTheory.HasExt`	`DFunLike.coe` `AddMonoidHom` `CategoryTheory.Abelian.Ext` `obj` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Abelian.Ext.instAddCommGroup` `AddMonoidHom.instFunLike` `mapExtAddHom` `CategoryTheory.Abelian.Ext.mapExactFunctor`	—	—
`mapExtAddHom_coe` 📖	mathematical	`CategoryTheory.HasExt`	`DFunLike.coe` `AddMonoidHom` `CategoryTheory.Abelian.Ext` `obj` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Abelian.Ext.instAddCommGroup` `AddMonoidHom.instFunLike` `mapExtAddHom` `CategoryTheory.Abelian.Ext.mapExactFunctor`	—	—
`mapExtLinearMap_apply` 📖	mathematical	`CategoryTheory.HasExt`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CategoryTheory.Abelian.Ext` `obj` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `CategoryTheory.Abelian.Ext.instModule` `LinearMap.instFunLike` `mapExtLinearMap` `CategoryTheory.Abelian.Ext.mapExactFunctor`	—	—
`mapExtLinearMap_coe` 📖	mathematical	`CategoryTheory.HasExt`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CategoryTheory.Abelian.Ext` `obj` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `CategoryTheory.Abelian.Ext.instModule` `LinearMap.instFunLike` `mapExtLinearMap` `CategoryTheory.Abelian.Ext.mapExactFunctor`	—	—
`mapExtLinearMap_toAddMonoidHom` 📖	mathematical	`CategoryTheory.HasExt`	`AddMonoidHomClass.toAddMonoidHom` `CategoryTheory.Abelian.Ext` `obj` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `CategoryTheory.Abelian.Ext.instModule` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LinearMap.instFunLike` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mapExtLinearMap` `mapExtAddHom`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index