English
The above equivalence is constructed via a chain of isomorphisms between appropriate hom-sets, using coequalizers and adjunctions.
Русский
Указанная эквивалентность строится как цепочка изоморий между подходящими множествами гомотрезков, используя коэквалайзеры и сопряжения.
LaTeX
$$$\\text{(construction via coequalizers and adjunctions gives } \\mathrm{Hom}(L_A,B) \\cong \\mathrm{Hom}(A, (\\mathrm{comparison} \\;adj).\\mathrm{obj} B)\\text{).}$$$
Lean4
/-- We have a bijection of homsets which will be used to construct the left adjoint to the comparison
functor.
-/
@[simps!]
def comparisonLeftAdjointHomEquiv (A : adj.toMonad.Algebra) (B : D)
[HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] :
(comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B) :=
calc
(comparisonLeftAdjointObj adj A ⟶ B) ≃ { f : F.obj A.A ⟶ B // _ } := Cofork.IsColimit.homIso (colimit.isColimit _) B
_ ≃ { g : A.A ⟶ G.obj B // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g } :=
by
refine (adj.homEquiv _ _).subtypeEquiv ?_
intro f
rw [← (adj.homEquiv _ _).injective.eq_iff, Adjunction.homEquiv_naturality_left, adj.homEquiv_unit,
adj.homEquiv_unit, G.map_comp]
dsimp
rw [adj.right_triangle_components_assoc, ← G.map_comp, F.map_comp, Category.assoc, adj.counit_naturality,
adj.left_triangle_components_assoc]
apply eq_comm
_ ≃ (A ⟶ (comparison adj).obj B) :=
{ toFun := fun g =>
{ f := _
h := g.prop }
invFun := fun f => ⟨f.f, f.h⟩ }
