isLocallyInjective_iff_injective_of_separated

English

For a presheaf with separation, being locally injective is equivalent to having each component map injective.

Русский

Для предрассевы с отделением локальная инъективность эквивалентна тому, что каждый компонентный отображение инъективно.

LaTeX

$$$\\text{IsLocallyInjective } J \\varphi \\iff \\forall X,\\ Function.Injective (\\varphi.app X)$$$

Lean4

theorem isLocallyInjective_iff_injective_of_separated (hsep : Presieve.IsSeparated J (F₁ ⋙ forget D)) :
    IsLocallyInjective J φ ↔ ∀ (X : Cᵒᵖ), Function.Injective (φ.app X) :=
  by
  constructor
  · intro _ X x y h
    exact (hsep _ (equalizerSieve_mem J φ x y h)).ext (fun _ _ hf => hf)
  · apply isLocallyInjective_of_injective

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