Documentation Verification Report

Double

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

Statistics

Metric	Count
Definitions `double`, `doubleXIso₀`, `doubleXIso₁`, `evalCompCoyonedaCorepresentable`, `evalCompCoyonedaCorepresentableByDoubleId`, `evalCompCoyonedaCorepresentableBySingle`, `evalCompCoyonedaCorepresentative`, `mkHomFromDouble`	8
Theorems `double_d`, `double_d_eq_zero₀`, `double_d_eq_zero₁`, `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply`, `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply`, `evalCompCoyonedaCorepresentableBySingle_homEquiv_apply`, `evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply`, `from_double_hom_ext`, `from_double_hom_ext_iff`, `instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp`, `isZero_double_X`, `mkHomFromDouble_f₀`, `mkHomFromDouble_f₀_assoc`, `mkHomFromDouble_f₁`, `mkHomFromDouble_f₁_assoc`, `to_double_hom_ext`, `to_double_hom_ext_iff`	17
Total	25

HomologicalComplex

Definitions

Name	Category	Theorems
`double` 📖	CompOp	12 math math: `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply`, `double_d_eq_zero₀`, `isZero_double_X`, `mkHomFromDouble_f₀`, `mkHomFromDouble_f₁`, `to_double_hom_ext_iff`, `double_d`, `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply`, `mkHomFromDouble_f₀_assoc`, `double_d_eq_zero₁`, `mkHomFromDouble_f₁_assoc`, `from_double_hom_ext_iff`
`doubleXIso₀` 📖	CompOp	4 math math: `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply`, `mkHomFromDouble_f₀`, `double_d`, `mkHomFromDouble_f₀_assoc`
`doubleXIso₁` 📖	CompOp	3 math math: `mkHomFromDouble_f₁`, `double_d`, `mkHomFromDouble_f₁_assoc`
`evalCompCoyonedaCorepresentable` 📖	CompOp	—
`evalCompCoyonedaCorepresentableByDoubleId` 📖	CompOp	2 math math: `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply`, `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply`
`evalCompCoyonedaCorepresentableBySingle` 📖	CompOp	2 math math: `evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply`, `evalCompCoyonedaCorepresentableBySingle_homEquiv_apply`
`evalCompCoyonedaCorepresentative` 📖	CompOp	—
`mkHomFromDouble` 📖	CompOp	5 math math: `mkHomFromDouble_f₀`, `mkHomFromDouble_f₁`, `evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply`, `mkHomFromDouble_f₀_assoc`, `mkHomFromDouble_f₁_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`double_d` 📖	mathematical	`ComplexShape.Rel`	`d` `double` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Iso.hom` `doubleXIso₀` `CategoryTheory.Iso.inv` `doubleXIso₁`	—	—
`double_d_eq_zero₀` 📖	mathematical	`ComplexShape.Rel`	`d` `double` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`double_d_eq_zero₁` 📖	mathematical	`ComplexShape.Rel`	`d` `double` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply` 📖	mathematical	`ComplexShape.Rel`	`DFunLike.coe` `Equiv` `Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `double` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `eval` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Functor.CorepresentableBy.homEquiv` `evalCompCoyonedaCorepresentableByDoubleId` `CategoryTheory.CategoryStruct.comp` `Opposite.unop` `X` `CategoryTheory.Iso.inv` `doubleXIso₀` `Hom.f`	—	—
`evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply` 📖	mathematical	`ComplexShape.Rel`	`DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `HomologicalComplex` `instCategory` `CategoryTheory.types` `CategoryTheory.Functor.comp` `eval` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `double` `CategoryTheory.CategoryStruct.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.CorepresentableBy.homEquiv` `evalCompCoyonedaCorepresentableByDoubleId` `mkHomFromDouble` `CategoryTheory.CategoryStruct.comp` `X` `d`	—	—
`evalCompCoyonedaCorepresentableBySingle_homEquiv_apply` 📖	mathematical	`ComplexShape.Rel`	`DFunLike.coe` `Equiv` `Quiver.Hom` `HomologicalComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `single` `CategoryTheory.types` `CategoryTheory.Functor.comp` `eval` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Functor.CorepresentableBy.homEquiv` `evalCompCoyonedaCorepresentableBySingle` `CategoryTheory.CategoryStruct.comp` `Opposite.unop` `X` `CategoryTheory.Iso.inv` `singleObjXSelf` `Hom.f`	—	—
`evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply` 📖	mathematical	`ComplexShape.Rel`	`DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `HomologicalComplex` `instCategory` `CategoryTheory.types` `CategoryTheory.Functor.comp` `eval` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `single` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Functor.CorepresentableBy.homEquiv` `evalCompCoyonedaCorepresentableBySingle` `mkHomFromSingle`	—	—
`from_double_hom_ext` 📖	—	`ComplexShape.Rel` `Hom.f` `double`	—	—	`hom_ext` `CategoryTheory.Limits.IsZero.eq_of_src` `isZero_double_X`
`from_double_hom_ext_iff` 📖	mathematical	`ComplexShape.Rel`	`Hom.f` `double`	—	`from_double_hom_ext`
`instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp` 📖	mathematical	—	`CategoryTheory.Functor.IsCorepresentable` `HomologicalComplex` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.types` `eval` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op`	—	—
`isZero_double_X` 📖	mathematical	`ComplexShape.Rel`	`CategoryTheory.Limits.IsZero` `X` `double`	—	`CategoryTheory.Limits.isZero_zero`
`mkHomFromDouble_f₀` 📖	mathematical	`ComplexShape.Rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`Hom.f` `double` `mkHomFromDouble` `CategoryTheory.Iso.hom` `doubleXIso₀`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`mkHomFromDouble_f₀_assoc` 📖	mathematical	`ComplexShape.Rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`double` `Hom.f` `mkHomFromDouble` `CategoryTheory.Iso.hom` `doubleXIso₀`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mkHomFromDouble_f₀`
`mkHomFromDouble_f₁` 📖	mathematical	`ComplexShape.Rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`Hom.f` `double` `mkHomFromDouble` `CategoryTheory.Iso.hom` `doubleXIso₁`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`mkHomFromDouble_f₁_assoc` 📖	mathematical	`ComplexShape.Rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`double` `Hom.f` `mkHomFromDouble` `CategoryTheory.Iso.hom` `doubleXIso₁`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mkHomFromDouble_f₁`
`to_double_hom_ext` 📖	—	`ComplexShape.Rel` `Hom.f` `double`	—	—	`hom_ext` `CategoryTheory.Limits.IsZero.eq_of_tgt` `isZero_double_X`
`to_double_hom_ext_iff` 📖	mathematical	`ComplexShape.Rel`	`Hom.f` `double`	—	`to_double_hom_ext`

---

← Back to Index