coherentExtensiveEquivalence — Mathlib

Lean4

/-- The categories of coherent sheaves and extensive sheaves on `C` are equivalent if `C` is
preregular, finitary extensive, and every object is projective.
-/
@[simps]
def coherentExtensiveEquivalence [Preregular C] [FinitaryExtensive C] [∀ (X : C), Projective X] :
    Sheaf (coherentTopology C) A ≌ Sheaf (extensiveTopology C) A
    where
  functor :=
    { obj := fun F ↦ ⟨F.val, (isSheaf_iff_extensiveSheaf_of_projective F.val).mp F.cond⟩
      map := fun f ↦ ⟨f.val⟩ }
  inverse :=
    { obj := fun F ↦ ⟨F.val, (isSheaf_iff_extensiveSheaf_of_projective F.val).mpr F.cond⟩
      map := fun f ↦ ⟨f.val⟩ }
  unitIso := Iso.refl _
  counitIso := Iso.refl _

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