Basic

📁 Source: Mathlib/CategoryTheory/FinCategory/Basic.lean

Statistics

Metric	Count
Definitions fintypeHom, fintypeObj, discreteFintype, discreteHomFintype, finCategoryDiscreteOfFintype, finCategoryOpposite, finCategoryUlift, instFinCategoryOfFiniteOfIsThin	8
Theorems instFiniteDiscrete	1
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
discreteFintype 📖	CompOp	—
discreteHomFintype 📖	CompOp	—
finCategoryDiscreteOfFintype 📖	CompOp	7 math math: Limits.CompleteLattice.finite_coproduct_eq_finset_sup, Over.preservesTerminalIso_pullback, Over.prodComparisonIso_pullback_inv_left_snd', Over.prodComparisonIso_pullback_inv_left_fst_fst, Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', Over.prodComparisonIso_pullback_inv_left_fst_snd', Limits.CompleteLattice.finite_product_eq_finset_inf
finCategoryOpposite 📖	CompOp	1 math math: AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ
finCategoryUlift 📖	CompOp	—
instFinCategoryOfFiniteOfIsThin 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteDiscrete 📖	mathematical	—	Finite Discrete	—	Finite.of_equiv

CategoryTheory.FinCategory

Definitions

Name	Category	Theorems
fintypeHom 📖	CompOp	—
fintypeObj 📖	CompOp	11 math math: CategoryTheory.Limits.colimitLimitToLimitColimit_isIso, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ι_app, CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf, CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_π_app, CategoryTheory.Limits.colimitLimitToLimitColimit_surjective

---

← Back to Index