CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'
theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition' :
∀ {A : Type (u + 2)} [inst : CategoryTheory.Category.{u + 1, u + 2} A] (G : CategoryTheory.Functor A (Type (u + 1)))
[inst_1 : CategoryTheory.Limits.HasLimits A] [inst_2 : CategoryTheory.Limits.PreservesLimits G]
[inst_3 : G.ReflectsIsomorphisms] (F : CategoryTheory.Functor CompHausᵒᵖ A),
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology CompHaus) F ↔
Nonempty (CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)) ∧
CategoryTheory.regularTopology.EqualizerCondition (F.comp G)
This theorem states that for a given category 'A' and a functor 'G' from 'A' to the category of Types, assuming that 'A' has all limits and 'G' preserves these limits and reflects isomorphisms, for any functor 'F' from the opposite category of compact Hausdorff spaces to 'A', 'F' is a sheaf with respect to the coherent Grothendieck topology on compact Hausdorff spaces if and only if there exists a functor that not only preserves finite products when composed with 'F' and 'G' but also satisfies the equalizer condition when so composed. The equalizer condition here means that the composed functor takes kernel pairs of effective epimorphisms to equalizer diagrams.
More concisely: A functor F from the opposite category of compact Hausdorff spaces to a category A with all limits, preserving these limits and reflecting isomorphisms is a sheaf for the coherent Grothendieck topology if and only if there exists a functor H from A to Types such that F and G (where G is a functor from A to Types) preserve finite products and the composite F ∘ H takes kernel pairs of effective epimorphisms to equalizer diagrams.
|
CategoryTheory.isSheaf_coherent_iff_regular_and_extensive
theorem CategoryTheory.isSheaf_coherent_iff_regular_and_extensive :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D)
[inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryPreExtensive C],
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ∧
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
This theorem states that a presheaf `F` is a sheaf with respect to the coherent Grothendieck topology on a precoherent category `C` if and only if it is a sheaf with respect to both the extensive Grothendieck topology on a finitary pre-extensive category `C` and the regular Grothendieck topology on a preregular category `C`. Here, `C` is a category with contextually defined typings, `D` is another category, and `F` is a functor from the opposite category of `C` to `D`.
More concisely: A presheaf F is a sheaf with respect to the coherent Grothendieck topology on a precoherent category C if and only if it is both a sheaf with respect to the extensive Grothendieck topology on the finitary pre-extensive category C and the regular Grothendieck topology on the preregular category C.
|
CondensedSet.equalizerCondition
theorem CondensedSet.equalizerCondition :
∀ (X : CondensedSet), CategoryTheory.regularTopology.EqualizerCondition X.val
The theorem `CondensedSet.equalizerCondition` states that every condensed set satisfies the equalizer condition. In the context of category theory, this means that for every condensed set `X`, if we consider `X` as a contravariant functor, it maps kernel pairs of effective epimorphisms to equalizer diagrams. In other words, `X` preserves the structure of equalizers in the category. This is a property that is often considered in the study of certain kinds of topological spaces and sheaves.
More concisely: The theorem `CondensedSet.equalizerCondition` asserts that every condensed set is a contravariant functor preserving equalizers in the category of sets and effective epimorphisms.
|