2 ms·
I think the magic word is: isomorphism! An isomorphism is a way to relate two different sets such that each element is paired with exactly one in the other set
by _nalply 2y ago
I think the magic word is: isomorphism!
An isomorphism is a way to relate two different sets such that each element is paired with exactly one in the other set such that it does not matter if you do operations before or after.
In my calculator the set of reals is isomorph to the set of complex numbers with imaginary part zero:
ℝ ⬄ { c | c ∈ ℂ and im(c) = 0 }
So I can coerce to complex numbers without impunity because of that isomporphism! And I know it is an isomorphism because if adding two reals then coercing to complex is the same as coercing first then adding.
TIL: In a way mathematics has types like programming languages.
I hope I am not too far off here. I didn't look up anything, this all went into my head this morning.
- ndriscoll 2y agoThis is sort of true, but there are isomorphisms which aren't "good enough" in some sense. E.g. if you're familiar with linear algebra, there's a thing called a dual space, which (for finite dimensions) is isomorphic to your space, but when you change coordinates, dual spaces change their coordinates backwards. Or for complex numbers, when you extend R by adding `i` (sometimes written C=R[i]), if you look carefully, you'll see that you could have instead added an element α = -i, and you'll notice that R[α] is isomorphic to R[i] in a way where the isomorphism maps R to itself; in a sense you can't tell whether you added i or -i, and this degree of freedom is important when studying field extensions. The closest thing I'm aware of to "pretty much equal" is "unique up to unique isomorphism", so they may not be equal, but they're isomorphic, and there's no flexibility to make any choices of which isomorphism to use. But "isomorphism" also implies you have a particular context/structure in mind that you want to preserve, e.g. a set isomorphism (a bijection) may not be a linear isomorphism (~an invertible matrix). In practice, you may be working in multiple contexts at once, so you invent Functors which map one type of morphism to another, and now you care about Categories.