Restricting adjunctions #
Adjunction.restrictFullyFaithful shows that an adjunction can be restricted along fully faithful
inclusions.
noncomputable def
CategoryTheory.Adjunction.restrictFullyFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
:
L ⊣ R
If C is a full subcategory of C' and D is a full subcategory of D', then we can restrict
an adjunction L' ⊣ R' where L' : C' ⥤ D' and R' : D' ⥤ C' to C and D.
The construction here is slightly more general, in that C is required only to have a full and
faithful "inclusion" functor iC : C ⥤ C' (and similarly iD : D ⥤ D') which commute (up to
natural isomorphism) with the proposed restrictions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
(X : C)
:
iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
(CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (comm2.hom.app (L.obj X)))
theorem
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
(X : C)
{Z : C'}
(h : iC.obj (R.obj (L.obj X)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X)) h = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
(CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X))
(CategoryTheory.CategoryStruct.comp (comm2.hom.app (L.obj X)) h))
@[simp]
theorem
CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
(X : D)
:
iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X))
(CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))
theorem
CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
(X : D)
{Z : D'}
(h : iD.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X)) h = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X))
(CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X))
(CategoryTheory.CategoryStruct.comp (adj.counit.app (iD.obj X)) h))
theorem
CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{C' : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C']
{D' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D']
{iC : CategoryTheory.Functor C C'}
{iD : CategoryTheory.Functor D D'}
{L' : CategoryTheory.Functor C' D'}
{R' : CategoryTheory.Functor D' C'}
(adj : L' ⊣ R')
(hiC : iC.FullyFaithful)
(hiD : iD.FullyFaithful)
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : iC.comp L' ≅ L.comp iD)
(comm2 : iD.comp R' ≅ R.comp iC)
{X : C}
{Y : D}
(f : L.obj X ⟶ Y)
:
((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f = hiC.preimage
(CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
(CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X))
(CategoryTheory.CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))