Quotient

📁 Source: Mathlib/CategoryTheory/Shift/Quotient.lean

Statistics

Metric	Count
Definitions quotient, iso, functor_commShift, liftCommShift, IsCompatibleWithShift	5
Theorems iso_hom_app, iso_inv_app, liftCommShift_commShiftIso, liftCommShift_compatibility, condition	5
Total	10

CategoryTheory.HasShift

Definitions

Name	Category	Theorems
quotient 📖	CompOp	4 math math: CategoryTheory.Quotient.LiftCommShift.iso_hom_app, CategoryTheory.Quotient.liftCommShift_compatibility, CategoryTheory.Quotient.liftCommShift_commShiftIso, CategoryTheory.Quotient.LiftCommShift.iso_inv_app

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
functor_commShift 📖	CompOp	3 math math: LiftCommShift.iso_hom_app, liftCommShift_compatibility, LiftCommShift.iso_inv_app
liftCommShift 📖	CompOp	2 math math: liftCommShift_compatibility, liftCommShift_commShiftIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftCommShift_commShiftIso 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Quotient category lift CategoryTheory.HasShift.quotient liftCommShift LiftCommShift.iso	—	—
liftCommShift_compatibility 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.NatTrans.CommShift CategoryTheory.Functor.comp CategoryTheory.Quotient category functor lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category lift.isLift CategoryTheory.Functor.CommShift.comp CategoryTheory.HasShift.quotient functor_commShift liftCommShift	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.commShiftIso_comp_hom_app liftCommShift_commShiftIso LiftCommShift.iso_hom_app CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id

CategoryTheory.Quotient.LiftCommShift

Definitions

Name	Category	Theorems
iso 📖	CompOp	3 math math: iso_hom_app, CategoryTheory.Quotient.liftCommShift_commShiftIso, iso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom_app 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor CategoryTheory.HasShift.quotient CategoryTheory.Quotient.lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.Functor.obj CategoryTheory.Quotient.functor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Quotient.functor_commShift	—	CategoryTheory.Quotient.natTransLift_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
iso_inv_app 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Functor.comp CategoryTheory.Quotient.lift CategoryTheory.shiftFunctor CategoryTheory.HasShift.quotient CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.Functor.obj CategoryTheory.Quotient.functor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Iso.hom CategoryTheory.Quotient.functor_commShift	—	CategoryTheory.Quotient.natTransLift_app CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id

HomRel

Definitions

Name	Category	Theorems
IsCompatibleWithShift 📖	CompData	1 math math: HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic

HomRel.IsCompatibleWithShift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.shiftFunctor CategoryTheory.Functor.map	—	—

---

← Back to Index