preregular_isSheaf_iff — Mathlib

English

The regular sheaf condition can be checked after precomposing with an equivalence.

Русский

Условие шейфовости по регулярной топологии можно проверить после предварительного сопряжения через эквивалентность.

LaTeX

$$$\text{IsSheaf}(\mathrm{regularTopology}\ C, F) \iff \text{IsSheaf}(\mathrm{regularTopology}\ D, e^{-1}\!\circ\! F)$$$

Lean4

/-- The regular sheaf condition can be checked after precomposing with the equivalence.
-/
theorem preregular_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) :
    haveI := e.preregular
    IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F) :=
  by
  refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩
  rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
  · exact (e.sheafCongrPreregular A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.cond
  · exact Functor.isoWhiskerRight e.op.unitIso F

Похожие утверждения