Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m just here to check the code since there’s no way to check in the editor.
Proof: Take any isomorphism $f$, let $f = gh$ and $h f^{-1} = g' h'$ be the unique factorizations. Then $id = ghf^{−1} = (gg')h'$, so $h' = id$ and $gg' = id$, whence $g = id$ and $g' = id$ since $g, g' \in R_+$. Thus $f = h \in R_−$. The same argument applied to $f^{−1}$ shows that $f$ preserves the degree, hence $f = id$.
I’m just here to check the code since there’s no way to check in the editor.
Proof: Take any isomorphism $f$, let $f = gh$ and $h f^{-1} = g' h'$ be the unique factorizations. Then $id = gh f^{−1} = (gg')h'$, so $h' = id$ and $gg' = id$, whence $g = id$ and $g' = id$ since $g, g' \in R_+$. Thus $f = h \in R_−$. The same argument applied to $f^{−1}$ shows that $f$ preserves the degree, hence $f = id$.
For checking code for the $n$Lab best to use the Sandbox page.
The parser here on the $n$Forum does not behave identically to that for $n$Lab pages.
1 to 5 of 5