ofSheafForgetStonean — Mathlib

Lean4
/-- The condensed object associated to a presheaf on `Stonean` whose postcomposition with the
forgetful functor preserves finite products.
-/
noncomputable def ofSheafForgetStonean [∀ X, HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A] [HasForget A]
    [ReflectsFiniteProducts (CategoryTheory.forget A)] (F : Stonean.{u}ᵒᵖ ⥤ A)
    [PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)] : Condensed A :=
  StoneanCompHaus.equivalence A |>.functor.obj
    { val := F
      cond := by
        apply isSheaf_coherent_of_projective_of_comp F (CategoryTheory.forget A)
        rw [isSheaf_iff_preservesFiniteProducts_of_projective]
        exact ⟨fun _ ↦ inferInstance⟩ }
Похожие утверждения