English
If r is locally constant with finite fiber, then the explicit finite coproduct on the fiber exists (HasExplicitFiniteCoproducts).
Русский
Если локально константное отображение r имеет конечную фибер-фиду, то существует явное конечное coproduct-объединение фибры.
LaTeX
$$$[HasExplicitFiniteCoproducts\, P] \Rightarrow \text{HasExplicitFiniteCoproduct}(\mathrm{LocallyConstant.fiber}\, r)$$$
Lean4
/-- To check equality of two elements of `X(S)`, it suffices to check equality after composing with
each `X(S) → X(Sᵢ)`.
-/
theorem presheaf_ext (X : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w) [PreservesFiniteProducts X] (x y : X.obj ⟨S⟩)
[HasExplicitFiniteCoproducts.{u} P] (h : ∀ (a : Fiber f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y) :
x = y := by
apply injective_of_mono (X.mapIso (sigmaIso f).op).hom
apply injective_of_mono (sigmaComparison X (fun a ↦ (fiber f a).1))
ext a
specialize h a
rw [← sigmaComparison_comp_sigmaIso] at h
exact h
