instHasPullbacks — Mathlib

English

If the base category C has pullbacks, then the over category Over B also has pullbacks.

Русский

Если в базовой категории C существуют pullbacks, то в перекрёстной категории Over B тоже есть pullbacks.

LaTeX

$$$\text{HasPullbacks}(Over B) \quad\text{provided } \text{HasPullbacks}(C).$$$

Lean4

/-- Make sure we can derive pullbacks in `Over B`. -/
instance {B : C} [HasPullbacks C] : HasPullbacks (Over B) :=
  inferInstance

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