FunctorEquivalence

📁 Source: Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean

Statistics

Metric	Count
Definitions counitIso, functor, inverse, unitIso, functorEquivalence	5
Theorems counitIso_hom_app_app_τ₁, counitIso_hom_app_app_τ₂, counitIso_hom_app_app_τ₃, counitIso_inv_app_app_τ₁, counitIso_inv_app_app_τ₂, counitIso_inv_app_app_τ₃, functor_map_app, functor_obj_map, functor_obj_obj, inverse_map_τ₁, inverse_map_τ₂, inverse_map_τ₃, inverse_obj_X₁, inverse_obj_X₂, inverse_obj_X₃, inverse_obj_f, inverse_obj_g, unitIso_hom_app_τ₁_app, unitIso_hom_app_τ₂_app, unitIso_hom_app_τ₃_app, unitIso_inv_app_τ₁_app, unitIso_inv_app_τ₂_app, unitIso_inv_app_τ₃_app, functorEquivalence_counitIso, functorEquivalence_functor, functorEquivalence_inverse, functorEquivalence_unitIso	27
Total	32

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
functorEquivalence 📖	CompOp	4 math math: functorEquivalence_counitIso, functorEquivalence_functor, functorEquivalence_unitIso, functorEquivalence_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.ShortComplex CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor instCategory functorEquivalence FunctorEquivalence.counitIso	—	—
functorEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.ShortComplex CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor instCategory functorEquivalence FunctorEquivalence.functor	—	—
functorEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.ShortComplex CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor instCategory functorEquivalence FunctorEquivalence.inverse	—	—
functorEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.ShortComplex CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor instCategory functorEquivalence FunctorEquivalence.unitIso	—	—

CategoryTheory.ShortComplex.FunctorEquivalence

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	7 math math: counitIso_inv_app_app_τ₁, counitIso_inv_app_app_τ₂, CategoryTheory.ShortComplex.functorEquivalence_counitIso, counitIso_inv_app_app_τ₃, counitIso_hom_app_app_τ₁, counitIso_hom_app_app_τ₂, counitIso_hom_app_app_τ₃
functor 📖	CompOp	16 math math: counitIso_inv_app_app_τ₁, counitIso_inv_app_app_τ₂, unitIso_inv_app_τ₂_app, unitIso_inv_app_τ₁_app, CategoryTheory.ShortComplex.functorEquivalence_functor, unitIso_hom_app_τ₃_app, counitIso_inv_app_app_τ₃, functor_obj_map, counitIso_hom_app_app_τ₁, unitIso_inv_app_τ₃_app, functor_obj_obj, unitIso_hom_app_τ₁_app, functor_map_app, counitIso_hom_app_app_τ₂, unitIso_hom_app_τ₂_app, counitIso_hom_app_app_τ₃
inverse 📖	CompOp	21 math math: counitIso_inv_app_app_τ₁, counitIso_inv_app_app_τ₂, unitIso_inv_app_τ₂_app, unitIso_inv_app_τ₁_app, unitIso_hom_app_τ₃_app, inverse_obj_X₂, counitIso_inv_app_app_τ₃, inverse_obj_X₃, inverse_map_τ₁, inverse_obj_X₁, counitIso_hom_app_app_τ₁, inverse_obj_f, unitIso_inv_app_τ₃_app, unitIso_hom_app_τ₁_app, counitIso_hom_app_app_τ₂, CategoryTheory.ShortComplex.functorEquivalence_inverse, inverse_obj_g, unitIso_hom_app_τ₂_app, counitIso_hom_app_app_τ₃, inverse_map_τ₃, inverse_map_τ₂
unitIso 📖	CompOp	7 math math: unitIso_inv_app_τ₂_app, unitIso_inv_app_τ₁_app, unitIso_hom_app_τ₃_app, unitIso_inv_app_τ₃_app, unitIso_hom_app_τ₁_app, CategoryTheory.ShortComplex.functorEquivalence_unitIso, unitIso_hom_app_τ₂_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIso_hom_app_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁	—	—
counitIso_hom_app_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂	—	—
counitIso_hom_app_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃	—	—
counitIso_inv_app_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁	—	—
counitIso_inv_app_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂	—	—
counitIso_inv_app_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Limits.instHasZeroMorphismsFunctor inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃	—	—
functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.Functor.map functor CategoryTheory.Functor.mapShortComplex	—	CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj
functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor functor CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj	—	CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj
functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor functor CategoryTheory.ShortComplex.map CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj	—	—
inverse_map_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.comp CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.π₁ CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₃ CategoryTheory.Functor.whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ CategoryTheory.Functor.map inverse CategoryTheory.Functor.whiskerRight	—	—
inverse_map_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.comp CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.π₁ CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₃ CategoryTheory.Functor.whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ CategoryTheory.Functor.map inverse CategoryTheory.Functor.whiskerRight	—	—
inverse_map_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.comp CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.π₁ CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₃ CategoryTheory.Functor.whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ CategoryTheory.Functor.map inverse CategoryTheory.Functor.whiskerRight	—	—
inverse_obj_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory inverse CategoryTheory.Functor.comp CategoryTheory.ShortComplex.π₁	—	—
inverse_obj_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory inverse CategoryTheory.Functor.comp CategoryTheory.ShortComplex.π₂	—	—
inverse_obj_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory inverse CategoryTheory.Functor.comp CategoryTheory.ShortComplex.π₃	—	—
inverse_obj_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory inverse CategoryTheory.Functor.whiskerLeft CategoryTheory.ShortComplex.π₁ CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₁Toπ₂	—	—
inverse_obj_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory inverse CategoryTheory.Functor.whiskerLeft CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₃ CategoryTheory.ShortComplex.π₂Toπ₃	—	—
unitIso_hom_app_τ₁_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Iso.hom unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unitIso_hom_app_τ₂_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₂ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Iso.hom unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unitIso_hom_app_τ₃_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₃ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Iso.hom unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unitIso_inv_app_τ₁_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Iso.inv unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unitIso_inv_app_τ₂_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₂ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Iso.inv unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unitIso_inv_app_τ₃_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.X₃ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Iso.inv unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index