existsPullbackAdj — Mathlib

English

exists f is left adjoint to pullback f when appropriate conditions hold (HasImages, HasPullbacks).

Русский

exists f является левой смежностью к pullback f при подходящих условиях (HasImages, HasPullbacks).

LaTeX

$$$\existsPullbackAdj\ f : \mathrm{Subobject}(X) \dashv \mathrm{pullback}(f)$$$

Lean4

/-- `exists f : Subobject X ⥤ Subobject Y` is
left adjoint to `pullback f : Subobject Y ⥤ Subobject X`.
-/
def existsPullbackAdj (f : X ⟶ Y) [HasPullbacks C] : «exists» f ⊣ pullback f :=
  lowerAdjunction (MonoOver.existsPullbackAdj f)

Похожие утверждения