Lean4
/-- Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf. -/
@[stacks 00Z9 "This is a special case of the Stacks entry, but following a different
proof (see the Stacks comments)."]
def finestTopologySingle (P : Cᵒᵖ ⥤ Type v) : GrothendieckTopology C
where
sieves X S := ∀ (Y) (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f : Presieve Y)
top_mem' X Y
f := by
rw [Sieve.pullback_top]
exact Presieve.isSheafFor_top_sieve P
pullback_stable' X Y S f hS Z
g := by
rw [← pullback_comp]
apply hS
transitive' X S hS R hR Z
g := by
-- This is the hard part of the construction, showing that the given set of sieves satisfies
-- the transitivity axiom.
refine isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
· intro Y f _
rw [← pullback_comp]
apply (hS _ _).isSeparatedFor
· intro Y f hf
have := hR hf _ (𝟙 _)
rw [pullback_id, pullback_comp] at this
apply this
