English
Define the ideal I_y consisting of all scalars r ∈ R such that r · y lies in the domain of the maximal extension (extensionOfMax i f). This I_y is an ideal of R capturing which scalars send y into the extension’s domain.
Русский
Определим идеал I_y как множество всех скаляров r ∈ R, для которых r · y принадлежит области определения максимального расширения (extensionOfMax i f). Этот идеал — идеал в R, отражающий, какие скаляры отправляют y в область определения расширения.
LaTeX
$$$ I_y = \\{ r \\in R \\mid r \\cdot y \\in \\mathrm{domain}(\\mathrm{extensionOfMax}\\ i\\ f) \\} $$$
Lean4
/-- The ideal `I = {r | r • y ∈ N}` -/
def ideal (y : N) : Ideal R :=
(extensionOfMax i f).domain.comap ((LinearMap.id : R →ₗ[R] R).smulRight y)
