[proofplan]
Choose the given Kähler form $\omega$ as a closed positive real $(1,1)$-form representative of the class $[\omega]$. The pullback of differential forms commutes with the [exterior derivative](/theorems/1525), so $f^*\omega$ is closed and represents the cohomological pullback $f^*[\omega]$. Holomorphicity gives $df_x\circ J_X=J_Y\circ df_x$, which proves that the pullback form has type $(1,1)$ and lets us test semipositivity by evaluating $\omega$ on the vector $df_x(v)$ and its $J_Y$-rotation. The possible vanishing of $df_x(v)$ is exactly why the pulled-back form is semipositive rather than necessarily positive.
[/proofplan]
[step:Choose a Kähler representative of the class]
Since $\omega$ is a Kähler form on $Y$, it is a smooth real closed positive $(1,1)$-form. Its de Rham cohomology class is the given class
\begin{align*}
[\omega]\in H^{1,1}(Y)\cap H^2(Y,\mathbb R).
\end{align*}
We will prove that the smooth pullback form $f^*\omega$ has the asserted properties on $X$.
[/step]
[step:Show that the pulled-back form is closed and represents the pulled-back cohomology class]
The exterior derivative is natural with respect to smooth pullback, so
\begin{align*}
d(f^*\omega)=f^*(d\omega).
\end{align*}
Since $\omega$ is closed, $d\omega=0$, hence
\begin{align*}
d(f^*\omega)=0.
\end{align*}
Therefore $f^*\omega$ is a closed real two-form on $X$, and by the definition of the induced map on de Rham cohomology it represents
\begin{align*}
[f^*\omega]=f^*[\omega]\in H^2(X,\mathbb R).
\end{align*}
The compactness and Kähler hypotheses on $X$ ensure that the compact Kähler [Hodge decomposition](/theorems/2745) applies to $X$ [citetheorem:8066]. Thus, once we verify that the representative $f^*\omega$ has type $(1,1)$, this real de Rham class is an element of $H^{1,1}(X)\cap H^2(X,\mathbb R)$.
[/step]
[step:Use holomorphicity to preserve type and reality]
For each $x\in X$, let
\begin{align*}
df_x:T_xX\to T_{f(x)}Y
\end{align*}
denote the differential of $f$ at $x$. Since $f$ is holomorphic, its differential is complex-linear:
\begin{align*}
df_x(J_Xv)=J_Ydf_x(v)
\end{align*}
for every $x\in X$ and every $v\in T_xX$.
Let $x\in X$ and let $u,v\in T_xX$. Because $\omega$ has type $(1,1)$ as a real two-form on $Y$, it satisfies
\begin{align*}
\omega_{f(x)}(J_Ya,J_Yb)=\omega_{f(x)}(a,b)
\end{align*}
for all $a,b\in T_{f(x)}Y$. Using the definition of pullback and the complex-linearity of $df_x$, we obtain
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(df_x(J_Xu),df_x(J_Xv)).
\end{align*}
Thus
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(J_Ydf_x(u),J_Ydf_x(v)).
\end{align*}
Since $\omega$ has type $(1,1)$,
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(df_x(u),df_x(v))=(f^*\omega)_x(u,v).
\end{align*}
Hence $f^*\omega$ has type $(1,1)$ on $X$. Since $\omega$ is real and pullback commutes with complex conjugation on differential forms, $f^*\omega$ is real. Therefore
\begin{align*}
f^*\omega\in A^{1,1}(X)
\end{align*}
as a real form. Combining this type computation with the closedness proved above and the compact Kähler [Hodge decomposition](/theorems/3941) on $X$ [citetheorem:8066], its class lies in $H^{1,1}(X)\cap H^2(X,\mathbb R)$.
[guided]
The point of this step is to convert holomorphicity of $f$ into a statement about the type decomposition of forms. For each $x\in X$, the differential of $f$ is the real-[linear map](/page/Linear%20Map)
\begin{align*}
df_x:T_xX\to T_{f(x)}Y.
\end{align*}
Because $f$ is holomorphic, this real-linear map is compatible with the two complex structures:
\begin{align*}
df_x(J_Xv)=J_Ydf_x(v)
\end{align*}
for every $v\in T_xX$.
Now fix $x\in X$ and tangent vectors $u,v\in T_xX$. The pullback form is defined by inserting the pushed-forward tangent vectors into $\omega$:
\begin{align*}
(f^*\omega)_x(u,v)=\omega_{f(x)}(df_x(u),df_x(v)).
\end{align*}
To check that $f^*\omega$ has type $(1,1)$ as a real two-form, we test invariance under applying $J_X$ to both arguments. Using the definition of pullback gives
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(df_x(J_Xu),df_x(J_Xv)).
\end{align*}
Holomorphicity replaces each occurrence of $df_x(J_X\cdot)$ by $J_Ydf_x(\cdot)$, so
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(J_Ydf_x(u),J_Ydf_x(v)).
\end{align*}
Since $\omega$ is a real $(1,1)$-form on $Y$, it satisfies
\begin{align*}
\omega_{f(x)}(J_Ya,J_Yb)=\omega_{f(x)}(a,b)
\end{align*}
for all $a,b\in T_{f(x)}Y$. Applying this with $a=df_x(u)$ and $b=df_x(v)$ gives
\begin{align*}
(f^*\omega)_x(J_Xu,J_Xv)=\omega_{f(x)}(df_x(u),df_x(v)).
\end{align*}
By the definition of pullback, the right-hand side is
\begin{align*}
(f^*\omega)_x(u,v).
\end{align*}
Therefore $f^*\omega$ has type $(1,1)$.
Reality is also preserved under pullback: since $\omega$ takes real values on real tangent vectors, the form $f^*\omega$ takes real values on real tangent vectors. Hence $f^*\omega$ is a real $(1,1)$-form on $X$. Together with the closedness already proved, the compact Kähler Hodge decomposition on $X$ [citetheorem:8066] identifies the de Rham class of this closed real $(1,1)$-form as an element of
\begin{align*}
H^{1,1}(X)\cap H^2(X,\mathbb R).
\end{align*}
[/guided]
[/step]
[step:Verify semipositivity by evaluating on complex lines]
Let $x\in X$ and $v\in T_xX$. Using the definition of pullback and holomorphicity of $f$, we compute
\begin{align*}
(f^*\omega)_x(v,J_Xv)=\omega_{f(x)}(df_x(v),df_x(J_Xv)).
\end{align*}
Since $df_x(J_Xv)=J_Ydf_x(v)$, this becomes
\begin{align*}
(f^*\omega)_x(v,J_Xv)=\omega_{f(x)}(df_x(v),J_Ydf_x(v)).
\end{align*}
The form $\omega$ is positive because it is Kähler, so for every $w\in T_{f(x)}Y$,
\begin{align*}
\omega_{f(x)}(w,J_Yw)\geq 0.
\end{align*}
Applying this with $w=df_x(v)$ gives
\begin{align*}
(f^*\omega)_x(v,J_Xv)\geq 0.
\end{align*}
Thus $f^*\omega$ is semipositive. Combining this with closedness, reality, and type $(1,1)$ proves that $f^*[\omega]$ is represented by the closed semipositive real $(1,1)$-form $f^*\omega$.
[/step]
