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_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.IsContinuous (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.coherentTopology.equivalence
{C : Type (u + 1)}
{D : Type (u + 1)}
[CategoryTheory.LargeCategory C]
[CategoryTheory.LargeCategory D]
(F : CategoryTheory.Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
[F.ReflectsFiniteEffectiveEpiFamilies]
[F.Full]
[F.Faithful]
[CategoryTheory.Precoherent D]
[F.EffectivelyEnough]
(A : Type u_3)
[CategoryTheory.Category.{u + 1, u_3} A]
[CategoryTheory.Limits.HasLimits 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 + 1)}
{D : Type (u + 1)}
[CategoryTheory.LargeCategory C]
[CategoryTheory.LargeCategory 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_3)
[CategoryTheory.Category.{u + 1, u_3} A]
[CategoryTheory.Limits.HasLimits 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_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.IsContinuous (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.regularTopology.equivalence
{C : Type (u + 1)}
{D : Type (u + 1)}
[CategoryTheory.LargeCategory C]
[CategoryTheory.LargeCategory D]
(F : CategoryTheory.Functor C D)
[F.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.Full]
[F.Faithful]
[CategoryTheory.Preregular D]
[F.EffectivelyEnough]
(A : Type u_3)
[CategoryTheory.Category.{u + 1, u_3} A]
[CategoryTheory.Limits.HasLimits 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.