IsCompatible

Mathlib.CategoryTheory.Sites.CoversTop

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible

Lean4

/-- `x : FamilyOfElementsOnObjects F Y` is compatible if for any object `Z` such that
there exists a morphism `f : Z → Y i`, then the pullback of `x i` by `f` is independent
of `f` and `i`. -/
def IsCompatible (x : FamilyOfElementsOnObjects F Y) : Prop :=
  ∀ (Z : C) (i j : I) (f : Z ⟶ Y i) (g : Z ⟶ Y j), F.map f.op (x i) = F.map g.op (x j)

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

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

Разделы

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

Аффилиация

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