请输入您要查询的字词:

 

单词 41Quasiinverses
释义

4.1 Quasi-inverses


We have said that 𝗊𝗂𝗇𝗏(f) is unsatisfactory because it is not a mere proposition, whereas we would rather that a given function can “be an equivalence” in at most one way.However, we have given no evidence that 𝗊𝗂𝗇𝗏(f) is not a mere proposition.In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we exhibit a specific counterexample.

Lemma 4.1.1.

If f:AB is such that qinv(f) is inhabited, then

𝗊𝗂𝗇𝗏(f)(x:A(x=x)).
Proof.

By assumptionPlanetmathPlanetmath, f is an equivalence; that is, we have e:𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f) and so (f,e):AB.By univalence, 𝗂𝖽𝗍𝗈𝖾𝗊𝗏:(A=B)(AB) is an equivalence, so we may assume that (f,e) is of the form 𝗂𝖽𝗍𝗈𝖾𝗊𝗏(p) for some p:A=B.Then by path inductionMathworldPlanetmath, we may assume p is 𝗋𝖾𝖿𝗅A, in which case 𝗂𝖽𝗍𝗈𝖾𝗊𝗏(p) is 𝗂𝖽A.Thus we are reduced to proving 𝗊𝗂𝗇𝗏(𝗂𝖽A)((x:A)(x=x)).Now by definition we have

𝗊𝗂𝗇𝗏(𝗂𝖽A)g:AA((g𝗂𝖽A)×(g𝗂𝖽A)).

By function extensionality, this is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to

g:AA((g=𝗂𝖽A)×(g=𝗂𝖽A)).

And by http://planetmath.org/node/87641Exercise 2.10, this is equivalent to

h:(g:AA)(g=𝗂𝖽A)(𝗉𝗋1(h)=𝗂𝖽A)

However, by Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), (g:AA)(g=𝗂𝖽A) is contractibleMathworldPlanetmath with center 𝗂𝖽A; therefore by Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6) this type is equivalent to 𝗂𝖽A=𝗂𝖽A.And by function extensionality, 𝗂𝖽A=𝗂𝖽A is equivalent to (x:A)x=x.∎

We remark that http://planetmath.org/node/87864Exercise 4.3 asks for a proof of the above lemma which avoids univalence.

Thus, what we need is some A which admits a nontrivial element of (x:A)(x=x).Thinking of A as a higher groupoidPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, an inhabitant of (x:A)(x=x) is a natural transformation from the identity functor of A to itself.Such transformationsPlanetmathPlanetmath are said to form the center of a categoryMathworldPlanetmath,since the naturality axiom requires that they commute with all morphismsMathworldPlanetmath.Classically, if A is simply a group regarded as a one-object groupoid, then this yields precisely its center in the usual group-theoretic sense.This provides some motivation for the following.

Lemma 4.1.2.

Suppose we have a type A with a:A and q:a=a such that

  1. 1.

    The type a=a is a set.

  2. 2.

    For all x:A we have a=x.

  3. 3.

    For all p:a=a we have p\\centerdotq=q\\centerdotp.

Then there exists f:(x:A)(x=x) with f(a)=q.

Proof.

Let g:(x:A)a=x be as given by 2. First weobserve that each type x=Ay is a set. For since being a set is a mereproposition, we may apply the induction principle of propositional truncation, and assume that g(x)=|p| and g(y)=|q| for p:a=x and q:a=y. In this case, composing withp and q-1 yields an equivalence (x=y)(a=a). But (a=a) isa set by 1, so (x=y) is also a set.

Now, we would like to define f by assigning to each x the path g(x)-1\\centerdotq\\centerdotg(x), but this does not work because g(x) does not inhabit a=xbut rather a=x, and the type (x=x) may not be a mere proposition,so we cannot use induction on propositional truncation. Instead we can applythe technique mentioned in §3.9 (http://planetmath.org/39theprincipleofuniquechoice): we characterizeuniquely the object we wish to construct. Let us define, for each x:A, thetype

B(x):(r:x=x)(s:a=x)(r=s-1\\centerdotq\\centerdots).

We claim that B(x) is a mere proposition for each x:A.Since this claim is itself a mere proposition, we may again apply induction ontruncation and assume that g(x)=|p| for some p:a=x.Now suppose given (r,h) and (r,h) in B(x); then we have

h(p)\\centerdoth(p)-1:r=r.

It remains to show that h is identified with h when transported along this equality, which by transport in identity types and function types (§2.11 (http://planetmath.org/211identitytype),§2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom)), reduces to showing

h(s)=h(p)\\centerdoth(p)-1\\centerdoth(s)

for any s:a=x.But each side of this is an equality between elements of (x=x), so it follows from our above observation that (x=x) is a set.

Thus, each B(x) is a mere proposition; we claim that (x:A)B(x).Given x:A, we may now invoke the induction principle of propositional truncation to assume that g(x)=|p| for p:a=x.We define r:p-1\\centerdotq\\centerdotp; to inhabit B(x) it remains to show that for any s:a=x we haver=s-1\\centerdotq\\centerdots.Manipulating paths, this reduces to showing that q\\centerdot(p\\centerdots-1)=(p\\centerdots-1)\\centerdotq.But this is just an instance of 3.∎

Theorem 4.1.3.

There exist types A and B and a function f:AB such that qinv(f) is not a mere proposition.

Proof.

It suffices to exhibit a type X such that (x:X)(x=x) is not a mere proposition.Define X:(A:𝒰)𝟐=A, as in the proof of Lemma 3.8.5 (http://planetmath.org/38theaxiomofchoice#Thmprelem2).It will suffice to exhibit an f:(x:X)(x=x) which is unequal to λx.𝗋𝖾𝖿𝗅x.

Let a:(𝟐,|𝗋𝖾𝖿𝗅𝟐|):X, and let q:a=a be the path corresponding to the nonidentity equivalence e:𝟐𝟐 defined by e(0𝟐):1𝟐 and e(1𝟐):0𝟐.We would like to apply Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) to build an f.By definition of X, equalities in subset types (§3.5 (http://planetmath.org/35subsetsandpropositionalresizing)), and univalence, we have (a=a)(𝟐𝟐), which is a set, so 1 holds.Similarly, by definition of X and equalities in subset types we have 2.Finally, http://planetmath.org/node/87644Exercise 2.13 implies that every equivalence 𝟐𝟐 is equal to either 𝗂𝖽𝟐 or e, so we can show 3 by a four-way case analysis.

Thus, we have f:(x:X)(x=x) such that f(a)=q.Since e is not equal to 𝗂𝖽𝟐, q is not equal to 𝗋𝖾𝖿𝗅a, and thus f is not equal to λx.𝗋𝖾𝖿𝗅x.Therefore, (x:X)(x=x) is not a mere proposition.∎

More generally, Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) implies that any “Eilenberg–Mac Lane space” K(G,1), where G is a nontrivial abelian groupMathworldPlanetmath, will provide a counterexample; see http://planetmath.org/node/87582Chapter 8.The type X we used turns out to be equivalent to K(2,1).In http://planetmath.org/node/87579Chapter 6 we will see that the circle 𝕊1=K(,1) is another easy-to-describe example.

We now move on to describing better notions of equivalence.

随便看

 

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

 

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