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

source
instance CategoryTheory.coherentTopology.instIsCoverDense {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) [F.EffectivelyEnough] [Precoherent D] :
F.IsCoverDense (coherentTopology D)
source
theorem CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
theorem CategoryTheory.coherentTopology.eq_induced {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
instance CategoryTheory.coherentTopology.instIsDenseSubsite {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
theorem CategoryTheory.coherentTopology.coverPreserving {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
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
    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
      instance CategoryTheory.regularTopology.instIsCoverDense {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) [F.EffectivelyEnough] [Preregular D] :
      F.IsCoverDense (regularTopology D)
      source
      theorem CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
      theorem CategoryTheory.regularTopology.eq_induced {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
      instance CategoryTheory.regularTopology.instIsDenseSubsite {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
      theorem CategoryTheory.regularTopology.coverPreserving {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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
      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
        theorem CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive {C : Type u_1} [Category.{u_3, 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
        theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition {C : Type u_1} [Category.{u_3, 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
        instance CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal {C : Type u_1} [Category.{u_3, u_1} C] {A : Type u₃} [Category.{v₃, u₃} A] [Preregular C] [FinitaryExtensive C] (F : Sheaf (coherentTopology C) A) :
        Limits.PreservesFiniteProducts F.val
        source
        theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective {C : Type u_1} [Category.{u_3, 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
        theorem CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective {C : Type u_1} [Category.{u_3, 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
        def CategoryTheory.Presheaf.coherentExtensiveEquivalence {C : Type u_1} [Category.{u_3, 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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val {C : Type u_1} [Category.{u_3, 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
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso {C : Type u_1} [Category.{u_3, 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
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso {C : Type u_1} [Category.{u_3, 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
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val {C : Type u_1} [Category.{u_3, 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
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val {C : Type u_1} [Category.{u_3, 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
          @[simp]
          theorem CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val {C : Type u_1} [Category.{u_3, 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
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp {C : Type u_1} [Category.{u_3, 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.{u_3, 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
          theorem CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp {C : Type u_1} [Category.{u_3, 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.{u_3, 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
          instance CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits {C : Type u_1} [Category.{u_3, 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
          instance CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts {C : Type u_1} [Category.{u_3, 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