inj_of_sep — Mathlib

English

Under a separation hypothesis for P, for every X the map from P.obj(op X) into (J.toPlus P).obj(op X) is injective.

Русский

При условии разделимости P, для каждого X отображение P(X) в (J.toPlus P)(X) инъективно.

LaTeX

$$$\\forall X:\\;\\text{Obj}(C),\\; \\text{Injective}((J.toPlus P).app(op X))$$$

Lean4

theorem inj_of_sep (P : Cᵒᵖ ⥤ D)
    (hsep :
      ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))), (∀ I : S.Arrow, P.map I.f.op x = P.map I.f.op y) → x = y)
    (X : C) : Function.Injective ((J.toPlus P).app (op X)) :=
  by
  intro x y h
  simp only [toPlus_eq_mk] at h
  rw [eq_mk_iff_exists] at h
  obtain ⟨W, h1, h2, hh⟩ := h
  apply hsep X W
  intro I
  apply_fun fun e => e I at hh
  exact hh

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