Documentation Verification Report

CochainComplexPlus

📁 Source: Mathlib/Algebra/Homology/CochainComplexPlus.lean

Statistics

Metric	Count
Definitions `mapCochainComplexPlus`, `mapCochainComplexPlusCompι`, `fullyFaithfulι`, `quasiIso`, `ι`, `plus`	6
Theorems `mapCochainComplexPlusCompι_hom_app_f`, `mapCochainComplexPlusCompι_inv_app_f`, `mapCochainComplexPlus_map_hom_f`, `mapCochainComplexPlus_obj_obj_X`, `mapCochainComplexPlus_obj_obj_d`, `instHasFiniteColimits`, `instHasFiniteLimits`, `instHasTwoOutOfThreePropertyQuasiIso`, `instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape`, `instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape`, `instIsStableUnderRetractsQuasiIso`, `instIsStableUnderShiftIntPlus`, `mono_iff`, `instIsClosedUnderIsomorphismsIntPlus`, `plus_iff`	15
Total	21

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapCochainComplexPlus` 📖	CompOp	5 math math: `mapCochainComplexPlus_obj_obj_X`, `mapCochainComplexPlusCompι_inv_app_f`, `mapCochainComplexPlusCompι_hom_app_f`, `mapCochainComplexPlus_obj_obj_d`, `mapCochainComplexPlus_map_hom_f`
`mapCochainComplexPlusCompι` 📖	CompOp	2 math math: `mapCochainComplexPlusCompι_inv_app_f`, `mapCochainComplexPlusCompι_hom_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapCochainComplexPlusCompι_hom_app_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `obj` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.plus` `comp` `mapCochainComplexPlus` `CochainComplex.Plus.ι` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `AddRightCancelSemigroup.toIsRightCancelAdd` `category` `mapHomologicalComplex` `mapCochainComplexPlusCompι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mapCochainComplexPlusCompι_inv_app_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `obj` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.plus` `comp` `mapCochainComplexPlus` `CochainComplex.Plus.ι` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `AddRightCancelSemigroup.toIsRightCancelAdd` `category` `mapHomologicalComplex` `mapCochainComplexPlusCompι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mapCochainComplexPlus_map_hom_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `obj` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.plus` `comp` `CochainComplex.Plus.ι` `mapHomologicalComplex` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `map` `mapCochainComplexPlus` `HomologicalComplex.X`	—	—
`mapCochainComplexPlus_obj_obj_X` 📖	mathematical	—	`HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.plus` `obj` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapCochainComplexPlus`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mapCochainComplexPlus_obj_obj_d` 📖	mathematical	—	`HomologicalComplex.d` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.plus` `obj` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapCochainComplexPlus` `map` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

CochainComplex

Definitions

Name	Category	Theorems
`plus` 📖	CompOp	15 math math: `Plus.mono_iff`, `CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X`, `Plus.instHasFiniteLimits`, `Plus.instHasTwoOutOfThreePropertyQuasiIso`, `CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f`, `instIsClosedUnderIsomorphismsIntPlus`, `Plus.instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape`, `CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f`, `Plus.instHasFiniteColimits`, `Plus.instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape`, `plus_iff`, `CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d`, `Plus.instIsStableUnderShiftIntPlus`, `CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f`, `Plus.instIsStableUnderRetractsQuasiIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderIsomorphismsIntPlus` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `plus`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `isStrictlyGE_of_iso`
`plus_iff` 📖	mathematical	—	`plus` `IsStrictlyGE`	—	—

CochainComplex.Plus

Definitions

Name	Category	Theorems
`fullyFaithfulι` 📖	CompOp	—
`quasiIso` 📖	CompOp	2 math math: `instHasTwoOutOfThreePropertyQuasiIso`, `instIsStableUnderRetractsQuasiIso`
`ι` 📖	CompOp	3 math math: `CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f`, `CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f`, `CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteColimits` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.plus`	—	`CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits` `instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `HomologicalComplex.instHasColimitsOfShape` `AddRightCancelSemigroup.toIsRightCancelAdd`
`instHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.plus`	—	`CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits` `instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `HomologicalComplex.instHasLimitsOfShape` `AddRightCancelSemigroup.toIsRightCancelAdd`
`instHasTwoOutOfThreePropertyQuasiIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.plus` `quasiIso`	—	`CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage` `HomologicalComplex.instHasTwoOutOfThreePropertyQuasiIso`
`instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.plus`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.isStrictlyGE_of_ge` `Finset.min'_le` `Finset.union_singleton` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj` `CochainComplex.isStrictlyGE_iff` `CategoryTheory.Limits.IsZero.iff_id_eq_zero` `CategoryTheory.Limits.IsColimit.hom_ext` `HomologicalComplex.instPreservesColimitEval` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `HomologicalComplex.instHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `HomologicalComplex.instPreservesColimitsOfShapeEvalOfHasColimitsOfShape` `CategoryTheory.Limits.IsZero.eq_of_src` `CochainComplex.isZero_of_isStrictlyGE`
`instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.plus`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.isStrictlyGE_of_ge` `Finset.min'_le` `Finset.union_singleton` `CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj` `CochainComplex.isStrictlyGE_iff` `CategoryTheory.Limits.IsZero.iff_id_eq_zero` `CategoryTheory.Limits.IsLimit.hom_ext` `HomologicalComplex.instPreservesLimitEval` `CategoryTheory.Limits.instHasLimitCompOfPreservesLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `HomologicalComplex.instHasLimitsOfShape` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `HomologicalComplex.instPreservesLimitsOfShapeEvalOfHasLimitsOfShape` `CategoryTheory.Limits.IsZero.eq_of_tgt` `CochainComplex.isZero_of_isStrictlyGE`
`instIsStableUnderRetractsQuasiIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.plus` `quasiIso`	—	`CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage` `HomologicalComplex.instIsStableUnderRetractsQuasiIso`
`instIsStableUnderShiftIntPlus` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsStableUnderShift` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.plus` `Int.instAddMonoid` `CochainComplex.instHasShiftInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.isStrictlyGE_shift`
`mono_iff` 📖	mathematical	—	`CategoryTheory.Mono` `CochainComplex.Plus` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.plus` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `CategoryTheory.ObjectProperty.full_ι` `CategoryTheory.ObjectProperty.faithful_ι`

---

← Back to Index