FunctorExtension

📁 Source: Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

Statistics

Metric	Count
Definitions map, obj, counitIso, functorExtension, functorExtension₁, functorExtension₁Comp, functorExtension₁CompWhiskeringLeftToKaroubiIso, functorExtension₂, functorExtension₂CompWhiskeringLeftToKaroubiIso, karoubiUniversal, karoubiUniversal₁, karoubiUniversal₂, whiskeringLeftObjToKaroubiFullyFaithful	13
Theorems map_app_f, obj_map_f, obj_obj_X, obj_obj_p, counitIso_hom_app_app_f, counitIso_inv_app_app_f, functorExtension_map_app, functorExtension_obj_map, functorExtension_obj_obj, functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, functorExtension₁_map, functorExtension₁_obj, functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, functorExtension₂_map_app_f, functorExtension₂_obj_map_f, functorExtension₂_obj_obj_X, functorExtension₂_obj_obj_p, instIsEquivalenceFunctorKaroubiFunctorExtension, instIsEquivalenceFunctorKaroubiFunctorExtension₂, instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, karoubiUniversal_functor_eq, karoubiUniversal₁_counitIso, karoubiUniversal₁_functor, karoubiUniversal₁_inverse, karoubiUniversal₁_unitIso, karoubiUniversal₂_functor_eq, natTrans_eq, whiskeringLeft_obj_preimage_app	30
Total	43

CategoryTheory.Idempotents

Definitions

Name	Category	Theorems
functorExtension 📖	CompOp	5 math math: karoubiUniversal_functor_eq, functorExtension_map_app, instIsEquivalenceFunctorKaroubiFunctorExtension, functorExtension_obj_obj, functorExtension_obj_map
functorExtension₁ 📖	CompOp	9 math math: functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, functorExtension₂_map_app_f, karoubiUniversal₁_functor, functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, KaroubiUniversal₁.counitIso_hom_app_app_f, KaroubiUniversal₁.counitIso_inv_app_app_f, karoubiUniversal₁_unitIso, functorExtension₁_obj, functorExtension₁_map
functorExtension₁Comp 📖	CompOp	—
functorExtension₁CompWhiskeringLeftToKaroubiIso 📖	CompOp	3 math math: functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, karoubiUniversal₁_unitIso
functorExtension₂ 📖	CompOp	19 math math: instIsEquivalenceFunctorKaroubiFunctorExtension₂, functorExtension₂_map_app_f, CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj, functorExtension_map_app, functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, CategoryTheory.Abelian.LeftResolution.karoubi_π, functorExtension₂_obj_map_f, functorExtension_obj_obj, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', CategoryTheory.Abelian.LeftResolution.karoubi_F, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, functorExtension₂_obj_obj_X, functorExtension₂_obj_obj_p, functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ, functorExtension_obj_map, karoubiUniversal₂_functor_eq, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi, CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f
functorExtension₂CompWhiskeringLeftToKaroubiIso 📖	CompOp	2 math math: functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f
karoubiUniversal 📖	CompOp	1 math math: karoubiUniversal_functor_eq
karoubiUniversal₁ 📖	CompOp	4 math math: karoubiUniversal₁_functor, karoubiUniversal₁_counitIso, karoubiUniversal₁_unitIso, karoubiUniversal₁_inverse
karoubiUniversal₂ 📖	CompOp	1 math math: karoubiUniversal₂_functor_eq
whiskeringLeftObjToKaroubiFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorExtension_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Karoubi Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Equivalence.inverse toKaroubiEquivalence functorExtension₂ CategoryTheory.Functor.map functorExtension	—	—
functorExtension_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Karoubi Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functorExtension CategoryTheory.Equivalence.inverse toKaroubiEquivalence functorExtension₂	—	—
functorExtension_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functorExtension CategoryTheory.Equivalence.inverse toKaroubiEquivalence functorExtension₂	—	—
functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functorExtension₁ CategoryTheory.Functor.whiskeringLeft toKaroubi CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom functorExtension₁CompWhiskeringLeftToKaroubiIso Karoubi.p	—	—
functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp functorExtension₁ CategoryTheory.Functor.whiskeringLeft toKaroubi CategoryTheory.NatTrans.app CategoryTheory.Iso.inv functorExtension₁CompWhiskeringLeftToKaroubiIso Karoubi.p	—	—
functorExtension₁_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category functorExtension₁ FunctorExtension₁.map	—	—
functorExtension₁_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category functorExtension₁ FunctorExtension₁.obj	—	—
functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functorExtension₂ CategoryTheory.Functor.whiskeringLeft toKaroubi CategoryTheory.Functor.whiskeringRight CategoryTheory.NatTrans.app CategoryTheory.Iso.hom functorExtension₂CompWhiskeringLeftToKaroubiIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight toKaroubi CategoryTheory.Functor.comp functorExtension₂ CategoryTheory.Functor.whiskeringLeft CategoryTheory.NatTrans.app CategoryTheory.Iso.inv functorExtension₂CompWhiskeringLeftToKaroubiIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functorExtension₂_map_app_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.Functor.obj Karoubi Karoubi.instCategory FunctorExtension₁.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight toKaroubi CategoryTheory.NatTrans.app functorExtension₁ CategoryTheory.Functor.map functorExtension₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Karoubi.X Karoubi.p	—	CategoryTheory.NatTrans.naturality
functorExtension₂_obj_map_f 📖	mathematical	—	Karoubi.Hom.f Karoubi.X CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight toKaroubi CategoryTheory.Functor.map Karoubi.p functorExtension₂	—	—
functorExtension₂_obj_obj_X 📖	mathematical	—	Karoubi.X CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functorExtension₂	—	—
functorExtension₂_obj_obj_p 📖	mathematical	—	Karoubi.p CategoryTheory.Functor.obj Karoubi Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functorExtension₂ CategoryTheory.Functor.map Karoubi.X	—	—
instIsEquivalenceFunctorKaroubiFunctorExtension 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor CategoryTheory.Functor.category Karoubi Karoubi.instCategory functorExtension	—	karoubiUniversal_functor_eq CategoryTheory.Equivalence.isEquivalence_functor
instIsEquivalenceFunctorKaroubiFunctorExtension₂ 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor CategoryTheory.Functor.category Karoubi Karoubi.instCategory functorExtension₂	—	karoubiUniversal₂_functor_eq CategoryTheory.Equivalence.isEquivalence_functor
instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft toKaroubi	—	toKaroubi_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.isEquivalence_of_comp_right CategoryTheory.Functor.isEquivalence_trans CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight CategoryTheory.Functor.isEquivalence_inv
karoubiUniversal_functor_eq 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal functorExtension	—	—
karoubiUniversal₁_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal₁ KaroubiUniversal₁.counitIso	—	—
karoubiUniversal₁_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal₁ functorExtension₁	—	—
karoubiUniversal₁_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal₁ CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft toKaroubi	—	—
karoubiUniversal₁_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal₁ CategoryTheory.Iso.symm CategoryTheory.Functor.comp functorExtension₁ CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft toKaroubi CategoryTheory.Functor.id functorExtension₁CompWhiskeringLeftToKaroubiIso	—	—
karoubiUniversal₂_functor_eq 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Functor Karoubi Karoubi.instCategory CategoryTheory.Functor.category karoubiUniversal₂ functorExtension₂	—	—
natTrans_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Karoubi Karoubi.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Karoubi.X CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map Karoubi.decompId_i Karoubi.decompId_p	—	CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id Karoubi.decompId
whiskeringLeft_obj_preimage_app 📖	mathematical	—	CategoryTheory.NatTrans.app Karoubi Karoubi.instCategory CategoryTheory.Functor.preimage CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft toKaroubi CategoryTheory.Functor.IsEquivalence.full instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Karoubi.X CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map Karoubi.decompId_i CategoryTheory.Functor.comp Karoubi.decompId_p	—	CategoryTheory.Functor.IsEquivalence.full instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi natTrans_eq CategoryTheory.congr_app CategoryTheory.Functor.map_preimage

CategoryTheory.Idempotents.FunctorExtension₁

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: map_app_f, CategoryTheory.Idempotents.functorExtension₁_map
obj 📖	CompOp	6 math math: CategoryTheory.Idempotents.functorExtension₂_map_app_f, obj_obj_X, obj_obj_p, obj_map_f, map_app_f, CategoryTheory.Idempotents.functorExtension₁_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory obj CategoryTheory.NatTrans.app map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.p	—	—
obj_map_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.p obj	—	—
obj_obj_X 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory obj	—	—
obj_obj_p 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.p CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory obj CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.map	—	—

CategoryTheory.Idempotents.KaroubiUniversal₁

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	3 math math: counitIso_hom_app_app_f, counitIso_inv_app_app_f, CategoryTheory.Idempotents.karoubiUniversal₁_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIso_hom_app_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Idempotents.toKaroubi CategoryTheory.Idempotents.functorExtension₁ CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom counitIso CategoryTheory.Idempotents.Karoubi.X CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.decompId_p	—	—
counitIso_inv_app_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Idempotents.toKaroubi CategoryTheory.Idempotents.functorExtension₁ CategoryTheory.NatTrans.app CategoryTheory.Iso.inv counitIso CategoryTheory.Idempotents.Karoubi.X CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.decompId_i	—	—

---

← Back to Index