Theorems · Definition · category theory
CategoryTheory.FreeBicategory.liftHom
{B : Type u₁} →
[inst : Quiver B] →
{C : Type u₂} →
[inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] →
(F : B ⥤q C) → {a b : CategoryTheory.FreeBicategory B} → (a ⟶ b) → (F.obj a ⟶ F.obj b)Auxiliary definition for lift.
- Defined in
- Mathlib.CategoryTheory.Bicategory.Free
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- Prefunctor.objstatement · cited by 1,241
- Quiverstatement and proof · cited by 405
- CategoryTheory.CategoryStructstatement and proof · cited by 343
- Prefunctorstatement and proof · cited by 116
- CategoryTheory.FreeBicategorystatement and proof · cited by 51
- CategoryTheory.FreeBicategory.Hom.brecOnproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- CategoryTheory.FreeBicategory.liftproof · cited by 5
- CategoryTheory.FreeBicategory.liftHom₂statement · cited by 2
- CategoryTheory.FreeBicategory.liftHom₂_congrstatement and proof · cited by 1
- CategoryTheory.FreeBicategory.liftHom_idstatement · cited by 0
- CategoryTheory.FreeBicategory.lift_mapCompstatement · cited by 0
- CategoryTheory.FreeBicategory.lift_mapIdstatement · cited by 0
- CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂statement · cited by 0
- CategoryTheory.FreeBicategory.liftHom.eq_defstatement and proof · cited by 0
- CategoryTheory.FreeBicategory.liftHom_compstatement · cited by 0