Documentation

Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Categories of coherent sheaves #

Given a fully faithful functor F : C ⥤ D into a precoherent category, which preserves and reflects finite effective epi families, and satisfies the property F.EffectivelyEnough (meaning that to every object in C there is an effective epi from an object in the image of F), the categories of coherent sheaves on C and D are equivalent (see CategoryTheory.coherentTopology.equivalence).

The main application of this equivalence is the characterisation of condensed sets as coherent sheaves on either CompHaus, Profinite or Stonean. See the file Condensed/Equivalence.lean

We give the corresponding result for the regular topology as well (see CategoryTheory.regularTopology.equivalence).

theorem CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Precoherent D] (X : C) (S : CategoryTheory.Sieve X) :
(∃ (α : Type) (_ : Finite α) (Y : αC) (π : (a : α) → Y a X), CategoryTheory.EffectiveEpiFamily Y π ∀ (a : α), S.arrows (π a)) S (F.inducedTopology (CategoryTheory.coherentTopology D)) X
theorem CategoryTheory.coherentTopology.eq_induced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Precoherent D] :
instance CategoryTheory.coherentTopology.instIsDenseSubsite {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Precoherent D] :
Equations
  • =
theorem CategoryTheory.coherentTopology.coverPreserving {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Precoherent D] :

The equivalence from coherent sheaves on C to coherent sheaves on D, given a fully faithful functor F : C ⥤ D to a precoherent category, which preserves and reflects effective epimorphic families, and satisfies F.EffectivelyEnough.

Equations
Instances For

    The equivalence from coherent sheaves on C to coherent sheaves on D, given a fully faithful functor F : C ⥤ D to an extensive preregular category, which preserves and reflects effective epimorphisms and satisfies F.EffectivelyEnough.

    Equations
    Instances For
      theorem CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Preregular D] (X : C) (S : CategoryTheory.Sieve X) :
      (∃ (Y : C) (π : Y X), CategoryTheory.EffectiveEpi π S.arrows π) S (F.inducedTopology (CategoryTheory.regularTopology D)) X
      theorem CategoryTheory.regularTopology.eq_induced {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [CategoryTheory.Preregular D] :
      Equations
      • =

      The equivalence from regular sheaves on C to regular sheaves on D, given a fully faithful functor F : C ⥤ D to a preregular category, which preserves and reflects effective epimorphisms and satisfies F.EffectivelyEnough.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] :
        CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso = CategoryTheory.Iso.refl ({ obj := fun (F : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) => { val := F.val, cond := }, map := fun {X Y : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A} (f : X Y) => { val := f.val }, map_id := , map_comp := }.comp { obj := fun (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) => { val := F.val, cond := }, map := fun {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X Y) => { val := f.val }, map_id := , map_comp := })

        The categories of coherent sheaves and extensive sheaves on C are equivalent if C is preregular, finitary extensive, and every object is projective.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For