Domain of definition of the partial left adjoint

Given a functor F : D ⥤ C, we define a functor F.partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ D which is defined on the full subcategory of C consisting of those objects X : C such that F ⋙ coyoneda.obj (op X) : D ⥤ Type _ is corepresentable. We have a natural bijection (F.partialLeftAdjoint.obj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y) that is similar to what we would expect for the image of the object X by the left adjoint of F, if such an adjoint existed.

Indeed, if the predicate F.LeftAdjointObjIsDefined which defines the F.PartialLeftAdjointSource holds for all objects X : C, then F has a left adjoint.

When colimits indexed by a category J exist in D, we show that the predicate F.LeftAdjointObjIsDefined is stable under colimits indexed by J.

TODO

• consider dualizing the results to right adjoints

def CategoryTheory.Functor.LeftAdjointObjIsDefined {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (X : C) : Prop

Given a functor F : D ⥤ C, this is a predicate on objects X : C corresponding to the domain of definition of the (partial) left adjoint of F.

Equations

• F.LeftAdjointObjIsDefined X = (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).IsCorepresentable

theorem CategoryTheory.Functor.leftAdjointObjIsDefined_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (X : C) : F.LeftAdjointObjIsDefined X ↔ (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).IsCorepresentable

theorem CategoryTheory.Functor.leftAdjointObjIsDefined_of_adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D} (adj : G ⊣ F) (X : C) : F.LeftAdjointObjIsDefined X

@[reducible, inline]

abbrev CategoryTheory.Functor.PartialLeftAdjointSource {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) : Type u₁

The full subcategory where F.partialLeftAdjoint shall be defined.

Equations

• F.PartialLeftAdjointSource = CategoryTheory.FullSubcategory F.LeftAdjointObjIsDefined

instance CategoryTheory.Functor.instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (X : F.PartialLeftAdjointSource) : (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X.obj))).IsCorepresentable

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.partialLeftAdjointObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (X : F.PartialLeftAdjointSource) : D

Given F : D ⥤ C, this is F.partialLeftAdjoint on objects: it sends X : C such that F.LeftAdjointObjIsDefined X holds to an object of D which represents the functor F ⋙ coyoneda.obj (op X.obj).

Equations

• F.partialLeftAdjointObj X = (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X.obj))).coreprX

noncomputable def CategoryTheory.Functor.partialLeftAdjointHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y : D} : (F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y)

Given F : D ⥤ C, this is the canonical bijection (F.partialLeftAdjointObj X ⟶ Y) ≃ (X.obj ⟶ F.obj Y) for all X : F.PartialLeftAdjointSource and Y : D.

Equations

• F.partialLeftAdjointHomEquiv = (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X.obj))).corepresentableBy.homEquiv

theorem CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y : D} {Y' : D} (f : F.partialLeftAdjointObj X ⟶ Y) (g : Y ⟶ Y') : F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv f) (F.map g)

noncomputable def CategoryTheory.Functor.partialLeftAdjointMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y : F.PartialLeftAdjointSource} (f : X ⟶ Y) : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Y

Given F : D ⥤ C, this is F.partialLeftAdjoint on morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.partialLeftAdjointHomEquiv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y : F.PartialLeftAdjointSource} (f : X ⟶ Y) : F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) = CategoryTheory.CategoryStruct.comp f (F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.id (F.partialLeftAdjointObj Y)))

theorem CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {X' : F.PartialLeftAdjointSource} {Y : D} (f : X ⟶ X') (g : F.partialLeftAdjointObj X' ⟶ Y) : F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointMap f) g) = CategoryTheory.CategoryStruct.comp f (F.partialLeftAdjointHomEquiv g)

@[simp]

theorem CategoryTheory.Functor.partialLeftAdjoint_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (X : F.PartialLeftAdjointSource) : F.partialLeftAdjoint.obj X = F.partialLeftAdjointObj X

@[simp]

theorem CategoryTheory.Functor.partialLeftAdjoint_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) : ∀ {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y), F.partialLeftAdjoint.map f = F.partialLeftAdjointMap f

noncomputable def CategoryTheory.Functor.partialLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor F.PartialLeftAdjointSource D

Given F : D ⥤ C, this is the partial adjoint functor F.PartialLeftAdjointSource ⥤ D.

Equations

• F.partialLeftAdjoint = { obj := F.partialLeftAdjointObj, map := fun {X Y : F.PartialLeftAdjointSource} => F.partialLeftAdjointMap, map_id := ⋯, map_comp := ⋯ }

theorem CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} (h : F.LeftAdjointObjIsDefined = ⊤) : F.IsRightAdjoint

theorem CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) : F.IsRightAdjoint ↔ F.LeftAdjointObjIsDefined = ⊤

noncomputable def CategoryTheory.Functor.corepresentableByCompCoyonedaObjOfIsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {R : CategoryTheory.Functor J F.PartialLeftAdjointSource} {c : CategoryTheory.Limits.Cocone (R.comp (CategoryTheory.fullSubcategoryInclusion F.LeftAdjointObjIsDefined))} (hc : CategoryTheory.Limits.IsColimit c) {c' : CategoryTheory.Limits.Cocone (R.comp F.partialLeftAdjoint)} (hc' : CategoryTheory.Limits.IsColimit c') : (F.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt))).CorepresentableBy c'.pt

Auxiliary definition for leftAdjointObjIsDefined_of_isColimit.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {R : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone R} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.HasColimitsOfShape J D] (h : ∀ (j : J), F.LeftAdjointObjIsDefined (R.obj j)) : F.LeftAdjointObjIsDefined c.pt

theorem CategoryTheory.Functor.leftAdjointObjIsDefined_colimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (R : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit R] [CategoryTheory.Limits.HasColimitsOfShape J D] (h : ∀ (j : J), F.LeftAdjointObjIsDefined (R.obj j)) : F.LeftAdjointObjIsDefined (CategoryTheory.Limits.colimit R)