Category instance for algebras over a commutative ring #
We introduce the bundled category AlgebraCat
of algebras over a fixed commutative ring R
along
with the forgetful functors to RingCat
and ModuleCat
. We furthermore show that the functor
associating to a type the free R
-algebra on that type is left adjoint to the forgetful functor.
An alias for AlgebraCat.{max u₁ u₂}
, to deal around unification issues.
Since the universe the ring lives in can be inferred, we put that last.
Instances For
The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.
Instances For
Typecheck a AlgHom
as a morphism in AlgebraCat R
.
Instances For
Forgetting to the underlying type and then building the bundled object returns the original algebra.
Instances For
The "free algebra" functor, sending a type S
to the free algebra on S
.
Instances For
The free/forget adjunction for R
-algebras.
Instances For
Build an isomorphism in the category AlgebraCat R
from a AlgEquiv
between Algebra
s.
Instances For
Build a AlgEquiv
from an isomorphism in the category AlgebraCat R
.
Instances For
Algebra equivalences between Algebra
s are the same as (isomorphic to) isomorphisms in
AlgebraCat
.