English
A simplified version of exists_of_sep emphasizing the existence of a representative for separated P.
Русский
Упрощенная версия exists_of_sep, подчеркивающая существование представителя для раздельного P.
LaTeX
$$$\\exists t:\\ ToType((J.plusObj P).obj(op X)), Meq.mk S t = s$$$
Lean4
/-- If `P` is separated, then `P⁺` is a sheaf. -/
theorem isSheaf_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) :
Presheaf.IsSheaf J (J.plusObj P) :=
by
rw [Presheaf.isSheaf_iff_multiequalizer]
intro X S
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (forget D) ?_
rw [isIso_iff_bijective]
constructor
· intro x y h
apply sep P S _ _
intro I
apply_fun Meq.equiv _ _ at h
apply_fun fun e => e I at h
dsimp only [ConcreteCategory.forget_map_eq_coe] at h
convert h <;> erw [Meq.equiv_apply] <;> rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι] <;> rfl
· rintro (x : ToType (multiequalizer (S.index _)))
obtain ⟨t, ht⟩ := exists_of_sep P hsep X S (Meq.equiv _ _ x)
use t
apply (Meq.equiv (D := D) _ _).injective
rw [← ht]
ext i
dsimp
rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
rfl
