exists_rep — Mathlib

English

Let X be an object of C and P a presheaf on C viewed through Opposite. For any element x of the object associated to (J.plusObj P) at op X, there exists a cover S of X and a representative y of P restricted to S such that x equals the image mk y.

Русский

Пусть X — объект в C, а P — префеш на C. Для любого элемента x объекта, связанного с (J.plusObj P).obj (op X), существует покрытие S X и представитель y в P, ограниченный на S, такой что x = mk y.

LaTeX

$$$\\exists S\\in J.Cover X\\;\\exists y\\in Meq\\ P\\ S\\; x = mk\\; y$$$

Lean4

theorem exists_rep {X : C} {P : Cᵒᵖ ⥤ D} (x : ToType ((J.plusObj P).obj (op X))) :
    ∃ (S : J.Cover X) (y : Meq P S), x = mk y :=
  by
  obtain ⟨S, y, h⟩ := Concrete.colimit_exists_rep (J.diagram P X) x
  use S.unop, Meq.equiv _ _ y
  rw [← h]
  dsimp [mk]
  simp

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