The Easton-support product of higher Cohen forcings

Let $F$ be an Easton function (Easton functions on regular cardinals). A condition in the Easton-support product $P(F)$ is a function $p$ with values in $\{0,1\}$ whose domain is a set of triples $(\kappa ,\alpha ,\beta )$ with $\kappa \in \mathrm{dom}(F)$, $\alpha <\kappa$ and $\beta <F(\kappa )$, subject to the Easton support condition

$\mid \{(\kappa ,\alpha ,\beta )\in \mathrm{dom}(p):\kappa \le \gamma \}\mid <\gamma \text{for every infinite regular cardinal }\gamma \mathrm{.}$

Each coordinate $\kappa$ carries the Cohen order $\mathrm{Add}(\kappa ,F(\kappa ))=\mathrm{Fn}(F(\kappa )\times \kappa ,2,<\kappa )$ (Cohen, collapse, and Lévy-collapse forcing orders), so the fibre $p_{\kappa }(\alpha ,\beta )=p(\kappa ,\alpha ,\beta )$ is a partial function $\kappa \times F(\kappa )\to 2$ of domain size $<\kappa$. A condition $p$ is stronger than $q$, written $p\le q$, exactly when $p\supseteq q$: stronger conditions extend functions, and the empty function is the largest condition. When $\mathrm{dom}(F)$ is a set, $P(F)$ is a set; when $\mathrm{dom}(F)$ is a proper class, $P(F)$ is a proper class and its conditions are still sets. The support condition at $\gamma =\kappa$ gives $\mid \mathrm{dom}(p_{\kappa })\mid <\kappa$ for every $\kappa \in \mathrm{dom}(F)$.

For an infinite regular $\lambda$ (Cofinality $\mathrm{cf}(\alpha )$, and regular and singular cardinals), the initial segment and the tail are the restrictions

$p^{\le \lambda }=p\upharpoonright \{(\kappa ,\alpha ,\beta ):\kappa \le \lambda \},p^{>\lambda }=p\upharpoonright \{(\kappa ,\alpha ,\beta ):\kappa >\lambda \},$

with $P^{\le \lambda }=\{p^{\le \lambda }:p\in P(F)\}$ and $P^{>\lambda }=\{p^{>\lambda }:p\in P(F)\}$. Each condition splits uniquely into these two restrictions, and each restriction retains every support bound. Conversely, a head condition and a tail condition have disjoint domains, so their union is a function. For every infinite regular $\gamma$, its triples with $\kappa \le \gamma$ form the union of two sets each of cardinality below $\gamma$, which again has cardinality below $\gamma$. Thus union is the inverse of the map $p\mapsto (p^{\le \lambda },p^{>\lambda })$, and both maps preserve extension. This proves the isomorphism $P(F)\cong P^{\le \lambda }\times P^{>\lambda }$ of forcing orders. $P^{\le \lambda }$ is the Easton product of the fibres with $\kappa \le \lambda$, $P^{>\lambda }$ the Easton product of the fibres with $\kappa >\lambda$, and both split by first coordinate exactly as displayed.