Polarizations and the Mumford isogeny attached to an ample line bundle

Assume AC for the cited square theorem. Let $A$ be an abelian variety over a field $k$ (Abelian varieties over a field), and suppose a dual abelian variety $A^{\vee }$ with its universal normalized Poincare bundle $\mathcal{P}$ on $A{\times }_k{A}^{\vee }$ has been supplied (The rigidified relative Picard functor and the dual abelian variety).

For an invertible sheaf $\mathcal{L}$ on $A$ the Mumford morphism ${\phi }_{\mathcal{L}}:A\to A^{\vee }$ is the homomorphism of The theorem of the square and the Mumford homomorphism into the Picard group; it is represented by the family $\mathrm{\Lambda }(\mathcal{L})=m^{\ast }\mathcal{L}\otimes p_1^{\ast }{\mathcal{L}}^{-1}\otimes p_2^{\ast }{\mathcal{L}}^{-1}\otimes {\pi }^{\ast }{e}^{\ast }\mathcal{L}$ on $A{\times }_{k}A$, rigidified along both identity factors, where $m:A{\times }_{k}A\to A$ is the group law, $p_1,p_2$ are the projections, $\pi :A{\times }_{k}A\to \mathrm{Spec}k$ is the structure morphism for the constant factor, and $e$ is the identity section; in particular $({\mathrm{id}}_A\times {\phi }_{\mathcal{L}}{)}^{\ast }\mathcal{P}\cong \mathrm{\Lambda }(\mathcal{L})$, and the map used here has domain $A{\times }_{k}A$.

A polarization of $A$ is a homomorphism $\lambda :A\to A^{\vee }$ such that, after extension of scalars to an algebraic closure of $k$, there exists an ample invertible sheaf $\mathcal{L}$ on $A_{\bar{k}}$ (Absolute ampleness by affine section opens) with ${\lambda }_{\bar{k}}={\phi }_{\mathcal{L}}$. A principal polarization is a polarization of degree one, where the degree of a polarization is the finite locally free rank of the associated isogeny, once $\lambda$ is known to be an isogeny.

This definition is conditional on the supply of the dual and the Poincare bundle; symmetry $\lambda ={\lambda }^{\vee }$ under the bidual identification, finiteness and the isogeny property, existence of the dual, and existence and square degree of polarizations are conclusions to be proved in the subsequent commissioned theorem and are not assumed as existence assertions here. Defining these conditional terms does not create a dependency from this definition back to that theorem.