coverPreserving

Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsDenseSubsite.coverPreserving

English

G preserves coverings: maps a cover in J to a cover in K via pushforward/pullback relations.

Русский

G сохраняет покрытия: отображает покрытие в J в покрытие в K через соответствия pushforward/pullback.

LaTeX

$$$\text{CoverPreserving}(J,K,G)$$$

Lean4

theorem coverPreserving : CoverPreserving J K G :=
  ⟨functorPushforward_mem_iff.mpr⟩

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

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

Разделы

Аффилиация

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