LiftToFinset

📁 Source: Mathlib/CategoryTheory/Preadditive/LiftToFinset.lean

Statistics

Metric	Count
Definitions	0
Theorems finiteSubcoproductsCocone_ι_app_eq_sum, finiteSubproductsCocone_π_app_eq_sum	2
Total	2

CategoryTheory.Limits.CoproductsFromFiniteFiltered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteSubcoproductsCocone_ι_app_eq_sum 📖	mathematical	—	CategoryTheory.NatTrans.app Finset CategoryTheory.Discrete Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder liftToFinsetObj CategoryTheory.Discrete.functor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt finiteSubcoproductsCocone CategoryTheory.Limits.Cocone.ι Finset.sum Finset.instMembership Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj CategoryTheory.Discrete.as AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.attach CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Sigma.π CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.instDecidableEqDiscrete CategoryTheory.Limits.Sigma.ι	—	CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Preadditive.comp_sum Finset.sum_eq_single CategoryTheory.Limits.Sigma.ι_π_of_ne_assoc CategoryTheory.Limits.zero_comp CategoryTheory.Limits.Sigma.ι_π_eq_id_assoc instIsEmptyFalse

CategoryTheory.Limits.ProductsFromFiniteCofiltered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteSubproductsCocone_π_app_eq_sum 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Finset CategoryTheory.Discrete CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt liftToFinsetObj CategoryTheory.Discrete.functor finiteSubproductsCone CategoryTheory.Limits.Cone.π Finset.sum Finset.instMembership Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj CategoryTheory.Discrete.as CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype Finset.Subtype.fintype AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.attach CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Pi.π CategoryTheory.Limits.Pi.ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.instDecidableEqDiscrete	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Preadditive.sum_comp Finset.sum_congr CategoryTheory.Category.assoc Finset.sum_eq_single CategoryTheory.Limits.Pi.ι_π_of_ne CategoryTheory.Limits.comp_zero CategoryTheory.Limits.Pi.ι_π_eq_id CategoryTheory.Category.comp_id instIsEmptyFalse

---

← Back to Index