Structures · Category theory
CategoryTheory.FinitaryPreExtensive
A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.
- Defined in
- Mathlib.CategoryTheory.Extensive
- Shape
- One type argument · adds hasFiniteCoproducts, hasPullbacksOfInclusions, universal'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.FinitaryPreExtensive is also a
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CategoryTheory.extensiveTopology
- CategoryTheory.extensiveCoverage
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
- CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
- CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive
- CategoryTheory.extensive_regular_generate_coherent
- CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
- CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan
- CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff
- CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff
- CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types
- CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin
- CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
- CategoryTheory.FinitaryPreExtensive.universal'
- CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts
- CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst
- CategoryTheory.extensiveCoverage.congr_simp
- CategoryTheory.coherentTopology.equivalence'
- CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc
- CategoryTheory.extensiveTopology.isSheaf_yoneda_obj
- CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis
- CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive
- CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
- CategoryTheory.extensiveTopology.subcanonical
- CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions
- CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis
- CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map
- CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts
- CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct
- CategoryTheory.instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology
- CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily
- CategoryTheory.instHasPairwisePullbacksOfExtensive
- CategoryTheory.FinitaryPreExtensive.hasPullbacksOfInclusions
- CategoryTheory.instExtensiveOfArrowsι