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:

1. 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).
2. 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 ?

• As you're noticing, the tricky part is identifying just which properties are preserved by, or invariant under, isomorphisms — and, by extension, which ones aren't. I think it's safe to say that there isn't a (uniform) way to "read off" or generate a list of all and only all those properties from the definition of the objects and morphisms of a category. – BrianO Feb 11 '16 at 11:41
• To expand a bit on what @BrianO said, isomorphisms differ between different kinds of objects. Broadly speaking, isomorphisms preserve "structure" between objects, but what this "structure" is depends very much on whether you are talking about groups, vector spaces, algebras, etc. Hence it's difficult to say what properties are preserved in general by isomorphisms. – mrp Feb 11 '16 at 11:49
• @mrp +1 on that. Groups, Abelian groups, ... algebras, all topological spaces, compact Hausdorff spaces, partially ordered sets, partially ordered monoids, the category arising from a single partially ordered set, topoi, ... General abstract nonsense is really very general :) – BrianO Feb 11 '16 at 11:58
• – goblin Feb 14 '16 at 10:08

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.