Structures · Category theory
CategoryTheory.FinCategory
A category with a Fintype of objects, and a Fintype for each morphism space.
- Defined in
- Mathlib.CategoryTheory.FinCategory.Basic
- Shape
- One type argument · adds fintypeObj, fintypeHom
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every CategoryTheory.FinCategory is also a
Provided automatically by
Concrete types that are instances14
- CategoryTheory.Discrete
- CategoryTheory.WithTerminal
- CategoryTheory.WithInitial
- CategoryTheory.Pairwise
- CategoryTheory.ULiftHom
- CategoryTheory.Bicone
- CategoryTheory.SingleObj
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.WidePullbackShape
- CategoryTheory.Limits.WidePushoutShape
- CategoryTheory.Limits.WalkingMultispan
- CategoryTheory.Limits.WalkingMulticospan
- CategoryTheory.FinCategory.AsType
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by98
- CategoryTheory.Limits.CompleteLattice.finiteLimitCone
- CategoryTheory.Limits.CompleteLattice.finiteColimitCocone
- CategoryTheory.FinCategory.equivAsType
- CategoryTheory.IsFiltered.cocone_nonempty
- CategoryTheory.IsCofiltered.cone
- CategoryTheory.PreservesFiniteLimitsOfFlat.lift
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux
- CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf
- CategoryTheory.FinCategory.objAsTypeToAsType
- CategoryTheory.FinCategory.asTypeToObjAsType
- CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup
- CategoryTheory.PreservesFiniteLimitsOfFlat.fac
- CategoryTheory.Limits.FintypeCat.jointly_surjective
- CategoryTheory.IsFiltered.cocone
- CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso
- CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom
- CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app
- CategoryTheory.IsCofiltered.cone_nonempty
- CategoryTheory.PreservesFiniteLimitsOfFlat.uniq
- FGModuleCat.instHasColimitsOfShapeOfFinCategory
- CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits
- CochainComplex.Plus.instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape
- CategoryTheory.finCategoryOpposite
- CategoryTheory.Limits.colimitLimitToLimitColimit_surjective
- CategoryTheory.finBiconeHom
- CategoryTheory.Arrow.finite
- CategoryTheory.FinCategory.objAsTypeToAsType_obj
- CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteColimits
- CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_finite_toFunctor
- CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory
- CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits
- CategoryTheory.Limits.CreatesFiniteColimits.createsFiniteColimits
- CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso
- CategoryTheory.FinCategory.fintypeHom
- FGModuleCat.instHasLimitsOfShapeOfFinCategory
- CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram
- CategoryTheory.Limits.ReflectsFiniteColimits.reflects
- CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteLimits
- CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac
- FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG
- CategoryTheory.FinCategory.asTypeEquivObjAsType
- CategoryTheory.FinCategory.asTypeFinCategory
- FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post
- CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim
- CategoryTheory.Limits.filtered_colim_preservesFiniteLimits
- FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG