This page is about the concept in functorial algebraic geometry. For functors between Z-categories see there.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A -functor or integers functor is a functor from the category of commutative rings CRing to the category of sets Set. The category of -functors is thus the functor category .
The forgetful functor is a -functor.
An affine scheme is a representable -functor.
Let be a -functor. Then the ring of fractions of is the set of natural transformations from to the forgetful functor .
The ring structure on is defined pointwise by the following, for every commutative ring and element :
The terminology β-functorβ is due to
(later volumes never appeared)
popularized through the English translation of the first couple of chapters:
Formulation in univalent homotopy type theory:
Last revised on November 9, 2024 at 02:00:56. See the history of this page for a list of all contributions to it.