precoherent_isSheaf_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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