Documentation Verification Report

HomEquiv

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

Statistics

Metric	Count
Definitions `HasLift`, `homEquiv`, `homRestrict`, `f`, `liftExtend`, `f`, `liftExtendfArrowIso`	7
Theorems `epi_liftExtend_f_iff`, `homEquiv_apply_coe`, `homEquiv_symm_apply`, `comm`, `comm_assoc`, `f_eq`, `homRestrict_comp_extendMap`, `homRestrict_comp_extendMap_assoc`, `homRestrict_f`, `homRestrict_hasLift`, `homRestrict_liftExtend`, `homRestrict_precomp`, `homRestrict_precomp_assoc`, `isIso_liftExtend_f_iff`, `comm`, `comm_assoc`, `f_eq`, `liftExtend_f`, `liftExtend_homRestrict`, `mono_liftExtend_f_iff`	20
Total	27

ComplexShape.Embedding

Definitions

Name	Category	Theorems
`HasLift` 📖	MathDef	4 math math: `homEquiv_symm_apply`, `homEquiv_apply_coe`, `homRestrict_hasLift`, `HomologicalComplex.restrictionToTruncGE'_hasLift`
`homEquiv` 📖	CompOp	2 math math: `homEquiv_symm_apply`, `homEquiv_apply_coe`
`homRestrict` 📖	CompOp	9 math math: `homRestrict_precomp`, `homRestrict_comp_extendMap_assoc`, `homEquiv_apply_coe`, `homRestrict_liftExtend`, `homRestrict_hasLift`, `homRestrict_precomp_assoc`, `homRestrict_f`, `liftExtend_homRestrict`, `homRestrict_comp_extendMap`
`liftExtend` 📖	CompOp	7 math math: `isIso_liftExtend_f_iff`, `epi_liftExtend_f_iff`, `mono_liftExtend_f_iff`, `homEquiv_symm_apply`, `homRestrict_liftExtend`, `liftExtend_f`, `liftExtend_homRestrict`
`liftExtendfArrowIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_liftExtend_f_iff` 📖	mathematical	`HasLift` `f`	`CategoryTheory.Epi` `HomologicalComplex.X` `HomologicalComplex.extend` `HomologicalComplex.Hom.f` `liftExtend` `HomologicalComplex.restriction`	—	`CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.epimorphisms`
`homEquiv_apply_coe` 📖	mathematical	—	`Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.restriction` `HasLift` `DFunLike.coe` `Equiv` `HomologicalComplex.extend` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `homRestrict`	—	—
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.restriction` `HasLift` `HomologicalComplex.extend` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `liftExtend`	—	—
`homRestrict_comp_extendMap` 📖	mathematical	—	`homRestrict` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.extend` `HomologicalComplex.extendMap` `HomologicalComplex.restriction`	—	`HomologicalComplex.hom_ext` `homRestrict_f` `HomologicalComplex.extendMap_f` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`homRestrict_comp_extendMap_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.restriction` `homRestrict` `HomologicalComplex.extend` `HomologicalComplex.extendMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homRestrict_comp_extendMap`
`homRestrict_f` 📖	mathematical	`f`	`HomologicalComplex.Hom.f` `HomologicalComplex.restriction` `homRestrict` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Iso.hom` `HomologicalComplex.restrictionXIso` `HomologicalComplex.extend` `HomologicalComplex.extendXIso`	—	`homRestrict.f_eq`
`homRestrict_hasLift` 📖	mathematical	—	`HasLift` `homRestrict`	—	`CategoryTheory.Limits.IsZero.eq_of_src` `HomologicalComplex.isZero_extend_X` `BoundaryGE.notMem` `homRestrict.f_eq` `HomologicalComplex.restrictionXIso.eq_1` `CategoryTheory.eqToIso_refl` `CategoryTheory.Iso.refl_hom` `CategoryTheory.Category.id_comp` `HomologicalComplex.Hom.comm_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`homRestrict_liftExtend` 📖	mathematical	`HasLift`	`homRestrict` `liftExtend`	—	`HomologicalComplex.hom_ext` `homRestrict_f` `liftExtend_f` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_assoc`
`homRestrict_precomp` 📖	mathematical	—	`homRestrict` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.extend` `HomologicalComplex.restriction` `HomologicalComplex.restrictionMap`	—	`HomologicalComplex.hom_ext` `homRestrict_f` `CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp`
`homRestrict_precomp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.restriction` `homRestrict` `HomologicalComplex.extend` `HomologicalComplex.restrictionMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homRestrict_precomp`
`isIso_liftExtend_f_iff` 📖	mathematical	`HasLift` `f`	`CategoryTheory.IsIso` `HomologicalComplex.X` `HomologicalComplex.extend` `HomologicalComplex.Hom.f` `liftExtend` `HomologicalComplex.restriction`	—	`CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms`
`liftExtend_f` 📖	mathematical	`HasLift` `f`	`HomologicalComplex.Hom.f` `HomologicalComplex.extend` `liftExtend` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.restriction` `CategoryTheory.Iso.inv` `HomologicalComplex.restrictionXIso` `HomologicalComplex.extendXIso`	—	`liftExtend.f_eq`
`liftExtend_homRestrict` 📖	mathematical	—	`liftExtend` `homRestrict` `homRestrict_hasLift`	—	`HomologicalComplex.hom_ext` `homRestrict_hasLift` `liftExtend_f` `homRestrict_f` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Limits.IsZero.eq_of_tgt` `HomologicalComplex.isZero_extend_X`
`mono_liftExtend_f_iff` 📖	mathematical	`HasLift` `f`	`CategoryTheory.Mono` `HomologicalComplex.X` `HomologicalComplex.extend` `HomologicalComplex.Hom.f` `liftExtend` `HomologicalComplex.restriction`	—	`CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.monomorphisms`

ComplexShape.Embedding.homRestrict

Definitions

Name	Category	Theorems
`f` 📖	CompOp	3 math math: `comm_assoc`, `comm`, `f_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.restriction` `f` `HomologicalComplex.d` `ComplexShape.Embedding.f`	—	`CategoryTheory.Category.assoc` `HomologicalComplex.Hom.comm_assoc` `HomologicalComplex.extend_d_eq` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.restriction` `f` `HomologicalComplex.d` `ComplexShape.Embedding.f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`f_eq` 📖	mathematical	`ComplexShape.Embedding.f`	`f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.restriction` `CategoryTheory.Iso.hom` `HomologicalComplex.restrictionXIso` `HomologicalComplex.extend` `HomologicalComplex.Hom.f` `HomologicalComplex.extendXIso`	—	`CategoryTheory.Category.id_comp`

ComplexShape.Embedding.liftExtend

Definitions

Name	Category	Theorems
`f` 📖	CompOp	3 math math: `comm_assoc`, `comm`, `f_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	`ComplexShape.Embedding.HasLift`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.extend` `f` `HomologicalComplex.d`	—	`f_eq` `HomologicalComplex.extend_d_eq` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `HomologicalComplex.Hom.comm_assoc` `CategoryTheory.Limits.IsZero.eq_of_tgt` `HomologicalComplex.isZero_extend_X` `CategoryTheory.Limits.IsZero.eq_of_src` `CategoryTheory.Limits.comp_zero` `Mathlib.Tactic.Reassoc.eq_whisker'` `ComplexShape.Embedding.boundaryGE` `CategoryTheory.Limits.zero_comp` `HomologicalComplex.shape`
`comm_assoc` 📖	mathematical	`ComplexShape.Embedding.HasLift`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.extend` `f` `HomologicalComplex.d`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`f_eq` 📖	mathematical	`ComplexShape.Embedding.f`	`f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `HomologicalComplex.restriction` `HomologicalComplex.extend` `CategoryTheory.Iso.inv` `HomologicalComplex.restrictionXIso` `HomologicalComplex.Hom.f` `HomologicalComplex.extendXIso`	—	`ComplexShape.Embedding.injective_f`

---

← Back to Index