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. For X : F.PartialLeftAdjointSource and Y : D, 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D C) : ObjectProperty C

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.

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

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

@[reducible, inline]

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

The full subcategory where F.partialLeftAdjoint shall be defined.

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

noncomputable def CategoryTheory.Functor.partialLeftAdjointObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : 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).

noncomputable def CategoryTheory.Functor.partialLeftAdjointHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : 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.

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

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

Auxiliary definition for leftAdjointObjIsDefined_of_isColimit.

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

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

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

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

theorem CategoryTheory.Functor.rightAdjointObjIsDefined_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (Y : D) : F.rightAdjointObjIsDefined Y ↔ (F.op.comp (yoneda.obj Y)).IsRepresentable

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

@[reducible, inline]

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

The full subcategory where F.partialRightAdjoint shall be defined.

instance CategoryTheory.Functor.instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (Y : F.PartialRightAdjointSource) : (F.op.comp (yoneda.obj Y.obj)).IsRepresentable

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

Given F : C ⥤ D, this is F.partialRightAdjoint on objects: it sends X : D such that F.rightAdjointObjIsDefined X holds to an object of C which represents the functor F.op ⋙ yoneda.obj X.obj.

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

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

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : X' ⟶ F.partialRightAdjointObj Y) (g : X ⟶ X') : F.partialRightAdjointHomEquiv (CategoryStruct.comp g f) = CategoryStruct.comp (F.map g) (F.partialRightAdjointHomEquiv f)

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

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

@[simp]

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : F.PartialRightAdjointSource} (f : X ⟶ Y) : F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) = CategoryStruct.comp (F.partialRightAdjointHomEquiv (CategoryStruct.id (F.partialRightAdjointObj X))) f.hom

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : X ⟶ F.partialRightAdjointObj Y) (g : Y ⟶ Y') : F.partialRightAdjointHomEquiv (CategoryStruct.comp f (F.partialRightAdjointMap g)) = CategoryStruct.comp (F.partialRightAdjointHomEquiv f) g.hom

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : F.obj X' ⟶ Y.obj) (g : X ⟶ X') : CategoryStruct.comp g (F.partialRightAdjointHomEquiv.symm f) = F.partialRightAdjointHomEquiv.symm (CategoryStruct.comp (F.map g) f)

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : F.obj X' ⟶ Y.obj) (g : X ⟶ X') {Z : C} (h : F.partialRightAdjointObj Y ⟶ Z) : CategoryStruct.comp g (CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f) h) = CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm (CategoryStruct.comp (F.map g) f)) h

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : F.obj X ⟶ Y.obj) (g : Y ⟶ Y') : CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f) (F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv.symm (CategoryStruct.comp f g.hom)

theorem CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : F.obj X ⟶ Y.obj) (g : Y ⟶ Y') {Z : C} (h : F.partialRightAdjointObj Y' ⟶ Z) : CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f) (CategoryStruct.comp (F.partialRightAdjointMap g) h) = CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm (CategoryStruct.comp f g.hom)) h

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

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

@[simp]

theorem CategoryTheory.Functor.partialRightAdjoint_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (Y : F.PartialRightAdjointSource) : F.partialRightAdjoint.obj Y = F.partialRightAdjointObj Y

@[simp]

theorem CategoryTheory.Functor.partialRightAdjoint_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : F.PartialRightAdjointSource} (f : X✝ ⟶ Y✝) : F.partialRightAdjoint.map f = F.partialRightAdjointMap f

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

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

noncomputable def CategoryTheory.Functor.representableByCompYonedaObjOfIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {J : Type u_1} [Category.{v_1, u_1} J] {R : Functor J F.PartialRightAdjointSource} {c : Limits.Cone (R.comp F.rightAdjointObjIsDefined.ι)} (hc : Limits.IsLimit c) {c' : Limits.Cone (R.comp F.partialRightAdjoint)} (hc' : Limits.IsLimit c') : (F.op.comp (yoneda.obj c.pt)).RepresentableBy c'.pt

Auxiliary definition for rightAdjointObjIsDefined_of_isLimit.

theorem CategoryTheory.Functor.rightAdjointObjIsDefined_of_isLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {J : Type u_1} [Category.{v_1, u_1} J] {R : Functor J D} {c : Limits.Cone R} (hc : Limits.IsLimit c) [Limits.HasLimitsOfShape J C] (h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) : F.rightAdjointObjIsDefined c.pt

theorem CategoryTheory.Functor.rightAdjointObjIsDefined_limit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {J : Type u_1} [Category.{v_1, u_1} J] (R : Functor J D) [Limits.HasLimit R] [Limits.HasLimitsOfShape J C] (h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) : F.rightAdjointObjIsDefined (Limits.limit R)