# Exposition of concrete constructions

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?

• @Moderators: I think this qualifies as CW. Apr 11 at 17:47
• Somewhat similar discussion at mathoverflow.net/questions/323779/… and maybe also mathoverflow.net/questions/309191/… Apr 11 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. Apr 11 at 18:20

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.

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