8

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?

Martin Brandenburg
  • 61,443
  • @Moderators: I think this qualifies as CW. – Martin Brandenburg Apr 11 '21 at 17:47
  • 1
    Somewhat similar discussion at https://mathoverflow.net/questions/323779/what-is-an-explicit-bijection-in-combinatorics and maybe also https://mathoverflow.net/questions/309191/how-to-be-rigorous-about-combinatorial-algorithms – Sam Hopkins Apr 11 '21 at 17:49
  • 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. – Neil Strickland Apr 11 '21 at 18:20

1 Answers1

9

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.

Igor Khavkine
  • 20,710