请输入您要查询的字词:

 

单词 2142EqualityOfSemigroups
释义

2.14.2 Equality of semigroups


Using the equations for path spaces discussed in the previous sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath,we can investigate when two semigroupsPlanetmathPlanetmath are equal. Given semigroups(A,m,a) and (B,m,a), by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), the type of paths(A,m,a)=𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉(B,m,a)is equal to the type of pairs

p1:A=𝒰B  and
p2:𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋(p1,(m,a))=(m,a).

By univalence, p1 is 𝗎𝖺(e) for some equivalence e. ByTheorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), function extensionality, and the above analysis oftransport in the type family 𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋, p2 is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a pairof proofs, the first of which shows that

y1,y2:Be(m(e-1(y1),e-1(y2)))=m(y1,y2)

and the second of which shows that a is equal to the inducedassociativity proof constructed from a in2.14.3 (http://planetmath.org/2141liftingequivalences#S0.E1). But by cancellation of inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath2.14.2 (http://planetmath.org/2141liftingequivalences#S0.E2X) is equivalent to

x1,x2:Ae(m(x1,x2))=m(e(x2),e(x2)).

This says that e commutes with the binary operationMathworldPlanetmath, in the sensethat it takes multiplication in A (i.e. m) to multiplication in B(i.e. m). A similar rearrangement is possible for the equation relatinga and a. Thus, an equality of semigroups consists exactly of anequivalence on the carrier types that commutes with the semigroupstructureMathworldPlanetmath.

For general types, the proof of associativity is thought of as part ofthe structure of a semigroup. However, if we restrict to set-like types(again, see http://planetmath.org/node/87576Chapter 3), theequation relating a and a is trivially true. Moreover, in thiscase, an equivalence between sets is exactly a bijection. Thus, we havearrived at a standard definition of a semigroup isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: abijection on the carrier sets that preserves the multiplicationoperationMathworldPlanetmath. It is also possible to use the category-theoretic definitionof isomorphism, by defining a semigroup homomorphism to be a mapthat preserves the multiplication, and arrive at the conclusionMathworldPlanetmath that equality ofsemigroups is the same as two mutually inverse homomorphismsMathworldPlanetmathPlanetmathPlanetmath; but wewill not show the details here; see §9.8 (http://planetmath.org/98thestructureidentityprinciple).

The conclusion is that, thanks to univalence, semigroups are equalprecisely when they are isomorphic as algebraic structuresPlanetmathPlanetmath. As we will see in §9.8 (http://planetmath.org/98thestructureidentityprinciple), theconclusion applies more generally: in homotopy type theory, all constructions ofmathematical structures automatically respect isomorphisms, without anytedious proofs or abuse of notation.

随便看

 

数学辞典收录了18232条数学词条,基本涵盖了常用数学知识及数学英语单词词组的翻译及用法,是数学学习的有利工具。

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 4:19:19