You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jean-Baptiste Vienney (Apr 22 2023 at 17:58):I have a logical situation that I think I have already encountered many times but I don't remember any other precise example.
I have an algebraic structure, let's call it a BGB. The definition of a BGB is constituted of two axioms: (1) compatibility (2) specialty.
It happens that every BGB is a GB and the definition of a GB comprises 3 axioms: (1) compatibility, (3) associativity, (4) coassociativity.
Thus the definition of BGB is equivalent to (1)+(2)+(3)+(4). It is a larger definition in the sense that (1)+(2) is syntactically strictly included in this definition.
A class of examples of BGB is constituted by the SA. It turns out that to prove that every SA is a BGB, the only method I know and maybe the easiest one is first to prove that every SA verifies (3) and (4) and then use it to prove that it also verifies (1) and (2). So, finally, in practice, to prove that an object is an SA I must first prove that it verifies (3) and (4) which seemed to be "consequences" of the short definition of BGB to finally be able to prove that it verifies the short definition, but by proving the biggest package (1)+(2)+(3)+(4) and not only (1)+(2) which is annoying because I wanted to be able to use the short definition in the examples too.
It seems to me that I have already encountered this schema many times: ie. when you need to prove that an example verifies consequences of a definition first to be able to prove that it verifies this definition. Do you have examples of this in your mind?
Note that when I say "consequence", "larger" etc. it is in a syntactic way and closer to the sense we use in the everyday life, for example when we think of causality. Reasoning only in term of truth is insufficient to explain these "logical" things that happen in the mathematical practice because you need something finer and more syntactic that for example the idea of equivalence which says that two things are equivalent if and only if each time one is true, then the other one is true.
Jean-Baptiste Vienney (Apr 22 2023 at 18:01):Jean-Baptiste Vienney said:
It seems to me that I have already encountered this schema many times: ie. when you need to prove that an example verifies consequences of a definition first to be able to prove that it verifies this definition. Do you have examples of this in your mind?
This paragraph is really my question.
Jean-Baptiste Vienney (Apr 22 2023 at 18:01):I hope it's clear.
Josselin Poiret (Apr 22 2023 at 18:29):it would probably help if you had a specific (or more than 1) example in mind
Jean-Baptiste Vienney (Apr 22 2023 at 18:33):The thing with the is an example but it's in something I'm writing. So I have a notion of binomial graded bialgebra. Associativity and coassociativity don't appear in the definition but each time I want to prove that something is a binomial graded bialgebra I first prove that it verifies the associativity and the coassociativity.
Jean-Baptiste Vienney (Apr 22 2023 at 18:35):I think I always encounter this. But I never remember the examples afterwards because you see this only when you do the proofs and you forget it afterwards.
Jean-Baptiste Vienney (Apr 22 2023 at 18:36):The only way to find another example for me is to do math and then one day suddenly find the same thing and then save it.
Jean-Baptiste Vienney (Apr 22 2023 at 18:43):I can try to provide exact definitions if you want but I'm not sure it will be super helpful because it's not well-known definitions.
Jean-Baptiste Vienney (Apr 22 2023 at 18:44):I was thinking to this stuff:
Abstract-CT2023.pdf
David Egolf (Apr 22 2023 at 18:50):Summarizing (hopefully) the above: we have that if a thing satisfies (1) and (2), then it satisfies (3) and (4).
But to show that a thing satisfies (1) and (2), it is easiest to start by showing it satisfies (3) and (4).
I guess for this to be the case there needs to be some tool available to us that makes it easier to prove that a thing satisfies (1) and (2) when we know that a thing satisfies (3) and (4).
Is that the idea?
Jean-Baptiste Vienney (Apr 22 2023 at 18:51):Yes exactly!
Jean-Baptiste Vienney (Apr 22 2023 at 18:52):Yes, (3) is associativity in the sense that a(bc) = (ab)c and (4) is coassociativity which is somewhat similar so they are very useful properties
Jean-Baptiste Vienney (Apr 22 2023 at 18:53):And it's easier in practice to first prove them to prove (1) and (2)
Jean-Baptiste Vienney (Apr 22 2023 at 19:04):I'm sure we have all encountered this situation several times but we just don't remember when
Jean-Baptiste Vienney (Apr 22 2023 at 20:06):(Well, I've checked if this automatic associativity and coassociativity also works for the special bialgebras in general ie. those such that (comultiplication followed by multiplication is the identity) but no, it works only with this graded definition (I guess, don't have any counterexample.). But I didn't want to speak of this particular thing.)