instHasPullbacksSingletonOfHasPullback

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.instHasPullbacksSingletonOfHasPullback

English

If g→X has a pullback with f, then the presieve (singleton g) has pullbacks along f.

Русский

Если у g: Z→X есть расслойка pullback с f, то presieve (singleton g) имеет pullbacks по f.

LaTeX

$$$\\text{singleton } g \\;\\text{HasPullbacks } f$ given $\\HasPullback g f$.$$

Lean4

instance (g : Z ⟶ X) [HasPullback g f] : (singleton g).HasPullbacks f where
  hasPullback {Z}
    h := by
    intro ⟨⟩
    infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru