Structures · Category theory
CategoryTheory.FinitaryExtensive
A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
- Defined in
- Mathlib.CategoryTheory.Extensive
- Shape
- One type argument · adds hasFiniteCoproducts, hasPullbacksOfInclusions, van_kampen'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.FinitaryExtensive is also a
Concrete types that are instances5
- CategoryTheory.Functor
- AlgebraicGeometry.Scheme
- TopCat
- CategoryTheory.Sheaf
- CompHausLike
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- CategoryTheory.Presheaf.coherentExtensiveEquivalence
- CategoryTheory.FinitaryExtensive.vanKampen
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
- CategoryTheory.FinitaryExtensive.van_kampen'
- CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts
- CategoryTheory.coherentTopology.isLocallySurjective_iff
- CategoryTheory.finitaryExtensive_of_preserves_and_reflects
- CategoryTheory.FinitaryExtensive.isPullback_initial_to
- CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit
- CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι
- CategoryTheory.extensiveTopology.isLocallySurjective_iff
- CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
- CategoryTheory.coherentTopology.epi_π_app_zero_of_epi
- CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map
- CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom
- CategoryTheory.coherentTopology.equivalence'
- CategoryTheory.finitaryExtensive_of_reflective
- CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify
- CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism
- CategoryTheory.finitaryExtensive_functor
- CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
- CategoryTheory.instCoproductsOfShapeDisjointOfFinitaryExtensiveOfFinite
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app
- CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits
- CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits
- CategoryTheory.isSheaf_pointwiseColimit
- CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive
- CategoryTheory.FinitaryExtensive.hasFiniteCoproducts
- CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app
- CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology
- CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp
- CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app
- CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit
- CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim
- CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective
- CategoryTheory.instMonoCoprodOfFinitaryExtensive
- CategoryTheory.instMonoι
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app
- CategoryTheory.FinitaryExtensive.hasPullbacksOfInclusions
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom
- CategoryTheory.FinitaryExtensive.mono_ι
- CategoryTheory.instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology