Documentation Verification Report

RestrictionHomology

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

Statistics

Metric	Count
Definitions `sc'Iso`, `restrictionCyclesIso`, `restrictionHomologyIso`, `restrictionOpcyclesIso`	4
Theorems `homologyπ_restrictionHomologyIso_hom`, `homologyπ_restrictionHomologyIso_hom_assoc`, `homologyπ_restrictionHomologyIso_inv`, `homologyπ_restrictionHomologyIso_inv_assoc`, `pOpcycles_restrictionOpcyclesIso_hom`, `pOpcycles_restrictionOpcyclesIso_hom_assoc`, `pOpcycles_restrictionOpcyclesIso_inv`, `pOpcycles_restrictionOpcyclesIso_inv_assoc`, `hasHomology`, `sc'Iso_hom_τ₁`, `sc'Iso_hom_τ₂`, `sc'Iso_hom_τ₃`, `sc'Iso_inv_τ₁`, `sc'Iso_inv_τ₂`, `sc'Iso_inv_τ₃`, `restrictionCyclesIso_hom_iCycles`, `restrictionCyclesIso_hom_iCycles_assoc`, `restrictionCyclesIso_inv_iCycles`, `restrictionCyclesIso_inv_iCycles_assoc`, `restrictionHomologyIso_hom_homologyι`, `restrictionHomologyIso_hom_homologyι_assoc`, `restrictionHomologyIso_inv_homologyι`, `restrictionHomologyIso_inv_homologyι_assoc`	23
Total	27

HomologicalComplex

Definitions

Name	Category	Theorems
`restrictionCyclesIso` 📖	CompOp	8 math math: `homologyπ_restrictionHomologyIso_inv_assoc`, `restrictionCyclesIso_hom_iCycles`, `homologyπ_restrictionHomologyIso_inv`, `homologyπ_restrictionHomologyIso_hom`, `restrictionCyclesIso_inv_iCycles_assoc`, `restrictionCyclesIso_hom_iCycles_assoc`, `restrictionCyclesIso_inv_iCycles`, `homologyπ_restrictionHomologyIso_hom_assoc`
`restrictionHomologyIso` 📖	CompOp	8 math math: `homologyπ_restrictionHomologyIso_inv_assoc`, `homologyπ_restrictionHomologyIso_inv`, `restrictionHomologyIso_inv_homologyι_assoc`, `homologyπ_restrictionHomologyIso_hom`, `restrictionHomologyIso_hom_homologyι`, `restrictionHomologyIso_hom_homologyι_assoc`, `restrictionHomologyIso_inv_homologyι`, `homologyπ_restrictionHomologyIso_hom_assoc`
`restrictionOpcyclesIso` 📖	CompOp	8 math math: `pOpcycles_restrictionOpcyclesIso_hom_assoc`, `pOpcycles_restrictionOpcyclesIso_inv`, `restrictionHomologyIso_inv_homologyι_assoc`, `restrictionHomologyIso_hom_homologyι`, `restrictionHomologyIso_hom_homologyι_assoc`, `restrictionHomologyIso_inv_homologyι`, `pOpcycles_restrictionOpcyclesIso_inv_assoc`, `pOpcycles_restrictionOpcyclesIso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homologyπ_restrictionHomologyIso_hom` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `homology` `homologyπ` `CategoryTheory.Iso.hom` `restrictionHomologyIso` `restrictionCyclesIso`	—	`CategoryTheory.ShortComplex.homologyMap_comp` `CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology` `CategoryTheory.cancel_mono` `CategoryTheory.ShortComplex.instMonoHomologyι` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology` `CategoryTheory.ShortComplex.π_homologyMap_ι` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `restrictionCyclesIso_hom_iCycles_assoc` `CategoryTheory.ShortComplex.homology_π_ι`
`homologyπ_restrictionHomologyIso_hom_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `homology` `homologyπ` `CategoryTheory.Iso.hom` `restrictionHomologyIso` `restrictionCyclesIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyπ_restrictionHomologyIso_hom`
`homologyπ_restrictionHomologyIso_inv` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `homology` `restriction` `homologyπ` `CategoryTheory.Iso.inv` `restrictionHomologyIso` `restrictionCyclesIso`	—	`CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `homologyπ_restrictionHomologyIso_hom` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`homologyπ_restrictionHomologyIso_inv_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `homology` `homologyπ` `restriction` `CategoryTheory.Iso.inv` `restrictionHomologyIso` `restrictionCyclesIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyπ_restrictionHomologyIso_inv`
`pOpcycles_restrictionOpcyclesIso_hom` 📖	mathematical	`ComplexShape.prev` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `restriction` `opcycles` `pOpcycles` `CategoryTheory.Iso.hom` `restrictionOpcyclesIso` `restrictionXIso`	—	`p_descOpcycles`
`pOpcycles_restrictionOpcyclesIso_hom_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `restriction` `opcycles` `pOpcycles` `CategoryTheory.Iso.hom` `restrictionOpcyclesIso` `restrictionXIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pOpcycles_restrictionOpcyclesIso_hom`
`pOpcycles_restrictionOpcyclesIso_inv` 📖	mathematical	`ComplexShape.prev` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `opcycles` `restriction` `pOpcycles` `CategoryTheory.Iso.inv` `restrictionOpcyclesIso` `restrictionXIso`	—	`p_descOpcycles`
`pOpcycles_restrictionOpcyclesIso_inv_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `opcycles` `pOpcycles` `restriction` `CategoryTheory.Iso.inv` `restrictionOpcyclesIso` `restrictionXIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pOpcycles_restrictionOpcyclesIso_inv`
`restrictionCyclesIso_hom_iCycles` 📖	mathematical	`ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `X` `CategoryTheory.Iso.hom` `restrictionCyclesIso` `iCycles` `restrictionXIso`	—	`liftCycles_i`
`restrictionCyclesIso_hom_iCycles_assoc` 📖	mathematical	`ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `CategoryTheory.Iso.hom` `restrictionCyclesIso` `X` `iCycles` `restrictionXIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictionCyclesIso_hom_iCycles`
`restrictionCyclesIso_inv_iCycles` 📖	mathematical	`ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `X` `CategoryTheory.Iso.inv` `restrictionCyclesIso` `iCycles` `restrictionXIso`	—	`liftCycles_i`
`restrictionCyclesIso_inv_iCycles_assoc` 📖	mathematical	`ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `restriction` `CategoryTheory.Iso.inv` `restrictionCyclesIso` `X` `iCycles` `restrictionXIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictionCyclesIso_inv_iCycles`
`restrictionHomologyIso_hom_homologyι` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `homology` `restriction` `opcycles` `CategoryTheory.Iso.hom` `restrictionHomologyIso` `homologyι` `restrictionOpcyclesIso`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Iso.inv_hom_id_assoc` `restrictionHomologyIso_inv_homologyι_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`restrictionHomologyIso_hom_homologyι_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `homology` `restriction` `CategoryTheory.Iso.hom` `restrictionHomologyIso` `opcycles` `homologyι` `restrictionOpcyclesIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictionHomologyIso_hom_homologyι`
`restrictionHomologyIso_inv_homologyι` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `homology` `restriction` `opcycles` `CategoryTheory.Iso.inv` `restrictionHomologyIso` `homologyι` `restrictionOpcyclesIso`	—	`CategoryTheory.ShortComplex.homologyMap_comp` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology` `CategoryTheory.cancel_epi` `CategoryTheory.ShortComplex.instEpiHomologyπ` `CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology` `CategoryTheory.ShortComplex.π_homologyMap_ι` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.ShortComplex.homology_π_ι_assoc` `pOpcycles_restrictionOpcyclesIso_inv`
`restrictionHomologyIso_inv_homologyι_assoc` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `homology` `restriction` `CategoryTheory.Iso.inv` `restrictionHomologyIso` `opcycles` `homologyι` `restrictionOpcyclesIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `restrictionHomologyIso_inv_homologyι`

HomologicalComplex.restriction

Definitions

Name	Category	Theorems
`sc'Iso` 📖	CompOp	6 math math: `sc'Iso_inv_τ₃`, `sc'Iso_inv_τ₁`, `sc'Iso_hom_τ₂`, `sc'Iso_inv_τ₂`, `sc'Iso_hom_τ₃`, `sc'Iso_hom_τ₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasHomology` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.f`	`HomologicalComplex.HasHomology` `HomologicalComplex.restriction`	—	`CategoryTheory.ShortComplex.hasHomology_of_iso`
`sc'Iso_hom_τ₁` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₁` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.hom` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—
`sc'Iso_hom_τ₂` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₂` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.hom` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—
`sc'Iso_hom_τ₃` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₃` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.hom` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—
`sc'Iso_inv_τ₁` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₁` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.inv` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—
`sc'Iso_inv_τ₂` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₂` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.inv` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—
`sc'Iso_inv_τ₃` 📖	mathematical	`ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.ShortComplex.Hom.τ₃` `HomologicalComplex.sc'` `HomologicalComplex.restriction` `CategoryTheory.Iso.inv` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `sc'Iso` `HomologicalComplex.X` `HomologicalComplex.restrictionXIso`	—	—

---

← Back to Index