User beroal - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T14:46:31Z http://mathoverflow.net/feeds/user/7093 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/78216/a-limit-of-operatornameid a limit of $\operatorname{id}$ beroal 2011-10-15T18:02:37Z 2011-10-17T14:12:30Z <p>In the title, $\operatorname{id}$ is a functor. Or $\operatorname{id}(C)$, to explicitely write a category $C$. So, a limit of all objects and morphisms in $C$. I am in doubt, is it proper to take such a big limit? Below I explain that $C$ in the motivating example is the category of algebras which usually is infinite. The question resides above, but if you can tell me something about the motivating example, you are welcome.</p> <p>I found a proof that if such a limit exists, it is an initial object in $C$. The apex of the limit is an initial object and the morphisms of the limit are <a href="http://en.wikipedia.org/wiki/Catamorphism" rel="nofollow">catamorphisms</a> (this is just a special name for that unique morphism that goes from any initial object). This occurs in programming. $C$ is the category of algebras, the limit $L$ of $\operatorname{id}(C)$ is a set (?) where every element is a function that picks for every algebra an element of the carrier of that algebra. Intuitively, the function folds hidden something by a given algebra. Sometimes it's desirable to keep this function rather then an element of some initial algebra $0$. We go from any element $x$ of $0$ to the element of $L$ by feeding $x$ to morphisms of $L$. We go from any element $y$ of $L$ to the element of $0$ by picking the component of $y$ that corresponds to $0$.</p> http://mathoverflow.net/questions/75312/do-arbib-and-manes-describe-just-concrete-categories Do Arbib and Manes describe just concrete categories? beroal 2011-09-13T13:45:58Z 2011-09-16T18:16:09Z <p>In “Arbib, Manes. Arrows, Structures and Functors. The Categorical Imperative. 6. Structured sets.” there is an approach to formalize structures. I have a strong feeling that they describe just concrete categories in other words. For a concrete category $(C, U)$, the <strong>set of structures on a set</strong> $X$ (this is Arbib, Manes's term) is $(fr\_ob(U))^{-1}(X)$ where $fr\_ob(U)$ is a mapping of $U$ on objects. Similarly, the set of <strong>admissible functions</strong> $A\to B$ (for $A\ B\in ob(C)$) is $im(fr\_hom(U)(A, B))$ where $fr\_hom(U)$ is a mapping of $U$ on morphisms.</p> <p>If I am on the right track, what do other parts of Arbib, Manes's theory (e.g. optimal lifts) correspond to?</p> <p>(Please add the tag “concrete-category” to this question.)</p> http://mathoverflow.net/questions/73664/what-is-the-theory-of-polynomials/73852#73852 Answer by beroal for What is the theory of polynomials? beroal 2011-08-27T16:14:51Z 2011-08-28T10:09:47Z <p>IMHO the answer to “where polynomials are initial” (not to the title question, which is too broad for me) is already given in “Awodey. Category theory. 9. Adjoints. 9.3. Examples of adjoints. Example 9.10.”</p> <p>In that example, the adjunction of functors is constructed, where its free (left adjoint) functor $F$ goes from the category of rings (=RingCat) to the category of rings with distinguished element (= pointed rings). If we define this adjunction via unit ($\eta$), then the definition says that</p> <blockquote> <p>for every object $R$ in RingCat (= for every ring $R$) there is an <strong>initial</strong> object in the category $select(R)\downarrow U$ (comma category),</p> </blockquote> <p>where $U$ is the forgetful functor.</p> <p>Furthermore, a chosen initial object for $R$ consists of $F(R)$ (= $R[x]$) and $\eta(R):R\to U(F(R))$ (= a ring homomorphism constructing constant polynomials). The distinguished element in $F(R)$ is “$x$” (the projection polynomial).</p> http://mathoverflow.net/questions/70361/a-self-dual-adjunction a “self-dual” adjunction beroal 2011-07-14T18:13:37Z 2011-07-14T19:24:54Z <p>Is there a name for $(U,\eta)$ such that $(\eta, \eta^{op}):U^{op}\dashv U$ (is an adjunction). To clarify — $C:category$, $(I,I^{op})$ is the contravariant isomorphism with $I:C^{op}\to C$, $U:C^{op}\to C,\ U^{op}:=I^{op}\circ U\circ I^{op},\ U^{op}:C\to C^{op}$, $\eta:id(C)\to U\circ U^{op},\ \eta^{op}:= I^{op}\eta I,\ \eta^{op}:U^{op}\circ U\to id(C^{op})$. E.g. in CCC, contravariant exponential functor and $\eta(a):=\lambda(x:a) f.f\ x$ is such an adjunction.</p> http://mathoverflow.net/questions/55955/is-there-a-category-with-a-subobject-classifier-but-which-is-not-finitely-complet Is there a category with a subobject classifier but which is not finitely complete? beroal 2011-02-19T04:03:37Z 2011-02-19T05:30:16Z <p>This is a reverse of the question <a href="http://mathoverflow.net/questions/14815/is-there-a-finitely-complete-category-with-terminal-object-but-no-subobject-class" rel="nofollow">“Is there a finitely complete category with terminal object but NO subobject classifier?”</a> From <a href="http://arxiv.org/abs/1012.5647" rel="nofollow">“An informal introduction to topos theory”</a> by Tom Leinster I learned that there is 3 definitions of a subobject classifier in some category C:</p> <ol> <li>where we directly work with morphisms of C: for every monomorphism there exists a characteristic morphism etc.;</li> <li>a terminal object in the category of monomorphisms and pullback squares;</li> <li>the functor Sub is representable.</li> </ol> <p>In order to make sense of (3) we need Sub which is defined via pullbacks in C. (3) requires C to have pullbacks. But (1) and (2) do not, though they imply existence of the terminal object. Is there a category with a subobject classifier and which is not finitely complete? (AFAIK subobject classifier → terminal object → (have pullbacks ↔ have finite limits = is finitely complete).)</p> http://mathoverflow.net/questions/53548/motivation-of-filtered-colimits motivation of filtered colimits beroal 2011-01-27T23:01:50Z 2011-01-29T08:33:53Z <p>I am trying to move in categorical algebra beyond the basics. A Lawvere theory L is a small category with finite products. (I know that there also is a functor $(skeleton(FinSet))^{op}\to L$, which restricts a number of sorts in the algebraic theory to 1. Lets drop that requirement for now.) How to convert some <a href="http://en.wikipedia.org/wiki/Variety_(universal_algebra)" rel="nofollow">variety</a> to a Lawvere theory is pretty clear for me. The link (varieties ↦ Lawvere theories) is clear in some elementary operations, like</p> <ul> <li>mapping an algebra by some functor F ↦ postcomposing F;</li> <li>underlying functor ↦ precomposition of a functor between Lawvere theories.</li> </ul> <p>Then filtered colimits come. Lets take for reference “Adámek. a categorical introduction to general algebra.” Chapter 2 “Sifted and filtered colimits” and chapter 3 “Reflixive coequalizers” are devoid of <strong>mentioning varieties</strong>. Why <a href="http://en.wikipedia.org/wiki/Filtered_colimit" rel="nofollow">the definition of a filtered colimit</a> is such? I suppose there should be more concrete explanations involving algebraic operations, this is called “algebra” after all. Google suggests few texts on this subject, but they are abstract too. Any references?</p> <p>The claim “an arbitrary algebra is a filtered colimit of finitely generated algebras” is needed to construct the left adjoint to an underlying functor. Can anyone refer me to its proof? (Update 2011-01-29. Also I want a precise proof constructing that left adjoint.) (Update 2011-01-29. Thank you all for insightful answers and comments. I suspect that there is no direct link between filtered colimits and traditional algebra, i.e. it is an abstract thing that is needed for another abstract thing… I need to think it through to formulate further questions.)</p> http://mathoverflow.net/questions/53022/abstract-nonsense-attribution/53480#53480 Answer by beroal for Abstract nonsense attribution beroal 2011-01-27T10:52:32Z 2011-01-27T11:04:53Z <p>$G(S):= \lbrace y\in Y | \forall x\in S. xRy \rbrace$</p> <p>$F(T):= \lbrace x\in X | \forall y\in T. xRy \rbrace$</p> <p>This Galois connection is called “polarities” in “M. Erne, J. Koslowski, A. Melton, G. E. Strecker. A Primer on Galois Connections.” and the relation-generated Galois connection in “Smith. The Galois Connection between Syntax and Semantics.”</p> http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language [solved] sequent calculus as programming language beroal 2010-06-26T05:31:17Z 2010-07-30T08:10:25Z <p>intuitionistic logic ~ programming</p> <p>natural deduction ~ lambda-calculus</p> <p>Hilbert system ~ combinatory logic {S, K}</p> <p>Gentzen system=sequent calculus ~ ?</p> <p>What would you write in place of the question mark?</p> <p>Update 0: Common mathematical tree notation for proofs is too cumbersome and redundant. I need a language as compact as e.g.:</p> <p><code> data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -} </code></p> <p>Update 1: After following the links suggested by commentators I found this perfectly concrete and accessible article: "Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure." There, "?" language is named "the usual interpretation of LJ cut-free proofs by normal lambda-terms", i.e. is made out of lambda-calculus.</p> http://mathoverflow.net/questions/24220/why-is-it-so-difficult-to-write-complete-computer-verifiable-proofs/24284#24284 Comment by beroal beroal 2012-07-21T18:35:05Z 2012-07-21T18:35:05Z “These linear scripts are unreadable unless replayed step-by-step in the proof assistant.” +1. Elementary tactics killed readability in Coq. Not to mention that you must learn dozens (hundreds?) little tactics. Lambda-calculus is shorter. However, advanced tactics, like “ring”, are useful. http://mathoverflow.net/questions/78216/a-limit-of-operatornameid Comment by beroal beroal 2011-10-17T14:06:45Z 2011-10-17T14:06:45Z @Charles Rezk: You say that if $C$ has an initial object $0$, then $0$ is a limit of $\operatorname{id}(C)$? I could not prove this, can you hint me? http://mathoverflow.net/questions/78216/a-limit-of-operatornameid Comment by beroal beroal 2011-10-17T14:04:44Z 2011-10-17T14:04:44Z @S. Carnahan: Yes, you are right. Usually I ignore foundations and call everything a “set.” $C$ is the category of algebras, so it is usually infinite. The second paragraph gives additional info (perhaps it will be relevant) and motivation. I do not like questions without motivation. http://mathoverflow.net/questions/75312/do-arbib-and-manes-describe-just-concrete-categories Comment by beroal beroal 2011-09-16T18:18:10Z 2011-09-16T18:18:10Z @Qiaochu Yuan: Thanks, I did not know that. I have removed “ct.”. http://mathoverflow.net/questions/73664/what-is-the-theory-of-polynomials/73852#73852 Comment by beroal beroal 2011-08-28T10:36:49Z 2011-08-28T10:36:49Z @Todd Trimble: BTW, Emil's answer would be great if I could understand it. :) http://mathoverflow.net/questions/73664/what-is-the-theory-of-polynomials/73852#73852 Comment by beroal beroal 2011-08-28T10:31:46Z 2011-08-28T10:31:46Z @Todd Trimble: Not so slightly. Emil does not mention any adjunction, and I do not mention atomic=positive diagrams and associative algebras. I posted my answer because I could not follow Emil's answer because of a couple of unfamiliar terms. (Never heard of atomic=positive diagrams before. Now I see they are probably related to $\eta(R)$, though do not see how until I find the precise definition.) And I gave the reference. It is always good to know your predecessors and not to reinvent the wheel. :) http://mathoverflow.net/questions/70361/a-self-dual-adjunction/70366#70366 Comment by beroal beroal 2011-07-16T10:43:06Z 2011-07-16T10:43:06Z @Finn Lawler: Thanks, that is exactly what I was looking for. The power-object functor is a particular case of contravariant exponential functors. Contravariant exponential functors lead to the continuation monad. I will probably stick to MacLane's term. http://mathoverflow.net/questions/70361/a-self-dual-adjunction/70366#70366 Comment by beroal beroal 2011-07-16T10:37:57Z 2011-07-16T10:37:57Z @Finn Lawler: $I$ is a morphism between categories, i.e. a functor. http://mathoverflow.net/questions/55458/writing-semi-formal-proofs Comment by beroal beroal 2011-05-24T10:37:30Z 2011-05-24T10:37:30Z “He seemed skeptical that anyone would actually prefer symbols to English.” I prefer symbols to English. You are not alone. I write proofs for myself with Fitch diagrams. For myself because it is hard to post pictures on forums and IMHO not so many people understand that notation anyway. http://mathoverflow.net/questions/19152/why-is-a-topology-made-up-of-open-sets/19173#19173 Comment by beroal beroal 2011-02-19T14:51:58Z 2011-02-19T14:51:58Z @Vectornaut: There is a short answer by @Mike Benfield, which goes in parallel with mine. It seems that this point of view is not popular. If you have any further info, especially rigorously developed, I will be glad to hear that. http://mathoverflow.net/questions/19152/why-is-a-topology-made-up-of-open-sets/19173#19173 Comment by beroal beroal 2011-02-19T14:37:31Z 2011-02-19T14:37:31Z @Vectornaut: Your definition of a continuous map is a nice formalization of informal “a map without breaks” or “a map which preserves infinitesimal distances”. a touches A ↔ a is infinitely close to A. Infinitesimal distance between points does not make sense, so we need to replace one of the points with a set. That was crucial. I went the same way, but directly from the Kuratowski's axioms. a touches A ↔ $a\in cl(A)$. Thank you very much for the references because I did not know even where to start my search or what name it is called. I wonder why point-set topology is not derived this way. http://mathoverflow.net/questions/41563/teaching-proofs-in-the-era-of-google Comment by beroal beroal 2011-02-19T10:13:41Z 2011-02-19T10:13:41Z @Ryan Budney: Nobody can deny technology, everybody ought to accustom to it. Alex Bartel's answer seems like a solution to me. Novel questions, open problems force people to work in the real world. http://mathoverflow.net/questions/53548/motivation-of-filtered-colimits/53556#53556 Comment by beroal beroal 2011-01-29T08:35:13Z 2011-01-29T08:35:13Z Your edit of your comment is sufficient. http://mathoverflow.net/questions/53548/motivation-of-filtered-colimits/53575#53575 Comment by beroal beroal 2011-01-29T08:11:44Z 2011-01-29T08:11:44Z @Tom Leinster: I will add it when I will standing on a firm ground. http://mathoverflow.net/questions/53548/motivation-of-filtered-colimits/53575#53575 Comment by beroal beroal 2011-01-29T08:06:53Z 2011-01-29T08:06:53Z @David Roberts: Sorry, that was a stupid question. :) Further stupid question, is this “commuting” feature used in some proof other than construction of a free functors for in the context of Lawvere theories?