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.

Equations
    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.

      Equations
        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.

          Equations
            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.instPreservesFiniteProductsOppositeVal {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.val
              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.

              Equations
                Instances For
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val {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).val = f.val
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso {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] :
                  coherentExtensiveEquivalence.counitIso = Iso.refl ({ obj := fun (F : Sheaf (extensiveTopology C) A) => { val := F.val, cond := โ‹ฏ }, map := fun {X Y : Sheaf (extensiveTopology C) A} (f : X โŸถ Y) => { val := f.val }, map_id := โ‹ฏ, map_comp := โ‹ฏ }.comp { obj := fun (F : Sheaf (coherentTopology C) A) => { val := F.val, cond := โ‹ฏ }, map := fun {X Y : Sheaf (coherentTopology C) A} (f : X โŸถ Y) => { val := f.val }, map_id := โ‹ฏ, map_comp := โ‹ฏ })
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso {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] :
                  coherentExtensiveEquivalence.unitIso = Iso.refl (Functor.id (Sheaf (coherentTopology C) A))
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val {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] (F : Sheaf (extensiveTopology C) A) :
                  (coherentExtensiveEquivalence.inverse.obj F).val = F.val
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val {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] (F : Sheaf (coherentTopology C) A) :
                  (coherentExtensiveEquivalence.functor.obj F).val = F.val
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val {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).val = f.val
                  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
                  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
                  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