English
There is a canonical linear map from the ideal I_y to Q that sends the class representing r ∈ I_y to the value of the maximal extension on r · y, i.e., it uses the maximal extension to evaluate at the scalar representative of the element in the ideal.
Русский
Существует каноническое линейное отображение от Ideал I_y в Q, которое отправляет представление r ∈ I_y в Q на значение максимального расширения применённого к r · y.
LaTeX
$$$ idealTo(y) : (ExtensionOfMaxAdjoin.ideal i f y) \\to Q \\\\to r \\mapsto (\\mathrm{extensionOfMax}\\ i\\ f).toLinearPMap ( \\langle r \\cdot y, \\text{mem} \\rangle ) $$$
Lean4
/-- A linear map `I ⟶ Q` by `x ↦ f' (x • y)` where `f'` is the maximal extension -/
def idealTo (y : N) : ExtensionOfMaxAdjoin.ideal i f y →ₗ[R] Q
where
toFun (z : { x // x ∈ ideal i f y }) := (extensionOfMax i f).toLinearPMap ⟨(↑z : R) • y, z.prop⟩
map_add'
(z1 z2 : { x // x ∈
ideal i f y }) := by
simp_rw [← (extensionOfMax i f).toLinearPMap.map_add]
congr
apply add_smul
map_smul' z1
(z2 : { x // x ∈ ideal i f
y }) := by
simp_rw [← (extensionOfMax i f).toLinearPMap.map_smul]
congr 2
apply mul_smul
