This closely mirrors `Mathlib/RingTheory/Ideal/GoingDown.lean` by defining an analogous predicate `Algebra.HasGoingUp` and proving basic properties. It includes:

- `Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap`: going up is equivalent
  to specializations lifting along `Spec S → Spec R`.
- `Algebra.HasGoingUp.of_isIntegral`: integral algebras satisfy going up.
- `Ideal.exists_ltSeries_of_hasGoingUp`: a generalization of `exists_ideal_over_prime_of_isIntegral_of_isPrime` from `Mathlib/RingTheory/Ideal/GoingUp.lean` to chains of arbitrary length. This was previously an explicitly marked `TODO`.