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 Mathlib/Condensed/Equivalence.lean.

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

source
๐Ÿ“ coverage
instance CategoryTheory.coherentTopology.instIsCoverDense {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.EffectivelyEnough] [Precoherent D] :
F.IsCoverDense (coherentTopology D)
source
๐Ÿ“ coverage
theorem CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Precoherent D] (X : C) (S : Sieve X) :
(โˆƒ (ฮฑ : Type) (_ : Finite ฮฑ) (Y : ฮฑ โ†’ C) (ฯ€ : (a : ฮฑ) โ†’ Y a โŸถ X), EffectiveEpiFamily Y ฯ€ โˆง โˆ€ (a : ฮฑ), S.arrows (ฯ€ a)) โ†” S โˆˆ (F.inducedTopology (coherentTopology D)) X
source
๐Ÿ“ coverage
theorem CategoryTheory.coherentTopology.eq_induced {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Precoherent D] :
coherentTopology C = F.inducedTopology (coherentTopology D)
source
๐Ÿ“ coverage
instance CategoryTheory.coherentTopology.instIsDenseSubsite {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Precoherent D] :
Functor.IsDenseSubsite (coherentTopology C) (coherentTopology D) F
source
๐Ÿ“ coverage
theorem CategoryTheory.coherentTopology.coverPreserving {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Precoherent D] :
CoverPreserving (coherentTopology C) (coherentTopology D) F
source
๐Ÿ”ธ coverage
noncomputable def CategoryTheory.coherentTopology.equivalence {C : Type uโ‚} {D : Type uโ‚‚} [Category.{vโ‚, uโ‚} C] [Category.{vโ‚‚, uโ‚‚} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful] [Precoherent D] [F.EffectivelyEnough] (A : Type uโ‚ƒ) [Category.{vโ‚ƒ, uโ‚ƒ} A] [โˆ€ (X : Dแต’แต–), Limits.HasLimitsOfShape (StructuredArrow X F.op) A] :
Sheaf (coherentTopology C) A โ‰Œ Sheaf (coherentTopology D) A

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.

Instances For
    source
    ๐Ÿ”ธ coverage
    noncomputable def CategoryTheory.coherentTopology.equivalence' {C : Type uโ‚} {D : Type uโ‚‚} [Category.{vโ‚, uโ‚} C] [Category.{vโ‚‚, uโ‚‚} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [FinitaryExtensive D] [Preregular D] [FinitaryPreExtensive C] [Limits.PreservesFiniteCoproducts F] [F.EffectivelyEnough] (A : Type uโ‚ƒ) [Category.{vโ‚ƒ, uโ‚ƒ} A] [โˆ€ (X : Dแต’แต–), Limits.HasLimitsOfShape (StructuredArrow X F.op) A] :
    Sheaf (coherentTopology C) A โ‰Œ Sheaf (coherentTopology D) A

    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.

    Instances For
      source
      ๐Ÿ“ coverage
      instance CategoryTheory.regularTopology.instIsCoverDense {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.EffectivelyEnough] [Preregular D] :
      F.IsCoverDense (regularTopology D)
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Preregular D] (X : C) (S : Sieve X) :
      (โˆƒ (Y : C) (ฯ€ : Y โŸถ X), EffectiveEpi ฯ€ โˆง S.arrows ฯ€) โ†” S โˆˆ (F.inducedTopology (regularTopology D)) X
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.regularTopology.eq_induced {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Preregular D] :
      regularTopology C = F.inducedTopology (regularTopology D)
      source
      ๐Ÿ“ coverage
      instance CategoryTheory.regularTopology.instIsDenseSubsite {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Preregular D] :
      Functor.IsDenseSubsite (regularTopology C) (regularTopology D) F
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.regularTopology.coverPreserving {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [Preregular D] :
      CoverPreserving (regularTopology C) (regularTopology D) F
      source
      ๐Ÿ”ธ coverage
      noncomputable def CategoryTheory.regularTopology.equivalence {C : Type uโ‚} {D : Type uโ‚‚} [Category.{vโ‚, uโ‚} C] [Category.{vโ‚‚, uโ‚‚} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [Preregular D] [F.EffectivelyEnough] (A : Type uโ‚ƒ) [Category.{vโ‚ƒ, uโ‚ƒ} A] [โˆ€ (X : Dแต’แต–), Limits.HasLimitsOfShape (StructuredArrow X F.op) A] :
      Sheaf (regularTopology C) A โ‰Œ Sheaf (regularTopology D) A

      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.

      Instances For
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) [Preregular C] [FinitaryPreExtensive C] :
        IsSheaf (coherentTopology C) F โ†” IsSheaf (extensiveTopology C) F โˆง IsSheaf (regularTopology C) F
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) [Preregular C] [FinitaryExtensive C] [h : โˆ€ {Y X : C} (f : Y โŸถ X) [EffectiveEpi f], Limits.HasPullback f f] :
        IsSheaf (coherentTopology C) F โ†” Limits.PreservesFiniteProducts F โˆง regularTopology.EqualizerCondition F
        source
        ๐Ÿ“ coverage
        instance CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] (F : Sheaf (coherentTopology C) A) :
        Limits.PreservesFiniteProducts F.obj
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] :
        IsSheaf (coherentTopology C) F โ†” Limits.PreservesFiniteProducts F
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] :
        IsSheaf (coherentTopology C) F โ†” IsSheaf (extensiveTopology C) F
        source
        ๐Ÿ”ธ coverage
        def CategoryTheory.Presheaf.coherentExtensiveEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] :
        Sheaf (coherentTopology C) A โ‰Œ Sheaf (extensiveTopology C) A

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

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (coherentTopology C) A) (Xโœ : Cแต’แต–) :
          (coherentExtensiveEquivalence.unitIso.hom.app X).hom.app Xโœ = CategoryStruct.id (X.obj.obj Xโœ)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (coherentTopology C) A) (Xโœ : Cแต’แต–) :
          (coherentExtensiveEquivalence.unitIso.inv.app X).hom.app Xโœ = CategoryStruct.id (X.obj.obj Xโœ)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] {Xโœ Yโœ : Sheaf (extensiveTopology C) A} (f : Xโœ โŸถ Yโœ) :
          (coherentExtensiveEquivalence.inverse.map f).hom = f.hom
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (coherentTopology C) A) :
          (coherentExtensiveEquivalence.functor.obj X).obj = X.obj
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (extensiveTopology C) A) :
          (coherentExtensiveEquivalence.inverse.obj X).obj = X.obj
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (extensiveTopology C) A) (Xโœ : Cแต’แต–) :
          (coherentExtensiveEquivalence.counitIso.hom.app X).hom.app Xโœ = CategoryStruct.id (X.obj.obj Xโœ)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] {Xโœ Yโœ : Sheaf (coherentTopology C) A} (f : Xโœ โŸถ Yโœ) :
          (coherentExtensiveEquivalence.functor.map f).hom = f.hom
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] (X : Sheaf (extensiveTopology C) A) (Xโœ : Cแต’แต–) :
          (coherentExtensiveEquivalence.counitIso.inv.app X).hom.app Xโœ = CategoryStruct.id (X.obj.obj Xโœ)
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [h : โˆ€ {Y X : C} (f : Y โŸถ X) [EffectiveEpi f], Limits.HasPullback f f] [Limits.PreservesFiniteLimits s] (hF : IsSheaf (coherentTopology C) F) :
          IsSheaf (coherentTopology C) (F.comp s)
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [h : โˆ€ {Y X : C} (f : Y โŸถ X) [EffectiveEpi f], Limits.HasPullback f f] [Limits.ReflectsFiniteLimits s] (hF : IsSheaf (coherentTopology C) (F.comp s)) :
          IsSheaf (coherentTopology C) F
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] [Limits.PreservesFiniteProducts s] (hF : IsSheaf (coherentTopology C) F) :
          IsSheaf (coherentTopology C) (F.comp s)
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] (F : Functor Cแต’แต– A) {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] [Limits.ReflectsFiniteProducts s] (hF : IsSheaf (coherentTopology C) (F.comp s)) :
          IsSheaf (coherentTopology C) F
          source
          ๐Ÿ“ coverage
          instance CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [h : โˆ€ {Y X : C} (f : Y โŸถ X) [EffectiveEpi f], Limits.HasPullback f f] [Limits.PreservesFiniteLimits s] :
          (coherentTopology C).HasSheafCompose s
          source
          ๐Ÿ“ coverage
          instance CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts {C : Type u_1} [Category.{v_1, u_1} C] {A : Type uโ‚ƒ} [Category.{vโ‚ƒ, uโ‚ƒ} A] {B : Type uโ‚„} [Category.{vโ‚„, uโ‚„} B] (s : Functor A B) [Preregular C] [FinitaryExtensive C] [โˆ€ (X : C), Projective X] [Limits.PreservesFiniteProducts s] :
          (coherentTopology C).HasSheafCompose s