English
If there is a surjective map h: M → N with h(m) = m • (1 : N), then N → P → Q forms a scalar tower.
Русский
Если существует сюрьективное отображение h: M → N с h(m) = m • 1, тогда N → P → Q образует скалярную башню.
LaTeX
$$$ \text{IsScalarTower } N P Q$$$
Lean4
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / N / M` and `Q / P / M` are
scalar towers, then `Q / P / N` is also a scalar tower.
-/
@[to_additive]
theorem to₂₃₄ (M N P Q) [SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q]
[IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower M P Q]
(h : Function.Surjective fun m : M ↦ m • (1 : N)) : IsScalarTower N P Q where
smul_assoc n p q := by obtain ⟨m, rfl⟩ := h n; simp_rw [smul_one_smul, smul_assoc]
