# Laver function

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Laver_function
> Markdown URL: https://mediated.wiki/source/Laver_function.md
> Source: https://en.wikipedia.org/wiki/Laver_function
> Source revision: 1234959927
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{short description|Mathematical function in set theory}}
In [set theory](/source/set_theory), a '''Laver function''' (or '''Laver diamond''', named after its inventor, [Richard Laver](/source/Richard_Laver)) is a function connected with [supercompact cardinal](/source/supercompact_cardinal)s.

==Definition==
If κ is a supercompact cardinal, a Laver function is a function ''ƒ'':κ&nbsp;→&nbsp;''V''<sub>κ</sub> such that for every set ''x'' and every cardinal λ&nbsp;≥&nbsp;|TC(''x'')|&nbsp;+&nbsp;κ there is a supercompact measure ''U'' on [λ]<sup><κ</sup> such that if ''j''<sub>&nbsp;''U''</sub> is the associated elementary embedding then ''j''<sub>&nbsp;''U''</sub>(''ƒ'')(κ) = ''x''. (Here ''V''<sub>κ</sub> denotes the κ-th level of the [cumulative hierarchy](/source/cumulative_hierarchy), TC(''x'') is the [transitive closure](/source/transitive_set) of ''x'')

==Applications==
The original application of Laver functions was the following theorem of Laver.   
If κ is supercompact, there is a κ-c.c. [forcing](/source/forcing_(mathematics)) notion (''P'',&nbsp;≤) such after forcing with (''P'',&nbsp;≤) 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](/source/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](/source/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}}

---
Adapted from the Wikipedia article [Laver function](https://en.wikipedia.org/wiki/Laver_function) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Laver_function?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.