Documentation

Mathlib.CategoryTheory.ConcreteCategory.Notation

Notation for bundling a type into a concrete category #

Concrete categories in Mathlib come with a bundling map called of, turning a type equipped with the relevant typeclasses into an object of the category: CommRingCat.of R, TopCat.of X, ModuleCat.of R M, ...

This file introduces the notation ↧X for FooCat.of X, where the category FooCat is read off from the expected type. The name FooCat.of is looked up in the environment rather than through a typeclass, so ↧X is syntactically the same as FooCat.of. It also provides a corresponding delaborator CategoryTheory.delabOf that must be manually registered for every concrete category.

Implementation notes #

A typeclass cannot mediate this notation while keeping the elaborated term syntactically FooCat.of: the typeclass assumptions of of vary between categories ([CommRing R] for CommRingCat, but [AddCommGroup M] [Module R M] for ModuleCat R, etc...), so they cannot be abstracted away. Instead, ↧ guesses the relevant of function from the expected type FooCat .., and in particular assumes it is named FooCat.of.

We further assume of FooCat.of that the carrier is its last explicit argument. This covers both categories whose of is the structure constructor (CommRingCat.of R) and parameterised categories, where the parameters come first (ModuleCat.of R M): in the latter case the leading explicit arguments are elaborated as _ and solved by unification with the expected type.

source
def CategoryTheory.OfNotation.explicitArgs? (ty : Lean.Expr) :
Option (Nat × Nat)

The number of explicit arguments of a declaration of type ty, together with the index of the last one among all of its arguments.

Metadata is ignored. Returns none if ty takes no explicit argument.

Equations
Instances For
    source
    partial def CategoryTheory.OfNotation.findOf? (ty : Lean.Expr) :
    Lean.MetaM (Option (Lean.Name × Nat))

    Find the bundling map FooCat.of to use for the type ty, along with its number of explicit arguments.

    Before unfolding ty, we check its head constant FooCat, since a category can be reducibly defined in terms of another one while still having its own of: Profinite reduces to CompHausLike _, yet ↧X : Profinite should be Profinite.of X, not CompHausLike.of _ X. If no .of is found for the non-unfolded ty, we unfold it and try again.

    source
    def CategoryTheory.«term↧_» :
    Lean.ParserDescr

    ↧X is the object of a concrete category corresponding to the type X, i.e. FooCat.of X where the category FooCat is determined by the expected type.

    ↧X elaborates to a literal application of FooCat.of.

    • (↧R : CommRingCat) is CommRingCat.of R,
    • (↧M : ModuleCat R) is ModuleCat.of R M,
    • (↧A : CommAlgCat R) is CommAlgCat.of R A.

    The expected type must be known.

    Equations
    Instances For
      source
      def CategoryTheory.delabOf :
      Lean.PrettyPrinter.Delaborator.Delab

      Delaborate FooCat.of … X to ↧X.

      Tag FooCat.of with this to make it print using the ↧ notation:

      @[app_delab FooCat.of] meta def FooCat.delabOf := CategoryTheory.delabOf

      This falls back to delabApp, so that FooCat.of X doesn't get printed as { carrier := X, … } by delabStructureInstance even if delaboration fails in case FooCat.of is the constructor of structure FooCat.

      Equations
      Instances For