mapPullbackAdj — Mathlib

English

There is an adjunction: map f is left adjoint to pullback f.

Русский

Существует смежность: map f является левой смежностью к pullback f.

LaTeX

$$$\mathrm{map} f \dashv \mathrm{pullback} f$$$

Lean4

/-- `map f : Subobject X ⥤ Subobject Y` is
the left adjoint of `pullback f : Subobject Y ⥤ Subobject X`. -/
def mapPullbackAdj [HasPullbacks C] (f : X ⟶ Y) [Mono f] : map f ⊣ pullback f :=
  lowerAdjunction (MonoOver.mapPullbackAdj f)

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