English
Let K be a commutative ring and R a monoid acting on the polynomial ring K[X]. The rational function construction RatFunc K inherits a compatible R-action, so RatFunc K sits in a scalar tower with R and K[X]. In particular, RatFunc K carries the R-scalar action in a way that is compatible with its underlying K[X]-structure; i.e. IsScalarTower R K[X] RatFunc K holds.
Русский
Пусть K — коммутативное кольцо, а R — моноид, действующий на кольцо многочленов K[X]. Конструкция RatFunc K наследует совместимое действие над R, и RatFunc K образует цепочку скаляров вместе с R и K[X]. То есть RatFunc K оснащено действием над R так, что выполняется совместимость со связью R ⊢ K[X] ⊢ RatFunc K.
LaTeX
$$$ \operatorname{IsScalarTower}(R, K[X], \mathrm{RatFunc}\,K)$$$
Lean4
instance : IsScalarTower R K[X] (RatFunc K) :=
⟨fun c p q => q.induction_on' fun q r _ => by rw [← mk_smul, smul_assoc, mk_smul, mk_smul]⟩
