This is an attempt to define the localization of an algebra at an arbitrary multiplicatively closed subset of it, compared with the current localization at a multiplicatively closed subset of the base ring. I've had many attempts, trying to use CT and the fact that algebras over a base ring are equivalent to rings under a base ring, but the definitional behavior was really hard to predict and things just didn't compute well. I chose instead to just extend the existing construction in the most straightforward way. I'm still trying to formulate a recursion principle using the universal property, so that we're able to prove things about the localization without resorting to its actual construction.
Hi,
This is an attempt to define the localization of an algebra at an arbitrary multiplicatively closed subset of it, compared with the current localization at a multiplicatively closed subset of the base ring. I've had many attempts, trying to use CT and the fact that algebras over a base ring are equivalent to rings under a base ring, but the definitional behavior was really hard to predict and things just didn't compute well. I chose instead to just extend the existing construction in the most straightforward way. I'm still trying to formulate a recursion principle using the universal property, so that we're able to prove things about the localization without resorting to its actual construction.
This depends on a rebased version of #931.
LMKWYT