Division of objects in categories I hope this is not vague, but it seems in some categories with products one can define a division operation on objects. This would at least be a partial operation on objects with the feature that $(A\times B)/ A$ is isomorphic to $B.$ My question is just, has this kind of idea come up before in the category theory literature ? If so I would be interested to know where.
 A: Allow me to address your question with two very general kinds of remarks:

*

*The "division" operation can (and should) be interpreted as a right adjoint to a cartesian/monoidal product operation. So, a way to interpret $B/A$ is as an internal hom $A\Rightarrow B$ of sorts. This leads to the marvellous world of cartesian/monoidal closed categories that needs no introduction of sorts.
Observe that in this case, there is no hope to obtain a "real" division operation because the most you can get is the counit of the adjunction $A\times- \dashv (-)/A$, i.e. a map
$$ \epsilon : A \times B/A \to B$$
in general not an isomorphism (the unit, on its own right, will give a map $\eta : A \to (A\times B)/B$). The adjunction identities now witness for the fact that although it's not true that $A \frac BA=A$ and $\frac{AB}B=A$, we still have a "lax isomorphism" between the two objects. This is the most you can get, in general, and the plethora of examples of cartesian/monoidal closed categories hints that it's not wise to ask for more.

This is not a definitive answer maybe (why division is a right adjoint, and not a left? What exactly does it mean for a map to be a "lax isomorphism"?)... but I can argue that it can be a satisfying response as it opens up a whole branch of category theory (its connection with proof theory and deductive systems):
As far as I can remember -but please, prove me wrong! I'm not that keen on bibliographic research-, representing left and right homs in a monoidal structure as left and right "division" operations dates back to the genius of J. Lambek: check for example

Lambek, Joachim. "The mathematics of sentence structure." The American Mathematical Monthly 65.3 (1958): 154-170.

Categorical grammars, proof theory, and all that lives in between follow up with this idea. Remarkable, if you ask me: it embodies Freyd's definition of categorical thinking (good ideas, low tech solutions, unifying overarching themes).
Tightly connected to this story is the definition of "dualisable object" in a monoidal category. Once again, google/the nLab can tell you way more than what I know, let me just add that the notion of dualisable object is the real point of connection between these two stories, because dualisable objects tend to be "finite" in some sense.

This said, there is a way more enticing way to address your question.


*Recall that in basic algebra, if you have a (say, commutative) monoid $(A, +)$, a sufficient condition for it to admit a well-behaved "group of fractions", where each element $a\in A$ has an "additive inverse" is that $A$ is cancellative; if it is, the very same idea that builds $\mathbb Z$ out of $\mathbb N$ (quotient of pairs $(m,n)$ of natural numbers) and ultimately $\mathbb Q$ from $\mathbb Z$ (but there $(m,n)\in \mathbb Z \times \mathbb Z\setminus \{0\}$, of course) yields the Grothendieck group of the monoid.
What happens if instead of a monoid I want to do the same thing to a monoidal category $(A, \otimes)$?
The question is certainly well-motivated (this construction quite certainly predates Grothendieck, but the killer application was to consider the "group of fractions" of the commutative monoid arising as "decategorification of the category of topological vector bundles over a fixed compact manifold $X$", or for short, the "$K_0$ of $X$").
There, the second component of a pair is the "virtual" element that you add to the "true" ones in order for the formal subtraction $[a]-[a]$ to be defined, and yield the unit element of $A$. You can (legitimately) denote your monoid operation as multiplication, so you can (again, legitimately) think of its formal inverse as being $\frac1a$, and thus $a\frac1a=1$ "by construction".

So are we good? Problem solved?

Well.. Remember the assumption above, that the monoid $A$ was cancellative? The problem here is that in a category a monoidal product is extremely very rarely cancellative, meaning that the implication
$$ A\otimes B \cong C\otimes B \Rightarrow A\cong C \tag{$\star$}$$
is almost never true for familiar choices of the ambient category and of the product $\otimes$. For example, it is false in the category of sets, in the category of abelian groups, in the category of topological spaces, in the category of fields, in most posets regarded as categories, in most monoids regarded as trivial monoidal categories...

Ok, but when am I allowed to build a "categorified" group of fractions? Grothendieck did it, after all!

You're right! There are interesting cases in which you can, because $\otimes$ is cancellative. In the world of category theory, cancellativity is a strong property, that (quoting from the other MSE thread) "at a very informal level, the validity of [$(\star)$] is bound to the assumption that the objects of C [the ambient category] are in some sense "finite"."
For example, $(\star)$ if false for sets, but it is true for finite sets; it is false for vector spaces/modules, but it's true for finite-dimensional vector spaces; it is false for groups, but it's (probably: I vaguely remember a thread proving this...) true for finite groups... In general, it is true if (but not "only if") your category is endowed with a "notion of dimension", a "notion of dimension" being a strong monoidal functor $\mathcal C \to (\mathbb N,+)$ that "reflects zero": if $\dim A=0$, then $A\cong I$, the monoidal unit.
A slightly more technical example of a "cancellative" category is the subcategory of functors $F : {\sf Fin} \to {\sf Set}$ satisfying the following properties:

*

*$F$ commutes with finitely filtered colimits

*the left Kan extension of $F$ along the inclusion $J : {\sf Fin} \subset {\sf Set}$ commutes with all colimits.

I have intentionally hidden all complexity and a lot of technicalities under the carpet, but the upshot is that 1+2 is true if and only if $F$ admits a left dual in the category $[{\sf Fin}, {\sf Set}]$; this is another time a finiteness request, because it entails that $F$ is

*

*uniquely determined by its action on $1$, and

*such that $F1$ is a finite set.

I hope I managed to show you, now, why I said that dualisability is the bridge between the first story and the second!
And sorry for the wall of text.
