StupidTrunc

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

Statistics

Metric	Count
Definitions stupidTruncFunctor, stupidTrunc, stupidTruncMap, stupidTruncXIso	4
Theorems stupidTruncFunctor_map, stupidTruncFunctor_obj, instIsStrictlySupportedStupidTrunc, instIsStrictlySupportedStupidTrunc_1, isZero_stupidTrunc_X, isZero_stupidTrunc_iff, stupidTruncMap_comp, stupidTruncMap_comp_assoc, stupidTruncMap_id, stupidTruncMap_stupidTruncXIso_hom, stupidTruncMap_stupidTruncXIso_hom_assoc	11
Total	15

ComplexShape.Embedding

Definitions

Name	Category	Theorems
stupidTruncFunctor 📖	CompOp	2 math math: stupidTruncFunctor_map, stupidTruncFunctor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stupidTruncFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory stupidTruncFunctor HomologicalComplex.stupidTruncMap	—	—
stupidTruncFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory stupidTruncFunctor HomologicalComplex.stupidTrunc	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
stupidTrunc 📖	CompOp	10 math math: isZero_stupidTrunc_X, stupidTruncMap_comp, stupidTruncMap_id, isZero_stupidTrunc_iff, instIsStrictlySupportedStupidTrunc_1, stupidTruncMap_stupidTruncXIso_hom_assoc, instIsStrictlySupportedStupidTrunc, stupidTruncMap_comp_assoc, stupidTruncMap_stupidTruncXIso_hom, ComplexShape.Embedding.stupidTruncFunctor_obj
stupidTruncMap 📖	CompOp	6 math math: stupidTruncMap_comp, stupidTruncMap_id, ComplexShape.Embedding.stupidTruncFunctor_map, stupidTruncMap_stupidTruncXIso_hom_assoc, stupidTruncMap_comp_assoc, stupidTruncMap_stupidTruncXIso_hom
stupidTruncXIso 📖	CompOp	2 math math: stupidTruncMap_stupidTruncXIso_hom_assoc, stupidTruncMap_stupidTruncXIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStrictlySupportedStupidTrunc 📖	mathematical	—	IsStrictlySupported stupidTrunc	—	instIsStrictlySupportedExtend
instIsStrictlySupportedStupidTrunc_1 📖	mathematical	—	IsStrictlySupported stupidTrunc	—	CategoryTheory.Limits.IsZero.of_iso isZero_X_of_isStrictlySupported isZero_stupidTrunc_X
isZero_stupidTrunc_X 📖	mathematical	—	CategoryTheory.Limits.IsZero X stupidTrunc	—	isZero_extend_X
isZero_stupidTrunc_iff 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex instCategory stupidTrunc IsStrictlySupportedOutside	—	CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Functor.map_isZero instPreservesZeroMorphismsEval isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside instIsStrictlySupportedStupidTrunc IsStrictlySupportedOutside.isZero
stupidTruncMap_comp 📖	mathematical	—	stupidTruncMap CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory stupidTrunc	—	extendMap_comp
stupidTruncMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory stupidTrunc stupidTruncMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stupidTruncMap_comp
stupidTruncMap_id 📖	mathematical	—	stupidTruncMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory stupidTrunc	—	extendMap_id
stupidTruncMap_stupidTruncXIso_hom 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X stupidTrunc Hom.f stupidTruncMap CategoryTheory.Iso.hom stupidTruncXIso	—	extendMap_f CategoryTheory.Iso.trans_refl CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
stupidTruncMap_stupidTruncXIso_hom_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X stupidTrunc Hom.f stupidTruncMap CategoryTheory.Iso.hom stupidTruncXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stupidTruncMap_stupidTruncXIso_hom

---

← Back to Index