A transitive model M of ZFC is called a ground if the universe V is a set forcing extension of M. We show that the grounds ofV are downward set-directed. Consequently, we establish some fundamental theorems on the forcing method and the set-theoretic geology. For instance, the mantle, the intersection of all grounds, must be a model of ZFC. V has only set many grounds if and only if the mantle is a ground. We also show that if the universe (...) has some very large cardinal, then the mantle must be a ground. (shrink)

Assume. Let κ be a cardinal. A ‐ground is a transitive proper class W modelling such that V is a generic extension of W via a forcing of cardinality. The κ‐mantle is the intersection of all ‐grounds. We prove that certain partial choice principles in are the consequence of κ being inaccessible/weakly compact, and some other related facts.