-----
> [!proposition] Proposition. ([[going up]])
> Let $A \subset_{\iota} B$ be an [[integral algebra|integral extension]] of ([[commutative ring|commutative]]) [[ring|rings]]. Let $\mathfrak{p}_{1}, \mathfrak{p}_{2} \in \text{Spec }A$, $\mathfrak{p}_{1} \subset \mathfrak{p}_{2}$, and $\mathfrak{q} \in \text{Spec } B$, $\mathfrak{q}_{1} \cap A=\mathfrak{p}_{1}$. Then there is $\textcolor{thistle}{\mathfrak{q}_{2}} \in \text{Spec } B$ such that $\mathfrak{q}_{1} \subset \textcolor{thistle}{\mathfrak{q}_{2}}$ and $\textcolor{thistle}{\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] \arrow[r, "\textcolor{thistle}{\subset}" description, no head, dotted] & \textcolor{thistle}{\exists \mathfrak{q}_2} \arrow[d, no head, color=thistle] & \text{in Spec }B \\
> \mathfrak{p}_1 \arrow[r, "\subset" description, no head, dotted] & \mathfrak{p}_2 & \text{in Spec }A
> \end{tikzcd}
> \end{document}
> ```
>
> (In the diagram, $\mathfrak{q}_{1}$ is '[[lying over]]' $\mathfrak{p}_{1}$. The idea is that an inclusion $\mathfrak{p}_{1} \subset \mathfrak{p}_{2}$ in $\text{Spec }A$ induces an inclusion $\mathfrak{q}_{1} \subset \textcolor{thistle}{\mathfrak{q}_{2}}$ in $\text{Spec }B$ for some $\mathfrak{q}_{2}$ '[[lying over]]' $\mathfrak{p}_{2}$.)
> [!proof]- Proof. ([[going up]])
> Summary:
> 1. Consider the integral extension $A / \mathfrak{p}_{1} \hookrightarrow B / \mathfrak{q}_{1}$. Look at $\frac{\mathfrak{p}_{2}}{\mathfrak{p}_{1}} \in A / \mathfrak{p}_{1}$.
> 2. By [[lying over]], $\frac{\mathfrak{p}_{2}}{\mathfrak{p}_{1}}$ is contracted to by some $\frac{\mathfrak{q}_{2}}{\mathfrak{q}_{1}}$
> 3. Now draw the diagram below (and justify its existence) and use its commutativity to finish.
>
> Since $\mathfrak{p}_{1}=\mathfrak{q}_{1} \cap A$, the [[first isomorphism theorem]] gives a [[ring]] [[injection|embedding]] $A / \mathfrak{p}_{1} \hookrightarrow B / \mathfrak{q}_{1}$, and this is an [[integral algebra|integral extension]] by [[integral algebra|quotienting preserves integral extensions]].
>
> By [[lying over]], there exists $\frac{\mathfrak{q}_{2}}{\mathfrak{q}_{1}} \in \text{Spec }B /\mathfrak{q}_{1}$[^1] that contracts to $\frac{\mathfrak{p}_{2}}{\mathfrak{p}_{1}}$ in $A / \mathfrak{p}_{1}$, which in turn contracts to $\mathfrak{p}_{2}$ in $A$ (this is going uphill on $\downarrow _\to$ in the below diagram) . By commutativity of the diagram
>
> ```tikz
> \usepackage{tikz-cd}
> \usepackage{amsmath}
> \usepackage{amsfonts}
> \begin{document}
> % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBoBGAXVJADcBDAGwFcYkQBBAAgHouAdfgFt6OABYAzAE70A1sDQBfAPrkQi0uky58hFOQrU6TVuwBCvAcNGSZ8gI4q1GrdjwEiZYkYYs2iTnVNEAw3XSIDbxpfUwCzdSMYKABzeCJQaQghJAAmGhwIJABmfPosRnYxCAhZIIypLKQyEAKkAxayioCqmrqQTOzEPJbCxGaxGHoodhwAdwgJqYQXfobBkpG2mkXpgLmFyahlykUgA
> \begin{tikzcd}
> A \arrow[r, hook] \arrow[d, two heads] & B \arrow[d, two heads] \\
> A / \mathfrak{p}_1 \arrow[r, hook] & B / \mathfrak{q}_1
> \end{tikzcd}
> \end{document}
> ```
>
> (now going $^{\to}\downarrow$) this implies $\mathfrak{q}_{2} \cap A=\mathfrak{p}_{2}$, as required.
-----
####
[^1]: Any [[prime ideal]] in $\text{Spec }B / \mathfrak{q}_{1}$ may be unambiguously represented in such a form by [[the correspondence theorem for rings]].
----
#### 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
> ```