Structures · Category theory
CategoryTheory.Limits.HasFiniteCoproducts
A category has finite coproducts if there exists a colimit for every diagram
with shape Discrete J, where we have [Fintype J].
We require this condition only for J = Fin n in the definition, then deduce a version for any
J : Type* as a corollary of this definition.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Concrete types that are instances10
- CategoryTheory.Functor
- CategoryTheory.Over
- Action
- AlgebraicGeometry.Scheme
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.Sheaf
- CompHausLike
- CategoryTheory.MorphismProperty.Over
- CategoryTheory.MorphismProperty.CostructuredArrow
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by155
- AlgebraicTopology.DoldKan.Γ₀.splitting
- AlgebraicTopology.DoldKan.Γ₀.obj
- AlgebraicTopology.DoldKan.Γ₂
- AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂
- AlgebraicTopology.DoldKan.Γ₀
- CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj
- AlgebraicTopology.DoldKan.N₁Γ₀
- AlgebraicTopology.DoldKan.Γ₀.Obj.map
- CategoryTheory.Preadditive.DoldKan.equivalence
- CategoryTheory.Idempotents.DoldKan.Γ
- CategoryTheory.Idempotents.DoldKan.N
- AlgebraicTopology.DoldKan.N₂Γ₂
- AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
- CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone
- AlgebraicTopology.DoldKan.Γ₀'
- AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso
- AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso
- AlgebraicTopology.DoldKan.Γ₀NondegComplexIso
- AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
- CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone
- CategoryTheory.Idempotents.DoldKan.equivalence
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand
- AlgebraicTopology.DoldKan.Γ₂N₂
- CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset
- CategoryTheory.Idempotents.DoldKan.isoN₁
- CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀
- CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered
- CategoryTheory.Idempotents.DoldKan.η
- AlgebraicTopology.DoldKan.N₁Γ₀_app
- AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
- AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self
- CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
- CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology
- CategoryTheory.Idempotents.DoldKan.isoΓ₀
- AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id
- AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc
- CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels
- CategoryTheory.NormalEpiCategory.mono_of_zero_kernel
- AlgebraicTopology.DoldKan.Γ₂N₁
- AlgebraicTopology.DoldKan.Γ₀.map
- CategoryTheory.finitaryExtensive_of_preserves_and_reflects
- CategoryTheory.preserves_fin_of_preserves_binary_and_initial
- AlgebraicTopology.DoldKan.N₁Γ₀_hom_app
- CategoryTheory.Idempotents.DoldKan.hη
- AlgebraicTopology.DoldKan.identity_N₂_objectwise
- AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f
- AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app
- CategoryTheory.Preadditive.DoldKan.Γ
- AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom
Ancestors0
No ancestors.