English
The map pointToPoint defines a canonical point in the prime spectrum for each x: σ → K.
Русский
Отображение pointToPoint задаёт каноническую точку в примарном спектре для каждого x: σ → K.
LaTeX
$$pointToPoint x$$
Lean4
/-- The map `R ⧸ I →ₗ[R] R ⧸ (a • I)` defined by multiplication by `a` is injective if `a` is
a nonzero divisor.
-/
theorem mulQuot_injective {a : R} (I : Ideal R) (ha : a ∈ nonZeroDivisors R) : Function.Injective (Ideal.mulQuot a I) :=
by
simp only [mulQuot, Submodule.mapQ, ← ker_eq_bot]
apply Submodule.ker_liftQ_eq_bot'
apply le_antisymm
· have : Submodule.map (mul R R a) I = a • I := rfl
rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]
· have m : I = Submodule.comap (mul R R a) (a • I) := by
ext b
exact (Submodule.mul_mem_smul_iff ha).symm
simp [← m, ker_comp]
