English
The value of the constructed section at each Y_i equals the corresponding x_i.
Русский
Значение сконструированного раздела на каждом Y_i равно соответствующему x_i.
LaTeX
$$$\\forall i, (\\mathrm{section_}(hY,hF).1)(\\mathrm{op}(Y_i)) = x_i$$$
Lean4
theorem existsUnique_section (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : IsSheaf J F) :
∃! (s : F.sections), ∀ (i : I), s.1 (Opposite.op (Y i)) = x i :=
by
have H := (isSheaf_iff_isSheaf_of_type _ _).1 hF
apply existsUnique_of_exists_of_unique
· let s := fun (X : C) => (H _ (hY X)).amalgamate _ (hx.familyOfElements_isCompatible X)
have hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i) := fun {X} i f =>
by
have h := Presieve.IsSheafFor.valid_glue (H _ (hY X)) (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
simp only [op_id, F.map_id, types_id_apply] at h
exact h.trans (hx.familyOfElements_apply _ _ _)
have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (_ : W ⟶ Y i), F.map a.op (s X) = s W :=
by
intro W X a i b
rw [hs i b]
exact
(Presieve.IsSheafFor.valid_glue (H _ (hY X)) (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans
(familyOfElements_apply hx _ _ _)
refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩
rintro ⟨Y₁⟩ ⟨Y₂⟩ ⟨f : Y₂ ⟶ Y₁⟩
change F.map f.op (s Y₁) = s Y₂
apply (H.isSeparated _ (hY Y₂)).ext
rintro Z φ ⟨i, ⟨g⟩⟩
rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]
rfl
· intro y₁ y₂ hy₁ hy₂
exact hY.sections_ext ⟨F, hF⟩ (fun i => by rw [hy₁, hy₂])
