{{short description|Mathematical function in set theory}} In set theory, a '''Laver function''' (or '''Laver diamond''', named after its inventor, Richard Laver) is a function connected with supercompact cardinals.
==Definition== If κ is a supercompact cardinal, a Laver function is a function ''ƒ'':κ → ''V''<sub>κ</sub> such that for every set ''x'' and every cardinal λ ≥ |TC(''x'')| + κ there is a supercompact measure ''U'' on [λ]<sup><κ</sup> such that if ''j''<sub> ''U''</sub> is the associated elementary embedding then ''j''<sub> ''U''</sub>(''ƒ'')(κ) = ''x''. (Here ''V''<sub>κ</sub> denotes the κ-th level of the cumulative hierarchy, TC(''x'') is the transitive closure of ''x'')
==Applications== The original application of Laver functions was the following theorem of Laver. If κ is supercompact, there is a κ-c.c. forcing notion (''P'', ≤) such after forcing with (''P'', ≤) the following holds: κ is supercompact and remains supercompact after forcing with any κ-directed closed forcing.
There are many other applications, for example the proof of the consistency of the proper forcing axiom.
==References== {{refbegin}} *{{cite journal | zbl=0381.03039 | first=Richard | last=Laver | authorlink=Richard Laver | title=Making the supercompactness of κ indestructible under κ-directed closed forcing | journal=Israel Journal of Mathematics | volume=29 | year=1978 | issue=4 | pages=385–388 | doi=10.1007/bf02761175 | doi-access=}} {{refend}}
Category:Set theory Category:Large cardinals Category:Functions and mappings
{{settheory-stub}}