nLab generalized the

Redirected from "unique".
Contents

Context

Category theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Contents

Idea

In natural language, the definite article (‘the’ in English) is generally used only for nouns which are uniquely characterized by context. Hence we have “the Moon” and “the book I was just reading,” but only “a car” or “a wild late-night party.” (Sometimes “the book I was just reading” is abbreviated to “the book”, but it should be clear from context that only one book could be meant.) Philosophers call this use of the definite article to pick out an individual definite description.

In mathematics, and especially in category theory, homotopy theory/homotopy type theory and generally in higher category theory, it is common to use “the” more generally for objects/types which are characterized only up to coherent isomorphism/equivalence: Such need not actually be unique, but any two of them are isomorphic or more generally coherently equivalent in an essentially unique way (meaning that the ∞-groupoid of all such objects is contractible).

For example, one speaks (assuming that any exists) of “the” terminal object of a category, “the” Cartesian product of two objects, “the” left adjoint of a functor, and so on. Outside of pure category theory we have examples such as “the” Dedekind-complete ordered field (the field of real numbers).

Formalization

The notion of a “generalized the” can be formalized and treated uniformly in homotopy type theory. Here one may define an introduction rule for the as follows:

(A:Type),((a,p):IsContr(A))(the(A,a,p):A). (A:Type),((a,p):IsContr(A)) \vdash (the(A,a,p):A).

Here the term (a,p)(a,p) is one witness for the contractibility of the type AA. Then we have the(A,a,p)=a:Athe(A,a,p)=a:A.

Since IsContr(A)IsContr(A) is itself contractible, we could say that (a,p)(a,p) is the witness for the contractibility of the type AA, which may explain why we do not generally mention it.

If we wish to extend this treatment to types which are propositions, we might call such types FactThat(P)FactThat(P), for some statement PP. Then if PP holds, we can introduce a term ‘the(FactThat(P))the(FactThat(P))’.

References

The term “generalized the” was introduced by James Dolan and may first appear in print here:

Quoting:

Given a tensor product of the 2-Hilbert spaces HH and HH', we often write its underlying 2-Hilbert space as HHH \otimes H'. This notation may tempt one to speak of ‘the’ tensor product of HH and HH', which is is legitimate if one uses the generalized ‘the’ as advocated by Dolan [7]. In a set, when we speak of ‘the’ element with a given property, we implicitly mean that this element is unique. In a category, when we speak of ‘the’ object with a given property, we merely mean that this object is unique up to isomorphism — typically a specified isomorphism. Similarly, in a 2-category, when we speak of ‘the’ object with a given property, we mean that this object is unique up to equivalence — typically an equivalence that is specified up to a specified isomorphism. This is the sense in which we may refer to ‘the’ tensor product of HH and HH'. The generalized ‘the’ may be extended in an obvious recursive fashion to nn-categories.

Discussion in homotopy type theory:

Last revised on October 15, 2024 at 18:49:42. See the history of this page for a list of all contributions to it.