English
Let K be a coverage on C and P a Type-valued presheaf on C. A presheaf is a sheaf for the coverage K if and only if, for every object X and every presieve R on X with R ∈ K X, P is a sheaf for R.
Русский
Пусть K — покрытие на C, а P — прообразная функция значений типа на C. Поровняльный пеллер является sheaf для покрытия K тогда и только тогда, для каждого объекта X и каждого предсемени R на X с R ∈ K X, P является sheaf для R.
LaTeX
$$$\\mathrm{IsSheaf}_{K^{\\mathrm{Gro}}}(P) \\iff \\forall X, \\forall R \\in K(X),\\ \\mathrm{IsSheafFor}(P,R)$$$
Lean4
/-- The main theorem of this file: Given a coverage `K` on `C`,
a `Type*`-valued presheaf on `C` is a sheaf for `K` if and only if it is a sheaf for
the associated Grothendieck topology.
-/
theorem isSheaf_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
Presieve.IsSheaf K.toGrothendieck P ↔ (∀ {X : C} (R : Presieve X), R ∈ K X → Presieve.IsSheafFor P R) :=
by
constructor
· intro H X R hR
rw [Presieve.isSheafFor_iff_generate]
apply H _ <| Saturate.of _ _ hR
· intro H X S hS
suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by simpa using this (f := 𝟙 _)
induction hS with
| of X S hS =>
intro Y f
obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
apply Presieve.isSheafFor_of_factorsThru (S := T)
· intro Z g hg
obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
· apply H; assumption
· intro Z g _
obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
exact ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
| top => intros; simpa using Presieve.isSheafFor_top_sieve _
| transitive X R S _ _ H1 H2 =>
intro Y f
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
choose H1 H1' using H1
choose H2 H2' using H2
refine ⟨?_, fun x hx => ?_⟩
· intro x t₁ t₂ h₁ h₂
refine (H1 f).ext (fun Z g hg => ?_)
refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
simp only [← types_comp_apply]
rw [← P.map_comp, ← op_comp, h₁, h₂]
simpa only [Sieve.pullback_apply, Category.assoc] using hgg
let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible :=
by
intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
rw [hx]
rw [reassoc_of% h]
choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) => H2' hg (𝟙 _) (y g) (hy g)
let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
have hq : q.Compatible := by
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
apply (H2 h₁ g₁).ext
intro ZZ gg hgg
simp only [← types_comp_apply]
rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
· dsimp [y]; congr 1; simp only [Category.assoc, h]
· simpa [reassoc_of% h] using hgg
· simpa using hgg
obtain ⟨t, ht⟩ := H1' f q hq
refine ⟨t, fun Z g hg => ?_⟩
refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
on_goal 2 => simpa using hgg
refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
on_goal 2 => simpa using hggg
refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
apply hx
simp
