English
Given H, isSheafFor on S, and a condition h, then T isIsSheafFor P.
Русский
При условии H и isSheafFor на S и дополнительном условии, T является IsSheafFor P.
LaTeX
$$$T.IsSheafFor(P)$$$
Lean4
theorem isSheafFor_of_factorsThru {X : C} {S T : Presieve X} (P : Cᵒᵖ ⥤ Type*) (H : S.FactorsThru T)
(hS : S.IsSheafFor P)
(h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve Y), R.IsSeparatedFor P ∧ R.FactorsThruAlong S f) :
T.IsSheafFor P :=
by
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
choose W i e h1 h2 using H
refine ⟨?_, fun x hx => ?_⟩
· intro x y₁ y₂ h₁ h₂
refine hS.1.ext (fun Y g hg => ?_)
simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]
let y : S.FamilyOfElements P := fun Y g hg => P.map (i _).op (x (e hg) (h1 _))
have hy : y.Compatible := by
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op), ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op), ←
P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
apply hx
simp only [h2, h, Category.assoc]
let ⟨_, h2'⟩ := hS
obtain ⟨z, hz⟩ := h2' y hy
refine ⟨z, fun Y g hg => ?_⟩
obtain ⟨R, hR1, hR2⟩ := h hg
choose WW ii ee hh1 hh2 using hR2
refine hR1.ext (fun Q t ht => ?_)
rw [← types_comp_apply (P.map g.op) (P.map t.op), ← P.map_comp, ← op_comp, ← hh2 ht, op_comp, P.map_comp,
types_comp_apply, hz _ (hh1 _), ← types_comp_apply _ (P.map (ii ht).op), ← P.map_comp, ← op_comp]
apply hx
simp only [Category.assoc, h2, hh2]
