Consider sets $G$ and $H$ and a function $f : G \rightarrow H$. So far, it doesn't really make sense to ask whether $G$ and $H$ are groups (technically, the answer is "no, they're not groups"), and it certainly doesn't make any sense to ask whether $f$ is a group homomorphism.
However, viewing $G$ and $H$ as sets equipped with a binary operation, it suddenly makes sense to ask whether $G$ and $H$ are groups. Suppose they are. Then, it also makes sense to ask whether or not $f$ is a group homomorphism.
So $G$ and $H$ are just sets, but in context they can be viewed as groups, or topological spaces, or whatever.
So what I'm looking for is a rigorous way of endowing sets with additional structure within specific contexts. So for example, in the "empty-context," set $G$ is just a set, with no additional structure. But within a context, $G$ might be equipped with a binary operation, or some open sets, or whatever.
As a more complete example, I'd like to make precise the meaning of theorems like the following.
Theorem. Let $G$ and $H$ denote sets and $f : G \rightarrow H$ denote a function. Let $\Gamma$ denote a context wherein $G$ and $H$ are groups and $f$ is a group homomorphism. Then the following are equivalent.
- $f$ is an injection
- In the context $\Gamma$, it holds that the kernel of $f$ is a singleton set.
Note that condition 1 is context-independent, because whether or not $f$ is an injection or not does not depend on the additional structure that $\Gamma$ endows upon $G$ and $H$. On the other hand, condition 2 is context-dependent, because the meaning of "the kernel of $f$" depends on the additional structure that $\Gamma$ endows upon $H$.
So in conclusion, I'm looking for a rigorous approach to this idea that sets can gain structure within contexts. I want something that is near computer-readable, and not "hand-waivy."
Remark. Groups are just an example; I am not specifically interested in groups.
Edit. What follows is the thinking that lead me to the idea of context.
Usually, we can make assumptions by opening a new "environment" in our proof. For instance, if $p$ is already a natural number, we can open a new environment in which we assume that $p$ is prime. If we prove the statement $p>10$ within the new environment, then we get to write the statement "If $p$ is prime, then $p>10$" in the original environment.
Now importantly, when we open a new environment in this way, we are not usually allowed to "remove" assumptions. For instance, if $p$ is already natural, we can write "Assume $p$ is prime," but we cannot write, "Assume $p$ is no longer natural." That is, we cannot undo an assumption by making a new assumption.
In a sense, this is exactly what I'm looking for. I'd like to be able to say,
"Assume $G$ is no longer just a set; assume it is now a set together with a binary operation satisfying the group axioms."
Of course, no assumption could possibly achieve this. An assumption cannot undo a previous assumption.
So we get clever; we invent the notion of a context. Our sentence becomes:
Let $\Gamma$ denote a context in which $G$ is no longer just a set; rather, it is now a set together with a binary operation satisfying the group axioms.
Now we've made a bit of progress, because we're no longer trying to use assumptions to undo other assumptions.
But this begs the question: what does the above sentence even mean? And what is the right definition of the word "context"?