ran_isSheaf_of_isCocontinuous — Mathlib

English

Another variant of hom-ext style lemma in RanIsSheaf etc.

Русский

Ещё одна вариация леммы hom-ext в RanIsSheaf и т.д.

LaTeX

$$$\\dots$$$

Lean4

/-- If `G` is cocontinuous, then `G.op.ran` pushes sheaves to sheaves.

This is SGA 4 III 2.2. -/
@[stacks 00XK "Alternative reference. There, results are obtained under the additional assumption
      that `C` and `D` have pullbacks."]
theorem ran_isSheaf_of_isCocontinuous (ℱ : Sheaf J A) : Presheaf.IsSheaf K (G.op.ran.obj ℱ.val) :=
  by
  rw [Presheaf.isSheaf_iff_multifork]
  intro X S
  exact ⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2 (G.op.isPointwiseRightKanExtensionRanCounit ℱ.val) S⟩

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