User beroal - MathOverflow

a limit of $\operatorname{id}$

2011-10-15T18:02:37Z

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.

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 catamorphisms (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$.

Do Arbib and Manes describe just concrete categories?

2011-09-13T13:45:58Z

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 set of structures on a set $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 admissible functions $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.

If I am on the right track, what do other parts of Arbib, Manes's theory (e.g. optimal lifts) correspond to?

(Please add the tag “concrete-category” to this question.)

Answer by beroal for What is the theory of polynomials?

2011-08-27T16:14:51Z

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.”

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

for every object $R$ in RingCat (= for every ring $R$) there is an initial object in the category $select(R)\downarrow U$ (comma category),

where $U$ is the forgetful functor.

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).

a “self-dual” adjunction

2011-07-14T18:13:37Z

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.

Is there a category with a subobject classifier but which is not finitely complete?

2011-02-19T04:03:37Z

This is a reverse of the question “Is there a finitely complete category with terminal object but NO subobject classifier?” From “An informal introduction to topos theory” by Tom Leinster I learned that there is 3 definitions of a subobject classifier in some category C:

where we directly work with morphisms of C: for every monomorphism there exists a characteristic morphism etc.;
a terminal object in the category of monomorphisms and pullback squares;
the functor Sub is representable.

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).)

motivation of filtered colimits

2011-01-27T23:01:50Z

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 variety to a Lawvere theory is pretty clear for me. The link (varieties ↦ Lawvere theories) is clear in some elementary operations, like

mapping an algebra by some functor F ↦ postcomposing F;
underlying functor ↦ precomposition of a functor between Lawvere theories.

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 mentioning varieties. Why the definition of a filtered colimit 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?

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.)

Answer by beroal for Abstract nonsense attribution

2011-01-27T10:52:32Z

$G(S):= \lbrace y\in Y | \forall x\in S. xRy \rbrace$

$F(T):= \lbrace x\in X | \forall y\in T. xRy \rbrace$

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.”

[solved] sequent calculus as programming language

2010-06-26T05:31:17Z

intuitionistic logic ~ programming

natural deduction ~ lambda-calculus

Hilbert system ~ combinatory logic {S, K}

Gentzen system=sequent calculus ~ ?

What would you write in place of the question mark?

Update 0: Common mathematical tree notation for proofs is too cumbersome and redundant. I need a language as compact as e.g.:

data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -}

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.

Comment by beroal

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.

Comment by beroal

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?

Comment by beroal

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.

Comment by beroal

2011-09-16T18:18:10Z

@Qiaochu Yuan: Thanks, I did not know that. I have removed “ct.”.

Comment by beroal

2011-08-28T10:36:49Z

@Todd Trimble: BTW, Emil's answer would be great if I could understand it. :)

Comment by beroal

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. :)

Comment by beroal

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.

Comment by beroal

2011-07-16T10:37:57Z

@Finn Lawler: $I$ is a morphism between categories, i.e. a functor.

Comment by beroal

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.

Comment by beroal

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.

Comment by beroal

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.

Comment by beroal

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.

Comment by beroal

2011-01-29T08:35:13Z

Your edit of your comment is sufficient.

Comment by beroal

2011-01-29T08:11:44Z

@Tom Leinster: I will add it when I will standing on a firm ground.

Comment by beroal

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?