coe_pullback

Mathlib.CategoryTheory.Sites.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.Cover.coe_pullback

English

For S a covering sieve on X, f:Y→X and g:Z→Y, we have (S.pullback f).g iff S(g∘f).

Русский

Для покрытия S на X, морфизмов f:Y→X и g:Z→Y, верно: (S.pullback f).g эквивалентно S(g∘f).

LaTeX

$$$(S.pullback f).g \iff S (g \circ f)$$$

Lean4

@[simp]
theorem coe_pullback {Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) (S : J.Cover X) : (S.pullback f) g ↔ S (g ≫ f) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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