What's an Isomorphism?
I'm familiar with the definition (inverses and bijections, preserving operations) in the context of groups and vector spaces, the hoeomorphism of topological spaces, and have some feeling for the definition in category theory.
What I'm looking for is a mathematical justification:
- for statements like "....two isomorphic objects cannot be distinguished by using only the properties used to define morphisms; thus isomorphic objects may be considered the same as long as one considers only these properties and their consequences" (https://en.wikipedia.org/wiki/Isomorphism).
- for the reliance on isomorphism in proofs. For example, the internal direct sum of subspaces of a vector space is isomorphic to the external direct sum of these subspaces. One can prove that the internal direct sum is associative and commutative and then call on isomorphism to say the same applies to the external direct sum.
I would imagine somewhere in category theory there is some result along the lines that if $\phi$ is an isomorphism between two objects $O_1, O_2$ in a category, and $P$ is some logic statement about $O_1$ then $\phi(P) = P$, i.e. the logic statement about the corresponding entities in $O_2$ is true or false in accordance with the statement in $O_1$.
Maybe my imagination is running ahead of the facts, but I would appreciate some feedback on the formalisation of "...B is isomorphic to A and therefore since P is true in A ..."
Addendum: thanks for comments and answer. It seems that an easily accessible answer applicable across all categories may be too much to aim for. What about answers for specific categories ? If one takes for example the category of topological spaces it appears (from what I've read) that "properties which can be defined in terms of open sets are preserved by homeomorphism". Can this statement be proved as such, or must one execute specific proofs for compactness, connectedness, convergence, etc ?
So, as you've noticed, this notion is absolutely ubiquitous.
There's a general notion of "isomorphic objects are equal (for all intents and purposes)". Particularly for categorists, notions that distinguish between isomorphic (or more generally, equivalent) objects are often referred to as "evil". In category theory, the principle you describe is called the principle of equivalence (or principle of isomorphism for a weaker notion). Most definitions of category theory use standard set theory and thus readily allow for evil definitions. As such, there is no principle of equivalence for those definitions; you can readily state properties that do not hold under equivalence of categories (or even isomorphisms of categories). This is because, in standard set theory, there is a global notion of equality which will always be able to distinguish between non-equal isomorphic objects.
If you look at the link above, you'll notice a lot of references to Homotopy Type Theory. This is a very new and very exciting development that directly addresses this issue. The most relevant part for you is the Univalence Axiom. The Univalence Axiom literally states that, in the context of homotopy type theory, equality is equivalent to equivalence. So all that treating isomorphic objects as equal is completely justified in homotopy type theory. By itself that wouldn't be that exciting, but homotopy type theory is a (fairly minor in some ways) extension of Martin Löf type theory which has been studied by type theorists and computer scientists and implemented for decades. It is the logical foundation for the Coq proof assistant. This means that 1) we have implementations of this logic already, 2) this logic is demonstrably able to formalize just about any mathematical notion, and 3) people are already doing real math in this. In other words, this incarnation of the principle of equivalence effectively encompasses all of mathematics (in practice), and homotopy type theory provides a possible "foundations" for mathematics that much more directly matches how mathematicians actually do mathematics.
There are other approaches to this besides homotopy type theory. The link above mentioned FOLDS which is a much more conservative approach, but Makkai's work is generally worth checking out.
To step back a bit, the reason there is no theorem like you mention in category theory (as should be clear from the above) is that it isn't a theorem about category theory. It's a theorem about whatever meta-logic you are using to define category theory and those predicates $P$. There are three routes to go from here. You can just give up on such a property which is, technically, what just about everyone does for category theory. You can formulate a logic that is easy to specify and for which well-formedness is easy to check, and then prove the property about this logic. This is essentially what happens at the informal level and occasionally is formalized. For example, you can easily prove that the theorems in Peano arithmetic do not depend on what exactly numbers are, or that rational number arithmetic is well-defined. The problem with this route is that it is restrictive; only relatively simple properties can be stated and oftentimes even then only awkwardly. The third route, then, is to make a rich (but difficult to fully specify) logic that allows you to naturally and directly express what you want but whose well-formedness is (relatively) difficult to verify. This is the route homotopy type theory takes. (FOLDS is in between the second and third route.) This is what roughly what happens at an informal level for most mathematical work. Nominally set theory is the logic we're working in, but it is understood that polite company does not ask whether $2\in 3$ or whether $A\times B \times C$ is $(A\times B)\times C$ or $A\times(B\times C)$ or something else. There's an implicit notion of/language for "reasonable" questions to ask, and for those "reasonable" questions isomorphic objects are not distinguished.