17.2. Towers of extensions🔗

When we have a tower of ring extensions, T / S / R, there are three inclusion maps: R \to S, S \to T and R \to T. Those correspond to three Algebra instances:

variable [Algebra R S] [Algebra S T] [Algebra R T]

We then need to ensure the inclusion maps commute, for which we use the IsScalarTower class:

variable [IsScalarTower R S T]

example : algebraMap R T =
    (algebraMap S T).comp (algebraMap R S) :=
  IsScalarTower.algebraMap_eq R S T

Note that only having Algebra R S and Algebra S T instances is not enough to allow Lean to infer Algebra R T: the typeclass system cannot guess a value for S. If the Algebra R T instance is missing, you could declare it as:

example : Algebra R T :=
  Algebra.compHom T (algebraMap R S)

But a more specialized implementation is often better for definitional equality.

Mathlib has a variety of scalar tower instances. For example:

AddCommMonoid.nat_isScalarTower#synth IsScalarTower ℕ R S -- where `[Algebra R S]`
AddCommGroup.intIsScalarTower#synth IsScalarTower ℤ R S -- where `[Algebra R S]`
variable [CharZero K] [CharZero L] in
IsScalarTower.rat#synth IsScalarTower ℚ K L -- where `[Algebra K L]`

IsScalarTower.left R#synth IsScalarTower R R S
IsScalarTower.right#synth IsScalarTower R S S

Polynomial.isScalarTower#synth IsScalarTower R S (Polynomial S)

variable (s : Subring R) in
Submonoid.instIsScalarTowerSubtypeMem s#synth IsScalarTower s R S

variable (s : Submonoid S) in
OreLocalization.instIsScalarTower#synth IsScalarTower R S (Localization s)