Restriction

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

Statistics

Metric	Count
Definitions restrictionFunctor, restriction, restrictionMap, restrictionXIso	4
Theorems instAdditiveHomologicalComplexRestrictionFunctor, instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor, restrictionFunctor_map, restrictionFunctor_obj, restrictionMap_comp, restrictionMap_comp_assoc, restrictionMap_f, restrictionMap_f', restrictionMap_f'_assoc, restrictionMap_id, restriction_X, restriction_d, restriction_d_eq, restriction_d_eq_assoc	14
Total	18

ComplexShape.Embedding

Definitions

Name	Category	Theorems
restrictionFunctor 📖	CompOp	6 math math: restrictionFunctor_map, instAdditiveHomologicalComplexRestrictionFunctor, restrictionToTruncGE'NatTrans_app, restrictionFunctor_obj, truncLE'ToRestrictionNatTrans_app, instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveHomologicalComplexRestrictionFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.instPreadditive restrictionFunctor	—	—
instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms restrictionFunctor	—	—
restrictionFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory restrictionFunctor HomologicalComplex.restrictionMap	—	—
restrictionFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory restrictionFunctor HomologicalComplex.restriction	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
restriction 📖	CompOp	71 math math: pOpcycles_restrictionOpcyclesIso_hom_assoc, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, ComplexShape.Embedding.isIso_liftExtend_f_iff, homologyπ_restrictionHomologyIso_inv_assoc, restriction.hasHomology, restrictionMap_comp, restriction.sc'Iso_inv_τ₃, restrictionCyclesIso_hom_iCycles, restriction_d_eq, homologyπ_restrictionHomologyIso_inv, instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, pOpcycles_restrictionOpcyclesIso_inv, restriction.sc'Iso_inv_τ₁, restriction_X, instMonoFTruncLE'ToRestriction, restrictionMap_f'_assoc, restrictionToTruncGE'.comm_assoc, restriction_d, restrictionToTruncGE'.comm, restrictionHomologyIso_inv_homologyι_assoc, truncLE'.quasiIsoAt_truncLE'ToRestriction, restrictionMap_id, restriction.sc'Iso_hom_τ₂, ComplexShape.Embedding.homRestrict_precomp, ComplexShape.Embedding.epi_liftExtend_f_iff, CochainComplex.ConnectData.restrictionLEIso_inv_f, homologyπ_restrictionHomologyIso_hom, ComplexShape.Embedding.homRestrict_comp_extendMap_assoc, restrictionHomologyIso_hom_homologyι, isIso_truncLE'ToRestriction, ComplexShape.Embedding.mono_liftExtend_f_iff, CochainComplex.ConnectData.restrictionLEIso_hom_f, restrictionHomologyIso_hom_homologyι_assoc, ComplexShape.Embedding.homEquiv_symm_apply, ComplexShape.Embedding.homRestrict.comm_assoc, ComplexShape.Embedding.homEquiv_apply_coe, truncLE'ToRestriction_naturality_assoc, restrictionMap_comp_assoc, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, ComplexShape.Embedding.liftExtend_f, ComplexShape.Embedding.homRestrict.comm, restrictionCyclesIso_inv_iCycles_assoc, ComplexShape.Embedding.liftExtend.f_eq, truncGE'.quasiIsoAt_restrictionToTruncGE', CochainComplex.ConnectData.restrictionGEIso_inv_f, restrictionHomologyIso_inv_homologyι, restrictionToTruncGE'_naturality_assoc, instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, restrictionMap_f', ComplexShape.Embedding.homRestrict_precomp_assoc, restrictionToTruncGE'_naturality, restrictionMap_f, restrictionCyclesIso_hom_iCycles_assoc, restriction.sc'Iso_inv_τ₂, ComplexShape.Embedding.restrictionFunctor_obj, ComplexShape.Embedding.homRestrict_f, isIso_restrictionToTruncGE', ComplexShape.Embedding.homRestrict.f_eq, restrictionToTruncGE'.f_eq_iso_hom_iso_inv, truncLE'ToRestriction_naturality, restrictionToTruncGE'_f_eq_iso_hom_iso_inv, pOpcycles_restrictionOpcyclesIso_inv_assoc, restriction_d_eq_assoc, restriction.sc'Iso_hom_τ₃, ComplexShape.Embedding.homRestrict_comp_extendMap, restriction.sc'Iso_hom_τ₁, restrictionCyclesIso_inv_iCycles, homologyπ_restrictionHomologyIso_hom_assoc, pOpcycles_restrictionOpcyclesIso_hom, instEpiFRestrictionToTruncGE', CochainComplex.ConnectData.restrictionGEIso_hom_f
restrictionMap 📖	CompOp	13 math math: restrictionMap_comp, ComplexShape.Embedding.restrictionFunctor_map, restrictionMap_f'_assoc, restrictionMap_id, ComplexShape.Embedding.homRestrict_precomp, truncLE'ToRestriction_naturality_assoc, restrictionMap_comp_assoc, restrictionToTruncGE'_naturality_assoc, restrictionMap_f', ComplexShape.Embedding.homRestrict_precomp_assoc, restrictionToTruncGE'_naturality, restrictionMap_f, truncLE'ToRestriction_naturality
restrictionXIso 📖	CompOp	30 math math: pOpcycles_restrictionOpcyclesIso_hom_assoc, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, restriction.sc'Iso_inv_τ₃, restrictionCyclesIso_hom_iCycles, restriction_d_eq, pOpcycles_restrictionOpcyclesIso_inv, restriction.sc'Iso_inv_τ₁, restrictionMap_f'_assoc, restriction.sc'Iso_hom_τ₂, CochainComplex.ConnectData.restrictionLEIso_inv_f, CochainComplex.ConnectData.restrictionLEIso_hom_f, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, ComplexShape.Embedding.liftExtend_f, restrictionCyclesIso_inv_iCycles_assoc, ComplexShape.Embedding.liftExtend.f_eq, CochainComplex.ConnectData.restrictionGEIso_inv_f, restrictionMap_f', restrictionCyclesIso_hom_iCycles_assoc, restriction.sc'Iso_inv_τ₂, ComplexShape.Embedding.homRestrict_f, ComplexShape.Embedding.homRestrict.f_eq, restrictionToTruncGE'.f_eq_iso_hom_iso_inv, restrictionToTruncGE'_f_eq_iso_hom_iso_inv, pOpcycles_restrictionOpcyclesIso_inv_assoc, restriction_d_eq_assoc, restriction.sc'Iso_hom_τ₃, restriction.sc'Iso_hom_τ₁, restrictionCyclesIso_inv_iCycles, pOpcycles_restrictionOpcyclesIso_hom, CochainComplex.ConnectData.restrictionGEIso_hom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictionMap_comp 📖	mathematical	—	restrictionMap CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory restriction	—	—
restrictionMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory restriction restrictionMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictionMap_comp
restrictionMap_f 📖	mathematical	—	Hom.f restriction restrictionMap ComplexShape.Embedding.f	—	—
restrictionMap_f' 📖	mathematical	ComplexShape.Embedding.f	Hom.f restriction restrictionMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom restrictionXIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
restrictionMap_f'_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X restriction Hom.f restrictionMap CategoryTheory.Iso.hom restrictionXIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictionMap_f'
restrictionMap_id 📖	mathematical	—	restrictionMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory restriction	—	—
restriction_X 📖	mathematical	—	X restriction ComplexShape.Embedding.f	—	—
restriction_d 📖	mathematical	—	d restriction ComplexShape.Embedding.f	—	—
restriction_d_eq 📖	mathematical	ComplexShape.Embedding.f	d restriction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom restrictionXIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
restriction_d_eq_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X restriction d CategoryTheory.Iso.hom restrictionXIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restriction_d_eq

---

← Back to Index