Mathlib Map

Structures · Category theory

CategoryTheory.ConcreteCategory

A concrete category is a category C where objects correspond to types and morphisms to (bundled) functions between those types. In other words, it has a fixed faithful functor forget : C ⥤ Type. Note that ConcreteCategory potentially depends on three independent universe levels, * the universe level w appearing in forget : C ⥤ Type w * the universe level v of the morphisms (i.e. we have a Category.{v} C) * the universe level u of the objects (i.e C : Type u) They are specified that order, to avoid unnecessary universe annotations.

Defined in
Mathlib.CategoryTheory.ConcreteCategory.Basic
Shape
2 explicit arguments · adds hom, ofHom, hom_ofHom, ofHom_hom, id_apply, comp_apply
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances80

  • ModuleCat
  • Action
  • AddCommGrpCat
  • CategoryTheory.ObjectProperty.FullSubcategory
  • TopCat
  • Rep
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • CommRingCat
  • CategoryTheory.InducedCategory
  • ContinuousGeneratedByCat
  • AlgCat
  • CommMonCat
  • ProfiniteGrp
  • AddCommMonCat
  • MonCat
  • AddMonCat
  • CompHausLike
  • QuadraticModuleCat
  • SemimoduleCat
  • TopModuleCat
  • CommAlgCat
  • PartOrdEmb
  • RingCat
  • CommSemiRingCat
  • HopfAlgCat
  • BialgCat
  • TopRep
  • AddSemigrp
  • Semigrp
  • SemiRingCat
  • CoalgCat
  • CommBialgCat
  • Sequential
  • TopCommRingCat
  • Preord
  • Compactum
  • CommHopfAlgCat
  • CompactlyGenerated
  • FinBddDistLat
  • HeytAlg
  • AlexDisc
  • BddOrd
  • BoolAlg
  • AddMagmaCat
  • ProfiniteAddGrp
  • LinOrd
  • Frm
  • CategoryTheory.DifferentialObject
  • BddDistLat
  • BoolRing
  • LightDiagram
  • FinTopCat
  • MagmaCat
  • FiniteGrp
  • FiniteAddGrp
  • Lat
  • DistLat
  • PartOrd
  • DiscreteContAction
  • SimplexCategory
  • SemiNormedGrp
  • SemiNormedGrp₁
  • UniformSpaceCat
  • FinBoolAlg
  • NonemptyFinLinOrd
  • FinPartOrd
  • SemilatInfCat
  • CompleteLat
  • CpltSepUniformSpace
  • SemilatSupCat
  • BddLat
  • TwoP
  • GrpWithZero
  • ωCPO
  • Bipointed
  • Born
  • MeasCat
  • Pointed

How is a type an instance?

Loading the hierarchy index…

Assumed by564

Ancestors0

No ancestors.