English
If P is separated, then for any s: Meq (J.plusObj P) S there exists t: ToType((J.plusObj P).obj(op X)) with mk t = s.
Русский
Если P разделим, то для любого s: Meq (J.plusObj P) S существует t: ToType((J.plusObj P).obj(op X)) такой, что mk t = s.
LaTeX
$$$\\exists t:\\ ToType((J.plusObj P).obj(op X)),\\; Meq.mk S t = s$$$
Lean4
theorem exists_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) (S : J.Cover X) (s : Meq (J.plusObj P) S) : ∃ t : ToType ((J.plusObj P).obj (op X)), Meq.mk S t = s :=
by
have inj : ∀ X : C, Function.Injective ((J.toPlus P).app (op X)) := inj_of_sep _ hsep
choose T t ht using fun I =>
exists_rep
(s I)
-- Construct a large cover over which we will define a representative that will
-- provide the gluing of the given local sections.
let B : J.Cover X := S.bind T
choose Z e1 e2 he2 _ _ using fun I : B.Arrow => I.hf
let w : Meq P B := meqOfSep P hsep X S s T t ht
use mk w
ext I
dsimp [Meq.mk]
rw [ht, res_mk_eq_mk_pullback]
-- Use the separatedness of `P⁺` to prove that this is indeed a gluing of our
-- original local sections.
apply sep P (T I)
intro II
simp only [res_mk_eq_mk_pullback, eq_mk_iff_exists]
-- It suffices to prove equality for representatives over a
-- convenient sufficiently large cover...
use (J.pullback II.f).obj (T I)
let e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) :=
homOfLE
(by
intro Y f hf
apply Sieve.le_pullback_bind _ _ _ I.hf
· cases I
exact hf)
use e0, 𝟙 _
ext IV
let IA : B.Arrow := ⟨_, (IV.f ≫ II.f) ≫ I.f, ⟨I.Y, _, _, I.hf, Sieve.downward_closed _ II.hf _, rfl⟩⟩
let IB : S.Arrow := IA.fromMiddle
let IC : (T IB).Arrow := IA.toMiddle
let ID : (T I).Arrow := ⟨IV.Y, IV.f ≫ II.f, Sieve.downward_closed (T I).1 II.hf IV.f⟩
change t IB IC = t I ID
apply inj IV.Y
rw [toPlus_apply (T I) (t I) ID]
erw [toPlus_apply (T IB) (t IB) IC]
rw [← ht, ← ht]
-- Conclude by constructing the relation showing equality...
let IR : S.Relation := { fst.hf := IB.hf, snd.hf := I.hf, r.w := IA.middle_spec, .. }
exact s.condition IR
