English
If two morphisms in a binary bicone coincide on the underlying hom component, then they are identical.
Русский
Если два морфизма в бинарном bicone совпадают по фундаментальному компоненту, то они совпадают.
LaTeX
$$$$ f.hom = g.hom \;\Rightarrow\; f = g $$$$
Lean4
@[ext]
theorem hom_ext {Φ : uliftYoneda.{max w v₂}.LeftExtension (F ⋙ uliftYoneda.{max w v₁})}
(f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ) : f = g :=
by
ext P : 3
apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)
apply (colimitOfRepresentable.{max w v₂} P).hom_ext
intro x
have eq := F.op.lanUnit.naturality (uliftYonedaEquiv.{max w v₂}.symm x.unop.2)
have eq₁ := congr_fun (congr_app (congr_app (StructuredArrow.w f) x.unop.1.unop) (F.op.obj x.unop.1)) (ULift.up (𝟙 _))
have eq₂ := congr_fun (congr_app (congr_app (StructuredArrow.w g) x.unop.1.unop) (F.op.obj x.unop.1)) (ULift.up (𝟙 _))
dsimp at eq₁ eq₂ eq ⊢
simp only [reassoc_of% eq, ← Functor.whiskerLeft_comp]
congr 2
simp only [← cancel_epi ((compULiftYonedaIsoULiftYonedaCompLan F).hom.app x.unop.1.unop), NatTrans.naturality]
apply uliftYonedaEquiv.injective
dsimp [uliftYonedaEquiv_apply]
rw [eq₁, eq₂]
