English
For x: Meq P S and y: Meq P T, mk x = mk y is equivalent to the existence of W with arrows to S and T such that x.refine h1 = y.refine h2.
Русский
Для x: Meq P S и y: Meq P T, mk x = mk y эквивалентно существованию W с стрелками в S и T и равенством x.refine h1 = y.refine h2.
LaTeX
$$$mk x = mk y \\iff \\exists W:\\; J.Cover X,\\; h1: W\\to S, h2: W\\to T,\\; x.refine h1 = y.refine h2$$$
Lean4
/-- An auxiliary definition to be used in the proof of `exists_of_sep` below.
Given a compatible family of local sections for `P⁺`, and representatives of said sections,
construct a compatible family of local sections of `P` over the combination of the covers
associated to the representatives.
The separatedness condition is used to prove compatibility among these local sections of `P`. -/
def meqOfSep (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 : ∀ I : S.Arrow, J.Cover I.Y) (t : ∀ I : S.Arrow, Meq P (T I))
(ht : ∀ I : S.Arrow, s I = mk (t I)) : Meq P (S.bind T)
where
val I := t I.fromMiddle I.toMiddle
property := by
intro II
apply inj_of_sep P hsep
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, (J.toPlus P).naturality, (J.toPlus P).naturality,
ConcreteCategory.comp_apply, ConcreteCategory.comp_apply]
erw [toPlus_apply (T II.fst.fromMiddle) (t II.fst.fromMiddle) II.fst.toMiddle,
toPlus_apply (T II.snd.fromMiddle) (t II.snd.fromMiddle) II.snd.toMiddle]
rw [← ht, ← ht]
erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply];
rw [← (J.plusObj P).map_comp, ← (J.plusObj P).map_comp, ← op_comp, ← op_comp]
exact
s.condition
{ fst.hf := II.fst.from_middle_condition
snd.hf := II.snd.from_middle_condition
r.g₁ := II.r.g₁ ≫ II.fst.toMiddleHom
r.g₂ := II.r.g₂ ≫ II.snd.toMiddleHom
r.w := by simpa only [Category.assoc, Cover.Arrow.middle_spec] using II.r.w .. }
