## Summary

:::{.remark}
We summarize the lattices that will be relevant to our discussion:

$$\begin{aligned}
    \lkthree &= (22, 0, 0)_3 = U^3 \oplus E_8^2 = \rm{II}_{3, 19} &
    E_{10} &= (10, 0, 0)_1 = U \oplus E_8 = \mathrm{I}_{1, 9} \\
    S_{\En} &= (10, 10, 0)_1    = E_{10}(2) & 
    T_{\En} &= (12, 10, 0)_2    = U \oplus E_{10}(2) \\
    S_{\Co} &= (11, 11, 1)_1    = \gens{-2} \oplus E_{10}(2) & 
    T_{\Co} &= (11,11,1)_2      = \gens{2} \oplus E_{10}(2) \\
    S_{\dP} &= (2,2,0)_1        = U(2) &
    T_{\dP} &= (20, 2, 0)_2     = U \oplus U(2) \oplus E_8^2
\end{aligned}$$

:::

:::{.lemma}
\label{lem:embedding_eta}
Writing
\begin{align*}
T_{\Co} = \gens{2} \oplus E_{10}(2) &= \langle h, e', f',\alpha_1,\cdots, \alpha_8 \rangle \\
T_{\En} = U \oplus E_{10}(2) &= \langle \tilde e,\tilde f,\tilde e',\tilde f',\tilde \alpha_1,\cdots,\tilde \alpha_8\rangle,
\end{align*}
there is an embedding of lattices $T_{\Co} \injects T_{\En}$:
\begin{align*}
    \eta: \gens{2} \oplus E_{10}(2) &\to U \oplus E_{10}(2) \\
    (h, x) &\mapsto (\tilde e + \tilde f, x)
\end{align*}
which sends the generator $h$ of $\gens{2}$ to $\tilde e+\tilde f\in U$ and is the identity on the $E_{10}(2)$ summand. Since $\coker \eta$ is torsionfree, $\eta$ is a primitive embedding.
:::

:::{.lemma}
There is a sequence of primitive embeddings
\[
T_{\Co} \injects T_{\En} \injects T_{\dP} \injects \lkthree
\]  
which is unique up to $\Orth(\lkthree)$. In particular, this yields an embedding $T_{\Co}\injects T_{\dP}$ given by
\begin{align*}
    \gens{2} \oplus U(2) \oplus E_8(2) &\injects U \oplus U(2) \oplus E_8^2 \\
    (h,x,y) & \mapsto (\tilde e + \tilde f, x, y, y)
\end{align*}
and thus an embedding $F_{\Co} \injects F_{(2,2,0)}$.
:::

:::{.proof}
By \cite[Lem.\,2.4]{AEGS23}, it suffices to show uniqueness of $S_{\En} \injects S_{\Co}$, i.e.
\[
E_{10}(2) \injects \gens{-2}\oplus E_{10}(2)
,\]
or equivalently by untwisting,
\[
E_{10} \injects \gens{-1}\oplus E_{10}
.\]
This embedding is unique since one can write the codomain as $E_{10}^\perp \oplus E_{10}$. Similarly, by \cite[Cor.\,1.5.2, Thm.\,3.6.3]{nikulin1979integer-symmetric}, the homomorphism $\Orth(L)\to \Orth(T_{\Co})$ is surjective.
:::

:::{.lemma}
\label{lem:lattice-embeddings-induce-morphisms}
The embeddings of lattices $\eta: T_{\Co}\injects T_{\En}$ (resp. $T_{\Co} \injects T_{\dP}$) induce locally closed embedding $F_{\Co} \injects F_{\En}$ (resp. $F_{\Co} \injects F_{(2,2,0)}$) which extend to morphisms on the Baily-Borel compactifications.
:::

:::{.proof}
This follows from \cite[\S 5, Thm.\,2]{kiernan1972satake-compactification}.
:::

:::{.theorem}
$F_{\Co}$ is the normalization of a closed subvariety of $F_{\En}$.
:::

:::{.proof}
It suffices to show that $D(T_{\Co})/\Orth(T_{\Co}) \to D(T_{\En})/\Orth(T_{\En})$ is a finite morphism which is generically injective. 
The lattice embedding $T_{\Co}\injects T_{\En}$ induces an injective morphism $D(T_{\Co}) \injects D(T_{\En})$.
It remains to show that the stabilizer of $T_{\Co}$ in $\Orth(T_{\En})$ is precisely $\Orth(T_{\Co})$ and the morphism is finite.

This morphism is finite because...

The stabilizer statement follows from...


:::

\todo[inline]{I don't know how to prove this. Maybe one should embed into $T_{\dP}$ instead to get the stabilizer statement? Finiteness is still unclear. Maybe one can use finite $\iff$ proper and finite fibers, using Stacks tag 02LS. This can be checked Zariski locally?}

\todo[inline]{Maybe this can be proved using Zariski's main theorem: a birational morphism to a normal variety with finite fibers is an isomorphism onto an open subset. Is this morphism birational? What are the fibers, and how can we tell if they are finite?}