Commit 2023-04-06 15:15 37b23dab

View on Github →

feat: port CategoryTheory.Idempotents.FunctorExtension (#3300)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

added def CategoryTheory.Idempotents.FunctorExtension₁.map

added def CategoryTheory.Idempotents.FunctorExtension₁.obj

added def CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso

added def CategoryTheory.Idempotents.functorExtension₁

added theorem CategoryTheory.Idempotents.functorExtension₁_comp

added theorem CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi

added def CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi_iso

added def CategoryTheory.Idempotents.functorExtension₂

added def CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso

added theorem CategoryTheory.Idempotents.functorExtension₂_comp_whiskeringLeft_toKaroubi

added theorem CategoryTheory.Idempotents.isEquivalence_whiskeringLeft_obj_toKaroubi_aux

added theorem CategoryTheory.Idempotents.karoubiUniversal_functor_eq

added def CategoryTheory.Idempotents.karoubiUniversal₁

added theorem CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq

added theorem CategoryTheory.Idempotents.natTrans_eq

added theorem CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app