yoneda_obj_isGeneratedBy — Mathlib

English

The Yoneda image of an object X is generated by the identity on X via a canonical generating family.

Русский

Образ Йонеда объекта X порождается идентичностью на X через каноническую порождающую семейство.

LaTeX

$$$\\mathrm{PresheafIsGeneratedBy}(\\mathrm{yoneda.obj}\, X, \\lambda _: \\mathbf{1}_X)$$$

Lean4

theorem yoneda_obj_isGeneratedBy (X : C) : PresheafIsGeneratedBy (yoneda.obj X) (fun (_ : Unit) ↦ 𝟙 X) :=
  by
  simp only [Subpresheaf.isGeneratedBy_iff]
  ext U u
  simp only [yoneda_obj_obj, Subpresheaf.iSup_obj, Set.mem_iUnion, exists_const, Subpresheaf.top_obj, Set.top_eq_univ,
    Set.mem_univ, iff_true]
  exact ⟨u.op, by simp⟩

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