English
Infimums commute with the toPretopology operation and with the image under toPretopology of Grothendieck topologies.
Русский
И Inf и toPretopology совместимы с образом Grothendieck топологий и их изображениями.
LaTeX
$$$sInf T toPretopology = sInf(\\mathrm{image}(\\mathrm{GrothendieckTopology}.toPretopology, T))$$$
Lean4
/-- Given sieve `S` and presheaf `P : Cᵒᵖ ⥤ A`, their natural associated cone is a limit cone
iff `Hom (E, P -)` is a sheaf of types for the sieve `S` and all `E : A`. -/
theorem isLimit_iff_isSheafFor :
Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ E : Aᵒᵖ, IsSheafFor (P ⋙ coyoneda.obj E) S.arrows :=
by
dsimp [IsSheafFor]; simp_rw [compatible_iff_sieveCompatible]
rw [((Cone.isLimitEquivIsTerminal _).trans (isTerminalEquivUnique _ _)).nonempty_congr]
rw [Classical.nonempty_pi]; constructor
· intro hu E x hx
specialize hu hx.cone
rw [(homEquivAmalgamation hx).uniqueCongr.nonempty_congr] at hu
exact (unique_subtype_iff_existsUnique _).1 hu
· rintro h ⟨E, π⟩
let eqv := conesEquivSieveCompatibleFamily P S (op E)
rw [← eqv.left_inv π]
erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]
rw [unique_subtype_iff_existsUnique]
exact h _ _ (eqv π).2
