Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorYimingXu
    • CommentTimeNov 13th 2020
    • (edited Nov 13th 2020)

    I am reading the following document about Lawvere’s ETCS:

    My question is about Theorem 6 in this document. The aim is to prove an equivalence relation is an equalizer. On page 29, the author says:

    Finally we can assert our theorem (I think the a 0q=a 1ga_0q = a_1g in the link is a typo.) a 0q=a 1qa_0q = a_1q iff a 0a 1a_0 \equiv a_1.

    And finished the proof.

    That is, the author proves for every element a 0,a 1\langle a_0,a_1\rangle from the terminal object 11, we have the split via the map which we want to prove to be an equalizer. But to prove the equalizer result, we need that we still have the factorization when 11 is replaced by any arbitrary object. I know that 11 is the generator in ETCS, and have trouble working out the proof that the existence of factorization for 11 implies the existence of factorization for any TT. I tried taking the elements of TT, and unable to construct a factorization from TT from the factorization for its elements.

    Any help, please? Thank you!

    Note: If someone is reading the link above, then please note that the composition is written as: if f:AB,g:BCf: A \to B,g: B\to C, then the author will write fgfg to denote the composition of ff of gg, rather than gfg \circ f.

    • CommentRowNumber2.
    • CommentAuthorRichard Williamson
    • CommentTimeNov 14th 2020
    • (edited Nov 14th 2020)

    Interesting question! Do I understand correctly that you are essentially asking about the statement “which clearly implies the assertion in the theorem” in the first sentence of the proof of Theorem 6? I agree with you that the intended logic is not immediately obvious. We know that the required equaliser exists by Axiom 1. What the implication in the first sentence of the proof of Theorem 6 shows is that the image of this equaliser is a subset of the image of ff; the other way around is obvious from the universal property of an equaliser. From this, it is I thimk straightforward (recalling that ff and the equaliser are monomorphisms and admit retractions), using the fact that 11 is a generator, to deduce that ff is also an equaliser. Of course this has to be made formal in ETCS, but I think that is the way the argument goes, or at least can go.

    • CommentRowNumber3.
    • CommentAuthorYimingXu
    • CommentTimeNov 14th 2020
    • (edited Nov 14th 2020)

    Thanks a lot for replying! Yes, I am asking about why does it “clearly implies the assertion in the theorem” in the first sentence of the proof of Theorem 6, and I think I get your comment before “from this”. To confirm this argument. Do you mean that the first sentence of the proof gives ERE \subset R (EE is the equalizer) and the universal property of EE gives RER\subseteq E (where \subset is given as Definition 4 on page 18.) and then it remains to prove that RER\subset E and ERE\subset R implies RER\cong E? Is the final step “proving RER\cong E” using the retractions and 11 is a generator? If so, I think I get it, but I think I did not use the fact the 11 is a generator to show the isomorphism. Thank you!

    • CommentRowNumber4.
    • CommentAuthorRichard Williamson
    • CommentTimeNov 15th 2020
    • (edited Nov 15th 2020)

    Yes, that is the kind of thing I had in mind. One has to be a bit careful with the details though; I will give what I think is a complete proof below, and I think we do need that 11 is a generator (see step 7)), and that ff admits a retraction, but in fact do not need that ee admits a retraction.

    1) By Axiom 1, an equaliser e:EA×Ae: E \rightarrow A \times A of qp 0q \circ p_{0} and qp 1q \circ p_{1} exists.

    2) By assumption (this is what it means to say that it is a subset), f:RA×Af: R \rightarrow A \times A is a monomorphism.

    3) Since ee is the equaliser of qp 0q \circ p_{0} and qp 1q \circ p_{1}, we have that qp 0e(x)=qp 1e(x)q \circ p_{0} \circ e(x) = q \circ p_{1} \circ e(x) for every xEx \in E. It follows from the \Rightarrow direction of the first sentence of the proof of Theorem 6 that, for every xEx \in E, there is an r xRr_{x} \in R such that f 0(r x)=p 0e(x)f_{0}(r_{x}) = p_{0} \circ e(x) and f 1(r x)=p 1e(x)f_{1}(r_{x}) = p_{1} \circ e(x), and hence (using the universal property of a product) such that f(r x)=e(x)f(r_{x}) = e(x).

    4) Since qq is the co-equaliser of f 0f_{0} and f 1f_{1}, we have that qp 0f=qp 1fq \circ p_{0} \circ f = q \circ p_{1} \circ f. By the universal property of ee, we deduce that there is a (unique, though we will not need this) map g:REg: R \rightarrow E such that eg=fe \circ g = f.

    5) In ETCS, we are assuming that ff admits a retraction (see after Definition 2 in Lawvere’s paper; Lawvere writes that a monomorphism is a retract, which is rather confusing terminology, since ’retract’ must then be understood in the opposite sense to ’retraction’, whereas I at least would consider it more natural to take those to be synonymous; anyhow, it is supposed to mean that a monomorphism is a section of some map, i.e. admits a retraction). Let us denote it by f 1f^{-1}.

    6) We have that ef 1eg=ef 1f=ee \circ f^{-1} \circ e \circ g = e \circ f^{-1} \circ f = e. By the universal property of an equaliser, we deduce that f 1eg=idf^{-1} \circ e \circ g = id.

    7) We have that egf 1e=ff 1ee \circ g \circ f^{-1} \circ e = f \circ f^{-1} \circ e. For any yEy \in E, we have, by 3), that ff 1e(y)=ff 1f(r y)=f(r y)=e(y)f \circ f^{-1} \circ e(y) = f \circ f^{-1} \circ f(r_{y}) = f(r_y) = e(y). Since 11 is a generator, we deduce that ff 1e=ef \circ f^{-1} \circ e = e, and hence that egf 1e=ee \circ g \circ f^{-1} \circ e = e. By the universal property of an equaliser, we deduce that gf 1e=idg \circ f^{-1} \circ e = id.

    8) We have established in 6) and 7) that gg has f 1ef^{-1} \circ e as a two-sided inverse, and thus is an isomorphism.

    9) By 8), the fact that ee is an equaliser, and the fact that eg=fe \circ g = f from 4), it follows immediately that ff is an equaliser.

    If you agree that this is all fine, we should add this to the ETCS entry, I suggest, since Lawvere’s assertion that this is ’clear’ is a bit of a stretch, in my opinion!

    • CommentRowNumber5.
    • CommentAuthorYimingXu
    • CommentTimeNov 17th 2020

    Thank you for writting down the whole argument! Yes, I think the proof is correct. I am a bit surprised that your argument does not use the fact that ee admits a retraction though. I have written another argument in a theorem prover yesterday, which seems to me are the same to yours in spirit. I used proposition 2 on page 18, which used the fact that 11 is the generator. By proposition 2, a 0q=a 1qa 0a 1a_0q = a_1q\implies a_0\equiv a_1 implies ERE\subseteq R, and also by proposition 2, the universal property of EE implies RER\subseteq E, and then we only require a lemma:

    For subobject a:AX,b:BXa: A \to X,b: B \to X, if aba\subseteq b and bab\subseteq a, then ABA\cong B.

    I expect the proof of this lemma is basically the same as your argument on step 6 and 7, but I did use both the retraction of aa and of bb!

    And yes, adding this to the ETCS entry will be great!

    • CommentRowNumber6.
    • CommentAuthorYimingXu
    • CommentTimeNov 17th 2020

    For the proof of the lemma, aba\subset b implies there is an h 1:ABh_1: A \to B such that bh 1=ab \circ h_1 = a by definition of inclusion of subsets, bab\subseteq a implies there is an h 2:BAh_2:B \to A such that b=ah 2b = a\circ h_2.

    Denote aa' be the retraction of aa and bb' the retraction of bb, then

    id A=aa=abh 1id_A = a' \circ a = a' \circ b \circ h_1

    But we have b=ah 2b = a \circ h_2, so aah 2=aba'\circ a \circ h_2 = a' \circ b, that is, h 2=abh_2 = a'\circ b.

    Therefore, we conclude id A=h 2h 1id_A = h_2 \circ h_1. By a symmetry argument (using bb') id B=h 1h 2id_B = h_1\circ h_2, that proves the lemma.