Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeNov 13th 2020
   • (edited Nov 13th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexI am reading the following document about Lawvere's ETCS: http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf 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_1g$ in the link is a typo.) $a_0q = a_1q$ iff $a_0 \equiv a_1$. And finished the proof. That is, the author proves for every element $\langle a_0,a_1\rangle$ from the terminal object $1$, 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 $1$ is replaced by any arbitrary object. I know that $1$ is the generator in ETCS, and have trouble working out the proof that the existence of factorization for $1$ implies the existence of factorization for any $T$. I tried taking the elements of $T$, and unable to construct a factorization from $T$ 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: A \to B,g: B\to C$, then the author will write $fg$ to denote the composition of $f$ of $g$, rather than $g \circ f$.

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

   http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

   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 in the link is a typo.) iff .

   And finished the proof.

   That is, the author proves for every element from the terminal object , 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 is replaced by any arbitrary object. I know that is the generator in ETCS, and have trouble working out the proof that the existence of factorization for implies the existence of factorization for any . I tried taking the elements of , and unable to construct a factorization from 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 , then the author will write to denote the composition of of , rather than .

2. • CommentRowNumber2.
   • CommentAuthorRichard Williamson
   • CommentTimeNov 14th 2020
   • (edited Nov 14th 2020)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexInteresting 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 $f$; the other way around is obvious from the universal property of an equaliser. From this, it is I thimk straightforward (recalling that $f$ and the equaliser are monomorphisms and admit retractions), using the fact that $1$ is a generator, to deduce that $f$ 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.

   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 ; the other way around is obvious from the universal property of an equaliser. From this, it is I thimk straightforward (recalling that and the equaliser are monomorphisms and admit retractions), using the fact that is a generator, to deduce that 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.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeNov 14th 2020
   • (edited Nov 14th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks 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 $E \subset R$ ($E$ is the equalizer) and the universal property of $E$ gives $R\subseteq E$ (where $\subset$ is given as Definition 4 on page 18.) and then it remains to prove that $R\subset E$ and $E\subset R$ implies $R\cong E$? Is the final step "proving $R\cong E$" using the retractions and $1$ is a generator? If so, I think I get it, but I think I did not use the fact the $1$ is a generator to show the isomorphism. Thank you!

   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 ( is the equalizer) and the universal property of gives (where is given as Definition 4 on page 18.) and then it remains to prove that and implies ? Is the final step “proving ” using the retractions and is a generator? If so, I think I get it, but I think I did not use the fact the is a generator to show the isomorphism. Thank you!

4. • CommentRowNumber4.
   • CommentAuthorRichard Williamson
   • CommentTimeNov 15th 2020
   • (edited Nov 15th 2020)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexYes, 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 $1$ is a generator (see step 7)), and that $f$ admits a retraction, but in fact do not need that $e$ admits a retraction. 1) By Axiom 1, an equaliser $e: E \rightarrow A \times A$ of $q \circ p_{0}$ and $q \circ p_{1}$ exists. 2) By assumption (this is what it means to say that it is a subset), $f: R \rightarrow A \times A$ is a monomorphism. 3) Since $e$ is the equaliser of $q \circ p_{0}$ and $q \circ p_{1}$, we have that $q \circ p_{0} \circ e(x) = q \circ p_{1} \circ e(x)$ for every $x \in E$. It follows from the $\Rightarrow$ direction of the first sentence of the proof of Theorem 6 that, for every $x \in E$, there is an $r_{x} \in R$ such that $f_{0}(r_{x}) = p_{0} \circ e(x)$ and $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)$. 4) Since $q$ is the co-equaliser of $f_{0}$ and $f_{1}$, we have that $q \circ p_{0} \circ f = q \circ p_{1} \circ f$. By the universal property of $e$, we deduce that there is a (unique, though we will not need this) map $g: R \rightarrow E$ such that $e \circ g = f$. 5) In ETCS, we are assuming that $f$ 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^{-1}$. 6) We have that $e \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^{-1} \circ e \circ g = id$. 7) We have that $e \circ g \circ f^{-1} \circ e = f \circ f^{-1} \circ e$. For any $y \in E$, we have, by 3), that $f \circ f^{-1} \circ e(y) = f \circ f^{-1} \circ f(r_{y}) = f(r_y) = e(y)$. Since $1$ is a generator, we deduce that $f \circ f^{-1} \circ e = e$, and hence that $e \circ g \circ f^{-1} \circ e = e$. By the universal property of an equaliser, we deduce that $g \circ f^{-1} \circ e = id$. 8) We have established in 6) and 7) that $g$ has $f^{-1} \circ e$ as a two-sided inverse, and thus is an isomorphism. 9) By 8), the fact that $e$ is an equaliser, and the fact that $e \circ g = f$ from 4), it follows immediately that $f$ 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!

   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 is a generator (see step 7)), and that admits a retraction, but in fact do not need that admits a retraction.

   1) By Axiom 1, an equaliser of and exists.

   2) By assumption (this is what it means to say that it is a subset), is a monomorphism.

   3) Since is the equaliser of and , we have that for every . It follows from the direction of the first sentence of the proof of Theorem 6 that, for every , there is an such that and , and hence (using the universal property of a product) such that .

   4) Since is the co-equaliser of and , we have that . By the universal property of , we deduce that there is a (unique, though we will not need this) map such that .

   5) In ETCS, we are assuming that 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 .

   6) We have that . By the universal property of an equaliser, we deduce that .

   7) We have that . For any , we have, by 3), that . Since is a generator, we deduce that , and hence that . By the universal property of an equaliser, we deduce that .

   8) We have established in 6) and 7) that has as a two-sided inverse, and thus is an isomorphism.

   9) By 8), the fact that is an equaliser, and the fact that from 4), it follows immediately that 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!

5. • CommentRowNumber5.
   • CommentAuthorYimingXu
   • CommentTimeNov 17th 2020
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThank 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 $e$ 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 $1$ is the generator. By proposition 2, $a_0q = a_1q\implies a_0\equiv a_1$ implies $E\subseteq R$, and also by proposition 2, the universal property of $E$ implies $R\subseteq E$, and then we only require a lemma: For subobject $a: A \to X,b: B \to X$, if $a\subseteq b$ and $b\subseteq a$, then $A\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 $a$ and of $b$! And yes, adding this to the ETCS entry will be great!

   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 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 is the generator. By proposition 2, implies , and also by proposition 2, the universal property of implies , and then we only require a lemma:

   For subobject , if and , then .

   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 and of !

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

6. • CommentRowNumber6.
   • CommentAuthorYimingXu
   • CommentTimeNov 17th 2020
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexFor the proof of the lemma, $a\subset b$ implies there is an $h_1: A \to B$ such that $b \circ h_1 = a$ by definition of inclusion of subsets, $b\subseteq a$ implies there is an $h_2:B \to A$ such that $b = a\circ h_2$. Denote $a'$ be the retraction of $a$ and $b'$ the retraction of $b$, then $id_A = a' \circ a = a' \circ b \circ h_1$ But we have $b = a \circ h_2$, so $a'\circ a \circ h_2 = a' \circ b$, that is, $h_2 = a'\circ b$. Therefore, we conclude $id_A = h_2 \circ h_1$. By a symmetry argument (using $b'$) $id_B = h_1\circ h_2$, that proves the lemma.

   For the proof of the lemma, implies there is an such that by definition of inclusion of subsets, implies there is an such that .

   Denote be the retraction of and the retraction of , then

   But we have , so , that is, .

   Therefore, we conclude . By a symmetry argument (using ) , that proves the lemma.