Documentation Verification Report

Basic

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

Statistics

MetricCount
DefinitionsfintypeHom, fintypeObj, discreteFintype, discreteHomFintype, finCategoryDiscreteOfFintype, finCategoryOpposite, finCategoryUlift, instFinCategoryOfFiniteOfIsThin
8
TheoremsinstFiniteDiscrete
1
Total9

CategoryTheory

Definitions

NameCategoryTheorems
discreteFintype 📖CompOp—
discreteHomFintype 📖CompOp—
finCategoryDiscreteOfFintype 📖CompOp
12 mathmath: JointlyReflectIsomorphisms.shortComplexQuasiIso_iff, Limits.CompleteLattice.finite_coproduct_eq_finset_sup, JointlyReflectIsomorphisms.quasiIso_iff, JointlyReflectIsomorphisms.quasiIsoAt_iff, JointlyReflectIsomorphisms.shortExact_iff, Over.preservesTerminalIso_pullback, Over.prodComparisonIso_pullback_inv_left_snd', Over.prodComparisonIso_pullback_inv_left_fst_fst, preservesHomology_preadditiveYonedaObj_of_injective, 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 mathmath: AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ
finCategoryUlift 📖CompOp—
instFinCategoryOfFiniteOfIsThin 📖CompOp—

Theorems

NameKindAssumesProvesValidatesDepends On
instFiniteDiscrete 📖mathematical—Finite
Discrete		—Finite.of_equiv

CategoryTheory.FinCategory

Definitions

NameCategoryTheorems
fintypeHom 📖CompOp—
fintypeObj 📖CompOp
11 mathmath: 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