8
$\begingroup$

I am frequently interested to find less technical proofs of results which already appear in the literature, at least in some special cases of these results. Sometimes a published proof shows that an object with some properties exists, but actually the proof does not (at least not without additional work) construct that object in a concrete way. (Here object is understood to be in a very general sense, so functors for instance also qualify as objects.) Imagine for example a theorem stating that a certain functor is representable, and the proof uses some adjoint functor theorem: this does not really tell us much about the internal structure of a representing object, and it is often (not always) very useful to write down that representing object directly, including a direct proof that it actually represents the functor which also does not use much machinery.

I believe that it is worthwile to write down and maybe also publish a more direct, easy and constructive argument in case it is available and presumably not published so far. My question is basically how to fit this into the common "definition-theorem-proof" scheme of mathematical publications.

I cannot just have a theorem stating "There is an object with the property ...", since that existence statement is already known and I am actually more interested in the specific construction of that object. Another solution might be to put the construction of that object into a separate section, or a long definition, and then have a theorem stating "The object constructed above has the property ...". Another idea might be to find logical properties of a "concrete construction" which the published existence proof does not have; but I have to admit that this task is nontrivial for someone who is not an expert in mathematical logic, and it might become a bit artificial, and it might turn out that these logical properties actually already follow formally from the published proof. Basically, what I want is a theorem "There is an explicit construction of an object with the property ..." and give the construction in its proof, but the problem is that "explicit construction" is not a well-defined notion, as far as I know, so that it is unclear what qualifies as a proof of it.

Do you have other ideas or guidelines for a good exposition for a "concrete construction"? What are good examples of papers which have a good exposition of this type?

$\endgroup$
3
  • $\begingroup$ @Moderators: I think this qualifies as CW. $\endgroup$ Apr 11 at 17:47
  • 1
    $\begingroup$ Somewhat similar discussion at mathoverflow.net/questions/323779/… and maybe also mathoverflow.net/questions/309191/… $\endgroup$ Apr 11 at 17:49
  • $\begingroup$ Proof assistants give one answer to this. In Lean, for example, it is possible to use non-constructive axioms, but it is easy to check whether any given existence theorem has non-constructive dependencies, and if not then you can extract a witness. $\endgroup$ Apr 11 at 18:20
9
$\begingroup$

I think the following scheme is quite reasonable, which paraphrases your second option:

Def. Object X is...

Def. Property Y is...

Thm. Object X has Property Y.

Rmk. Object X is the first explicit example of Property Y.

You might need to put in quite a bit of effort to prove the Theorem, or to construct of X itself. Moreover, the Remark you are making is more about the state of the literature, rather than a formal statement, which is of course allowed in a remark. If you can also motivate why having an explicit example is important, the nontrivial mathematical content and the motivation make a perfectly reasonable recipe for a paper.

$\endgroup$
1
  • 8
    $\begingroup$ I find it somewhat amusing that this answer does not give a concrete example of this scheme :-) $\endgroup$ Apr 12 at 9:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.