lower — Mathlib

English

An adjunction between MonoOver A and MonoOver B descends to an adjunction between Subobject A and Subobject B via lowering.

Русский

Соседство между MonoOver A и MonoOver B переходит к соседству между Subobject A и Subobject B через понижение.

LaTeX

$$$\text{lowerAdjunction } L R : \text{lower } L \dashv \text{lower } R$ given an adjunction $L \dashv R$$$

Lean4

/-- Any functor `MonoOver X ⥤ MonoOver Y` descends to a functor
`Subobject X ⥤ Subobject Y`, because `MonoOver Y` is thin. -/
def lower {Y : D} (F : MonoOver X ⥤ MonoOver Y) : Subobject X ⥤ Subobject Y :=
  ThinSkeleton.map F

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