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 corresonding result for the regular topology as well (see
CategoryTheory.regularTopology.equivalence).
instance
CategoryTheory.coherentTopology.instIsCoverDense
{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.EffectivelyEnough]
[CategoryTheory.Precoherent D]
:
F.IsCoverDense (CategoryTheory.coherentTopology D)
Equations
- ⋯ = ⋯
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.inducedTopologyOfIsCoverDense (CategoryTheory.coherentTopology D)).sieves 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]
:
CategoryTheory.coherentTopology C = F.inducedTopologyOfIsCoverDense (CategoryTheory.coherentTopology D)
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]
:
instance
CategoryTheory.coherentTopology.coverLifting
{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]
:
F.IsCocontinuous (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D)
Equations
- ⋯ = ⋯
instance
CategoryTheory.coherentTopology.isContinuous
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
[F.ReflectsFiniteEffectiveEpiFamilies]
[F.Full]
[F.Faithful]
[F.EffectivelyEnough]
[CategoryTheory.Precoherent D]
:
F.IsContinuous (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.coherentTopology.equivalence
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
[F.ReflectsFiniteEffectiveEpiFamilies]
[F.Full]
[F.Faithful]
[CategoryTheory.Precoherent D]
[F.EffectivelyEnough]
(A : Type u₃)
[CategoryTheory.Category.{v₃, u₃} A]
[∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op) 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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.coherentTopology.equivalence'
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.Full]
[F.Faithful]
[CategoryTheory.FinitaryExtensive D]
[CategoryTheory.Preregular D]
[CategoryTheory.FinitaryPreExtensive C]
[CategoryTheory.Limits.PreservesFiniteCoproducts F]
[F.EffectivelyEnough]
(A : Type u₃)
[CategoryTheory.Category.{v₃, u₃} A]
[∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op) 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
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.regularTopology.instIsCoverDense
{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.EffectivelyEnough]
[CategoryTheory.Preregular D]
:
F.IsCoverDense (CategoryTheory.regularTopology D)
Equations
- ⋯ = ⋯
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.inducedTopologyOfIsCoverDense (CategoryTheory.regularTopology D)).sieves 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]
:
CategoryTheory.regularTopology C = F.inducedTopologyOfIsCoverDense (CategoryTheory.regularTopology D)
theorem
CategoryTheory.regularTopology.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.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.Full]
[F.Faithful]
[F.EffectivelyEnough]
[CategoryTheory.Preregular D]
:
instance
CategoryTheory.regularTopology.coverLifting
{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]
:
F.IsCocontinuous (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D)
Equations
- ⋯ = ⋯
instance
CategoryTheory.regularTopology.isContinuous
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
[F.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.Full]
[F.Faithful]
[F.EffectivelyEnough]
[CategoryTheory.Preregular D]
:
F.IsContinuous (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.regularTopology.equivalence
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.Full]
[F.Faithful]
[CategoryTheory.Preregular D]
[F.EffectivelyEnough]
(A : Type u₃)
[CategoryTheory.Category.{v₃, u₃} A]
[∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op) 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryPreExtensive C]
:
theorem
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
:
noncomputable instance
CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal
{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]
(F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A)
:
Equations
theorem
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X]
:
theorem
CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X]
:
@[simp]
theorem
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val
{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]
(F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A)
:
(CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.obj F).val = F.val
@[simp]
theorem
CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso
{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.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A))
@[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 := ⋯ })
@[simp]
theorem
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val
{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]
(F : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A)
:
(CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.obj F).val = F.val
@[simp]
theorem
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val
{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]
:
∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y),
(CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.map f).val = f.val
@[simp]
theorem
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val
{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]
:
∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A} (f : X ⟶ Y),
(CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.map f).val = f.val
def
CategoryTheory.Presheaf.coherentExtensiveEquivalence
{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]
:
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
theorem
CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.Limits.PreservesFiniteLimits s]
(hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F)
:
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
theorem
CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.Limits.ReflectsFiniteLimits s]
(hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s))
:
theorem
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X]
[CategoryTheory.Limits.PreservesFiniteProducts s]
(hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F)
:
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
theorem
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
(F : CategoryTheory.Functor Cᵒᵖ A)
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X]
[CategoryTheory.Limits.ReflectsFiniteProducts s]
(hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s))
:
instance
CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.Limits.PreservesFiniteLimits s]
:
(CategoryTheory.coherentTopology C).HasSheafCompose s
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{A : Type u₃}
[CategoryTheory.Category.{v₃, u₃} A]
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(s : CategoryTheory.Functor A B)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X]
[CategoryTheory.Limits.PreservesFiniteProducts s]
:
(CategoryTheory.coherentTopology C).HasSheafCompose s
Equations
- ⋯ = ⋯