English
Smulating with top corresponds to taking the map of I and restricting scalars: I • ⊤ = (I.map (algebraMap R S)).restrictScalars R.
Русский
Умножение на верхний элемент эквивалентно отображению и ограничению скаляров: I • ⊤ = (I.map (algebraMap R S)).restrictScalars R.
LaTeX
$$$I \\cdot \\top = (\\operatorname{map}(\\mathrm{algebraMap}_{R S}) I) \\restrictionScalars R$$$
Lean4
@[simp]
theorem smul_top_eq_map {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) :
I • (⊤ : Submodule R S) = (I.map (algebraMap R S)).restrictScalars R :=
Eq.trans (smul_restrictScalars I (⊤ : Ideal S)).symm <|
congrArg _ <| Eq.trans (Ideal.smul_eq_mul _ _) (Ideal.mul_top _)
