Documentation Verification Report

ExtendHomotopy

📁 Source: Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean

Statistics

Metric	Count
Definitions `extendHomotopyFunctor`, `extendHomotopyFunctorFactors`, `extend`, `hom`, `homAux`, `extendEquiv`, `ofExtend`	7
Theorems `instFaithfulHomotopyCategoryExtendHomotopyFunctor`, `instFullHomotopyCategoryExtendHomotopyFunctor`, `homAux_eq`, `hom_eq`, `hom_eq_zero₁`, `hom_eq_zero₂`, `extend_hom_eq`, `extend_ofExtend`, `ofExtend_extend`, `ofExtend_hom`	10
Total	17

ComplexShape.Embedding

Definitions

Name	Category	Theorems
`extendHomotopyFunctor` 📖	CompOp	2 math math: `instFaithfulHomotopyCategoryExtendHomotopyFunctor`, `instFullHomotopyCategoryExtendHomotopyFunctor`
`extendHomotopyFunctorFactors` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulHomotopyCategoryExtendHomotopyFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `HomotopyCategory` `instCategoryHomotopyCategory` `extendHomotopyFunctor`	—	`HomotopyCategory.quotient_obj_surjective` `CategoryTheory.Functor.map_surjective` `HomotopyCategory.instFullHomologicalComplexQuotient` `HomotopyCategory.eq_of_homotopy`
`instFullHomotopyCategoryExtendHomotopyFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `HomotopyCategory` `instCategoryHomotopyCategory` `extendHomotopyFunctor`	—	`HomotopyCategory.quotient_obj_surjective` `CategoryTheory.Functor.map_surjective` `HomotopyCategory.instFullHomologicalComplexQuotient` `instFullHomologicalComplexExtendFunctor`

Homotopy

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	3 math math: `extend_hom_eq`, `extend_ofExtend`, `ofExtend_extend`
`extendEquiv` 📖	CompOp	—
`ofExtend` 📖	CompOp	3 math math: `extend_ofExtend`, `ofExtend_extend`, `ofExtend_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_hom_eq` 📖	mathematical	`ComplexShape.Embedding.f`	`hom` `HomologicalComplex.extend` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.extendMap` `extend` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Iso.hom` `HomologicalComplex.extendXIso` `CategoryTheory.Iso.inv`	—	`extend.hom_eq`
`extend_ofExtend` 📖	mathematical	—	`extend` `ofExtend`	—	`ext` `extend_hom_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Limits.IsZero.eq_of_tgt` `HomologicalComplex.isZero_extend_X` `CategoryTheory.Limits.IsZero.eq_of_src`
`ofExtend_extend` 📖	mathematical	—	`ofExtend` `extend`	—	`ext` `extend_hom_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`ofExtend_hom` 📖	mathematical	—	`hom` `ofExtend` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.extend` `ComplexShape.Embedding.f` `CategoryTheory.Iso.inv` `HomologicalComplex.extendXIso` `HomologicalComplex.extendMap` `CategoryTheory.Iso.hom`	—	—

Homotopy.extend

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	3 math math: `hom_eq_zero₁`, `hom_eq_zero₂`, `hom_eq`
`homAux` 📖	CompOp	1 math math: `homAux_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homAux_eq` 📖	mathematical	—	`homAux` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.extend.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.X` `CategoryTheory.Iso.hom` `HomologicalComplex.extend.XIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`hom_eq` 📖	mathematical	`ComplexShape.Embedding.f`	`hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.extend` `CategoryTheory.Iso.hom` `HomologicalComplex.extendXIso` `CategoryTheory.Iso.inv`	—	`homAux_eq` `ComplexShape.Embedding.r_eq_some`
`hom_eq_zero₁` 📖	mathematical	—	`hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.extend` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Limits.IsZero.eq_of_src` `HomologicalComplex.isZero_extend_X`
`hom_eq_zero₂` 📖	mathematical	—	`hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.extend` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Limits.IsZero.eq_of_tgt` `HomologicalComplex.isZero_extend_X`

---

← Back to Index