17.3. Subrings🔗

Another way to represent ring extensions is with subrings. The main drawback of using subrings everywhere is viewing an existing ring as a subring of another requires transferring existing results. Moreover, there is no obvious "universal" ring we can choose for Mathlib to include every other ring as a subring. Still, Mathlib has tools to move between Algebra and Subring.

As mentioned above, a subring s \le R has an automatic Algebra instance:

variable (s : Subring R)
Algebra.ofSubring s#synth Algebra s R

Moreover, if we have an extension S / R, the expected IsScalarTower instance is found automatically:

variable [Algebra R S]
Submonoid.instIsScalarTowerSubtypeMem s#synth IsScalarTower s R S

Suppose we are given an inclusion of subrings:

variable {s t : Subring R} (h : s ≤ t)

Then we have to create the Algebra and IsScalarTower instances ourselves:

abbrev inclusionAlgebra : Algebra s t :=
  RingHom.toAlgebra (Subring.inclusion h)

instance : letI := inclusionAlgebra h;
    IsScalarTower s t R :=
  let := inclusionAlgebra h
  { smul_assoc := fun ⟨x, _⟩ ⟨y, _⟩ z ↦ smul_assoc x y z }

The other option is to turn s into a subring of t, as s.comap t.subtype:

Submonoid.instIsScalarTowerSubtypeMem (Subring.comap t.subtype s)#synth IsScalarTower (s.comap t.subtype) t R

When working pointwise this gets messy fast though, mapping between elements of s and the corresponding elements of s.comap t.subtype.