English
There exists a natural equivalence between morphisms from the constructed left adjoint applied to X into Y and morphisms from X to R(Y).
Русский
Существует естественное эквивалентное соответствие между морфизмами из образа строящегося левого сопряжения применённого к X в Y и морфизмами из X в R(Y).
LaTeX
$$$$(\\mathrm{constructLeftAdjointObj}\\, R\\, F'\\, adj_1\\, adj_2\\, X) \\longrightarrow Y\\;\\cong\\; (X \\longrightarrow R(X)\\, Y)$$$$
Lean4
/-- The homset equivalence which helps show that `R` is a right adjoint. -/
@[simps!]
noncomputable def constructLeftAdjointEquiv [∀ X : B, RegularEpi (adj₁.counit.app X)] (Y : A) (X : B) :
(constructLeftAdjointObj _ _ adj₁ adj₂ X ⟶ Y) ≃ (X ⟶ R.obj Y) :=
calc
(constructLeftAdjointObj _ _ adj₁ adj₂ X ⟶ Y) ≃
{ f : F'.obj (U.obj X) ⟶ Y // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap _ _ adj₁ adj₂ _ ≫ f } :=
Cofork.IsColimit.homIso (colimit.isColimit _) _
_ ≃ { g : U.obj X ⟶ U.obj (R.obj Y) // U.map (F.map g ≫ adj₁.counit.app _) = U.map (adj₁.counit.app _) ≫ g } :=
by
apply (adj₂.homEquiv _ _).subtypeEquiv _
intro f
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left, otherMap, assoc,
adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality, adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit,
adj₂.right_triangle_components, comp_id, Functor.comp_map, ← U.map_comp, assoc, ← adj₁.counit_naturality,
adj₂.homEquiv_unit, adj₂.homEquiv_unit, F.map_comp, assoc]
rfl
_ ≃ { z : F.obj (U.obj X) ⟶ R.obj Y // _ } :=
by
apply (adj₁.homEquiv _ _).symm.subtypeEquiv
intro g
rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit, adj₁.homEquiv_counit, adj₁.homEquiv_counit,
F.map_comp, assoc, U.map_comp, F.map_comp, assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
apply eq_comm
_ ≃ (X ⟶ R.obj Y) := (Cofork.IsColimit.homIso (counitCoequalises adj₁ X) _).symm
