Is there a rigorous theory of context, whereby sets can gain additional structure within a context?

Question

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.

1. $f$ is an injection
2. 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"?

Answer 1

I'm not entirely sure what you are after, but perhaps the following will be useful to you.

Fixing a context $\Gamma $ can be thought of as fixing a category $C$. After all, the context you seem to be referring to amounts to specifying the axioms of a structure on sets and then singling out the structure preserving functions, calling them homomorphisms.

Thus, actually, you are looking at concrete categories: a category $C$ together with a faithful forgetful functor to $Set$. Basically, this says that the things in your context are sets endowed with some extra structure and that the morhpisms are structure preserving functions.

Now the theorem you quote can be re-written as follows. Consider the concrete category $Grp$ of groups and group homomorphisms with its forgetful functor $U:Grp \to Set$. Let $G,H$ be groups and $f:G\to H$ a homomorphism. The following are equivalent:

1) $U(f):U(G)\to U(H)$ is an injective function.

2) $f:G\to H$ has trivial kernel.

So now your observation that condition one is context free simply means that you consider a property of something in the context of groups after applying the forgetful functor to. The observation that condition 2 is context dependent means that it is happening in the category $Grp$ and not in $Set$.

Since dealing with kernels categorically is slightly, involved lets instead consider the notion of monomorphism categorically. A morphism $f:A\to B$ is a monomorphism if it can be cancled on the left: given $g,h:Z\to A$ with $f\circ g=f\circ h$, it follows that $g=h$.

Now, the following holds:

1) In the category $Set$ of sets and functions, a morphism $f$ is a monomorphism iff it is an injective function.

2) In the category $Grp$ of groups and homomorphisms, a morphism $f$ is a monomorphism iff its kernel is trivial.

Both of these theorems characterize monomorphism in the category in terms of some other property.

Now, your thoerem can be restated again as:

A morphism $f$ in $Grp$ is a monomorphism iff $U(f)$ is a monomorphism.

So, you seem to be interested in properties that are reflected and/or preserved by the forgetful functor. At this point I'll refer you to the book Abstract and concrete categories