over_forget_locallyCoverDense — Mathlib

English

For every object X, the forgetful functor from Over X is locally cover-dense with respect to J, i.e., it satisfies the local-density condition in the overcategory context.

Русский

Для каждого X непрямой канонический функтор из Over X удовлетворяет локальную плотность по J.

LaTeX

$$$\\forall X,\\ (Over.\\mathrm{forget } X).\\mathrm{LocallyCoverDense } J$$$

Lean4

instance over_forget_locallyCoverDense (X : C) : (Over.forget X).LocallyCoverDense J where
  functorPushforward_functorPullback_mem Y
    T := by
    convert T.property
    ext Z f
    constructor
    · rintro ⟨_, _, g', hg, rfl⟩
      exact T.val.downward_closed hg g'
    · intro hf
      exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩

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