English
Let J be a category and R : J ⥤ D. If HasLimit R and HasLimitsOfShape J C, then for any h : ∀ j : J, F.rightAdjointObjIsDefined (R.obj j) we have F.rightAdjointObjIsDefined (limit R).
Русский
Пусть J — категория, R : J ⥤ D. Если существует предел у R и в C существуют пределы формы J, то при любом заданном условии h: ∀ j, F.rightAdjointObjIsDefined (R.obj j) правая сопряжённая существует на пределе limit R.
LaTeX
$$$[HasLimit R] \\; [HasLimitsOfShape J C] \\; (\\forall j : J, F.rightAdjointObjIsDefined (R.obj j)) \\Rightarrow F.rightAdjointObjIsDefined (limit R)$$$
Lean4
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `F` (and hence also `R`) is fully faithful, all
components of the natural transformation `G ⟶ L` are epimorphisms iff all components of the natural
transformation `F ⟶ R` are monomorphisms. -/
theorem epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app :
(∀ X, Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ X, Mono (q.rightTriple.leftToRight.app X) :=
by
simp_rw [mono_leftToRight_app_iff_mono_adj₂_unit_app, rightToLeft_eq_counits]
dsimp
simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.id_obj, whiskerLeft_app, Category.comp_id,
Category.id_comp]
simp_rw [epi_comp_iff_of_epi, epi_iff_forall_injective, mono_iff_forall_injective]
rw [forall_comm]
refine forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_
rw [← (q.adj₁.homEquiv _ _).comp_injective _]
simp_rw [Function.comp_def, q.adj₁.homEquiv_naturality_left]
refine ((q.adj₁.homEquiv _ _).injective_comp fun f ↦ _).trans ?_
rw [← ((q.adj₂.homEquiv _ _).trans (q.adj₃.homEquiv _ _)).comp_injective _]
simp [Function.comp_def, ← q.adj₂.homEquiv_symm_id, ← q.adj₂.homEquiv_naturality_right_symm, ← q.adj₃.homEquiv_id,
← q.adj₃.homEquiv_naturality_left]
