-----
> [!proposition] Proposition. ([[going down]])
> Let $A \subset B$ be an [[integral algebra|integral extension]] of [[integral domain|integral domains]], $A$ [[integral closure|integrally closed]] ([[field of fractions|in]] $\text{Frac }A$). Let $\mathfrak{p}_{1},\mathfrak{p}_{2} \in \text{Spec } A$, $\mathfrak{p}_{1} \supset \mathfrak{p}_{2}$, [[lying over|and]] $\mathfrak{q}_{1} \in \text{Spec } B$, $\mathfrak{q}_{1} \cap A=\mathfrak{p}_{1}$. Then there is $\mathfrak{q}_{2} \in \text{Spec } B$ such that $\mathfrak{q}_{1} \supset \mathfrak{q}_{2}$ and $\mathfrak{q}_{2} \cap A=\mathfrak{p}_{2}$.
>
> ```tikz
> \usepackage{tikz-cd}
> \usepackage{amsmath}
> \usepackage{amsfonts}
> \usepackage{xcolor}
>
> % Define the thistle color
> \definecolor{thistle}{RGB}{216,191,216}
>
> \begin{document}
> \begin{tikzcd}
> \mathfrak{q}_1 \arrow[d, no head] & \textcolor{thistle}{\exists \mathfrak{q}_2} \arrow[d, no head, color=thistle] \arrow[l, "\textcolor{thistle}{\supset}" description, no head, dotted] & \text{in Spec }B \\
> \mathfrak{p}_1 & \mathfrak{p}_2 \arrow[l, "\supset" description, no head, dotted] & \text{in Spec }A
> \end{tikzcd}
> \end{document}
> ```
>
>
> [!note] Note.
> Note that going down requires slightly stronger hypotheses than [[going up]], namely that $A,B$ are [[integral domain|integral domains]] and $A$ is [[integral closure|integrally closed]] (in $\text{Frac }A$). These assumptions are satisfied e.g. when applying [[Noether's normalization theorem]] to an [[integral domain]].
>
Having $A,B$ domains with $A$ integrally closed in $\text{Frac }A$ allows us to use the [[characterization of integrality over an ideal (in an integrally closed domain)]] in the proof.
> [!proof]- Proof. ([[going down]])
> We begin by successively rephrasing the goal (using only elementary considerations) until we obtain an actionable sufficiency to prove. At that point, the most important result we'll need is
>
> Consider the composite $A \hookrightarrow B \hookrightarrow B_{\mathfrak{q}_{1}}$ (injective because $B$ is an [[integral domain]]).
>
>
> *Want: to show $\mathfrak{p}_{2} \in \text{Spec }A$ is [[contraction of an ideal|contracted]] under the composite from some $\mathfrak{n} \in \text{Spec }B_{\mathfrak{q}_{1}}$, because then we can take $\mathfrak{q}_{2}:=\mathfrak{n} \cap B$ with $\mathfrak{q}_{2} \supset \mathfrak{q}_{1}$ to see $\underbrace{ \mathfrak{q}_{2} \cap A }_{ =\mathfrak{p}_{2}, \text{ by assump.} } \subset \underbrace{ \mathfrak{q}_{1} \cap A }_{ =\mathfrak{p}_{1} }$.*
>
> Recall the general statement about contracted ideals, that $\mathfrak{b}$ is contracted iff $\mathfrak{b}^{ec}=\mathfrak{b}$. So the goal is to show $\underbrace{ \overbrace{ \mathfrak{p}_{2}B_{\mathfrak{q}_{1}} }^{ \text{extend} } \cap A }_{ \text{contract} }=\mathfrak{p}_{2}$. Recalling that $\mathfrak{b}^{ec} \supset \mathfrak{b}$ always, it's enough to check "$\subset
quot;. Thus,
>
> *Want: $(\mathfrak{p}_{2}B_{\mathfrak{q}_{1}}) \cap A \subset \mathfrak{p}_{2}$.*
>
> The [[extension of an ideal|extension]] $\mathfrak{p}_{2}B_{\mathfrak{q}_{1}}$ takes place in two steps: $\mathfrak{p}_{2} \mapsto \mathfrak{p}_{2}B \mapsto \mathfrak{p}_{2}B_{\mathfrak{q}_{1}}$. Take $\frac{y}{s} \in (\mathfrak{p}_{2}B_{\mathfrak{q}_{1}}) \cap A$, $y \in \mathfrak{p}_{2}B$, $s \in B-\mathfrak{q}$.
>
> *Want: $\frac{y}{s} \in \mathfrak{p}_{2}$.* This is what we shall prove, by contradiction. First note:
>
>
> Since $B$ is [[integral element of an algebra|integral]] over $A$, the [[integral closure]] of $\mathfrak{p}_{2}$ in $B$ is $\sqrt{ \mathfrak{p}_{2}B }$ (see [[integrality over an ideal]]). Hence $y \in \mathfrak{p}_{2}B \subset \sqrt{ \mathfrak{p}_{2}B }$ is integral over $\mathfrak{p}_{2}$. Now can apply the [[characterization of integrality over an ideal (in an integrally closed domain)]]: $\frac{y}{1}$ is to be [[algebraic element|algebraic]] over $\text{Frac }A$, with the [[minimal polynomial|minimal equation]] of $y$ over $\text{Frac }A$ being $(*) \ y^{r}+u_{1}y^{r-1} + \dots + u_{n}y^{0}=0, \text{ for some } u_{i} \in \sqrt{ \mathfrak{p}_{2} }\overbrace{ = }^{ \mathfrak{p}_{2} \text{ prime} }\mathfrak{p}_{2}.$
> We can divide here. Write $\underbrace{ y }_{ \in B }=\frac{y}{\underbrace{ s }_{ \in A }}\underbrace{ s }_{ \in B }$ and so $y,s \in \text{Frac }B$ and $\frac{y}{s} \in \text{Frac }A$. Thus the minimal equation of $s$ over $\text{Frac }A$ is obtained by writing[^1] $\left( \frac{y}{s}s \right)^{r} + \underbrace{ u_{1} }_{ \in \mathfrak{p}_{2} }\left( \frac{y}{s} s \right)^{r-1} + \dots + \underbrace{ u_{r} }_{ \in \mathfrak{p}_{2} }=0$
> and dividing by $\ \left( \frac{y}{s} \right)^{r}$: $(* * ) \ s ^{r}+ \underbrace{ \left( \frac{s}{y} \right)^{1} }_{ \in \text{Frac }A } \underbrace{ u_{1} }_{ \in \mathfrak{p}_{2} } s ^{r-1} + \dots + \underbrace{ \left( \frac{s}{y} \right)^{r} }_{ \in \text{Frac }A } \underbrace{ u_{r} }_{ \in \mathfrak{p}_{2} }=0.$
> But $s \in B$, and so $s$ is integral over $A$, and thus [[characterization of integrality over an ideal (in an integrally closed domain)]] says all the coefficients $\left( \frac{s}{y} \right)^{1}\underbrace{ u_{1} }_{ \in \mathfrak{p}_{2} },\dots, \left( \frac{s}{y} \right)^{r}\underbrace{ u_{r} }_{ \in \mathfrak{p}_{2} }$ are in $A$.
>
> *Now,* suppose $\frac{y}{s} \notin \mathfrak{p}_{2}$. Then $\underbrace{ u_{i} }_{ \in \mathfrak{p}_2 }=\underbrace{ \left( \frac{y}{s} \right)^{i} }_{ \notin \mathfrak{p}_{2} } \underbrace{ \left( \frac{s}{y} \right)^{i}u_{i} }_{ \in A }$, and [[prime ideal|so]] $\left( \frac{s}{y} \right)^{i}u_{i} \in \mathfrak{p}_{2}$. Thus $s ^{r} \in \underbrace{ \mathfrak{p}_{2}B }_{ \subset \mathfrak{p}_{1}B = (\mathfrak{q}_{1} \cap A)B \subset \mathfrak{q}_{1} }$ by $(* *)$, a contradiction.
>
-----
####
[^1]: General fact — his notes explain in a footnote if not convinced.
----
#### References
> [!backlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM [[]]
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```