Mathlib Map

Structures · Category theory

CategoryTheory.Category

The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

Defined in
Mathlib.CategoryTheory.Category.Basic
Shape
One type argument · adds id_comp, comp_id, assoc
Open in Mathlib docs

Extends1

Extended by1

Forgetful instances

Every CategoryTheory.Category is also a

Concrete types that are instances100

  • Quiver.Hom
  • CategoryTheory.Functor.obj
  • CategoryTheory.Functor
  • CategoryTheory.Over
  • ModuleCat
  • CategoryTheory.Grp
  • HomologicalComplex
  • CategoryTheory.PreZeroHypercover.I₀
  • Action
  • CategoryTheory.Mon
  • AlgebraicGeometry.Scheme
  • AddCommGrpCat
  • CategoryTheory.ObjectProperty.FullSubcategory
  • TopCat
  • CategoryTheory.ShrinkHoms
  • CategoryTheory.MonoidalOpposite
  • Rep
  • CategoryTheory.Quotient
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • SheafOfModules
  • CategoryTheory.Paths
  • CategoryTheory.Ind
  • CategoryTheory.Skeleton
  • CategoryTheory.Comma
  • SSet.Truncated.HomotopyCategory
  • CategoryTheory.Cat.FreeRefl
  • HomotopyCategory
  • CategoryTheory.WithTerminal
  • CategoryTheory.WithInitial
  • CommRingCat
  • AlgebraicGeometry.SheafedSpace
  • AlgebraicGeometry.LocallyRingedSpace
  • PresheafOfModules
  • CategoryTheory.Under
  • CategoryTheory.MorphismProperty.Localization
  • CategoryTheory.InducedCategory
  • DerivedCategory
  • AlgebraicGeometry.Scheme.Modules
  • CategoryTheory.CostructuredArrow
  • ContinuousGeneratedByCat
  • AlgCat
  • CategoryTheory.GradedObject
  • CategoryTheory.StructuredArrow
  • AlgebraicGeometry.PresheafedSpace
  • CommMonCat
  • TopCat.Presheaf
  • ProfiniteGrp
  • CategoryTheory.Arrow
  • CategoryTheory.Center
  • CategoryTheory.Limits.Cocone
  • CategoryTheory.Limits.Cone
  • CategoryTheory.Bundled.α
  • CategoryTheory.AddGrp
  • AddCommMonCat
  • CategoryTheory.AddMon
  • CategoryTheory.MorphismProperty.Comma
  • TopCat.Sheaf
  • MonCat
  • CategoryTheory.Limits.CatCospanTransform
  • CategoryTheory.ShortComplex
  • CategoryTheory.Pairwise
  • AddMonCat
  • CategoryTheory.ULiftHom
  • CategoryTheory.Bicone
  • CategoryTheory.Comonad.Coalgebra
  • CompHausLike
  • CategoryTheory.Monad.Algebra
  • CategoryTheory.SingleObj
  • CategoryTheory.MorphismProperty.LeftFraction.Localization
  • QuadraticModuleCat
  • SemimoduleCat
  • TopModuleCat
  • CategoryTheory.Monoidal.Transported
  • CommAlgCat
  • PartOrdEmb
  • RingCat
  • CommSemiRingCat
  • CategoryTheory.Limits.limit
  • HopfAlgCat
  • CategoryTheory.Monad
  • CategoryTheory.Pretriangulated.Triangle
  • CategoryTheory.Comon
  • CategoryTheory.Comonad
  • BialgCat
  • CategoryTheory.Idempotents.Karoubi
  • CategoryTheory.Mat_
  • TopRep
  • AddSemigrp
  • Semigrp
  • CategoryTheory.WideSubcategory
  • SemiRingCat
  • CategoryTheory.FreeMonoidalCategory
  • CoalgCat
  • CommBialgCat
  • Sequential
  • TopCommRingCat
  • Preord
  • Compactum

How is a type an instance?

Loading the hierarchy index…

Assumed by46,547

Ancestors40