-----
> [!proposition] Proposition. ([[integral extensions are zero-dimensional]])
> Let $A \subset B$ be an [[integral algebra|integral extension]]. Then their [[Krull dimension|dimensions]] agree: $\text{dim }A=\text{dim }B.$ If the extension is in fact of $k$-[[algebra|algebras]], with $A,B$ [[integral domain|integral domains]] and $k$ some [[field]], then the [[transcendence basis|transcendence degrees]] agree: $\text{trdeg}_{k}A=\text{trdeg}_{k}B$
^proposition
> [!proof]- Proof. ([[integral extensions are zero-dimensional]])
>
> Summary:
> 1. Draw a picture with $\text{Spec }B$ hanging over $\text{Spec }A$.
> 2. Using [[lying over]] and [[going up]] to show $\text{dim }A \leq \text{dim }B$
> 3. To show $\text{dim }B \geq \text{dim }A$, just push a chain in $B$ through $\iota^{*}$. [[Incomparability]] guarantees that it will yield a chain in $A$.
>
> **$\text{dim }A \leq \text{dim }B.$**
>
> Take a chain $\mathfrak{p}_{0} \subsetneq \dots \subsetneq \mathfrak{p}_{d}, \mathfrak{p}_{i} \in \text{Spec }A, d \geq 0.$
> By [[lying over]] and [[going up]], there are $\mathfrak{q}_{1} \subset \dots \subset \mathfrak{q}_{d}$, $\mathfrak{q}_{i} \in \text{Spec }B$, such that $\mathfrak{q}_{i} \cap A=\mathfrak{p}_{i}$. We must have $\mathfrak{q}_{i} \neq \mathfrak{q}_{i+1}$ because $\mathfrak{p}_{i} \neq \mathfrak{p}_{i+1}$. Thus $\text{dim }B \geq d$, thus $\text{dim }B \geq \text{dim }A$ since $d$ was arbitrary.
>
> **$\text{dim }B \leq \text{dim }A$.** Take a chain $\mathfrak{q}_{0} \subsetneq \dots \subsetneq \mathfrak{q}_{d}, \mathfrak{q}_{i} \in \text{Spec }B, d \geq 0.$
> Contracting to $A$, get a chain $\mathfrak{q}_{0} \cap A \subset \dots \subset \mathfrak{q}_{d} \cap A.$
> We must have $\mathfrak{q}_{i} \cap A \neq \mathfrak{q}_{i+1} \cap A$ because $\mathfrak{q }_{i}\subsetneq \mathfrak{q}_{i+1}$ and [[incomparability]]. Thus, $\text{dim }A \geq d$, and thus $\text{dim }A \geq \text{dim }B$ since $d$ was arbitrary.
-----
####
----
#### 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
> ```