functorPullback_monotone

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.functorPullback_monotone

← MathLib Explorer

English

For a fixed F, R ↦ R.pullback F is monotone.

Русский

Для фиксированного функторa F отображение R.pullback F монотонно.

LaTeX

$$$ R \\le T \\Rightarrow R.pullback F \\le T.pullback F $$$

Lean4

theorem functorPullback_monotone (X : C) : Monotone (Sieve.functorPullback F : Sieve (F.obj X) → Sieve X) :=
  (functor_galoisConnection F X).monotone_u

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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