English
The sequence R/I -> R/(aI) -> R/(a) given by multiplication by a and then quotient by a is exact.
Русский
Порядый последовательности R/I → R/(aI) → R/(a) по умножению на a и взятию фактор-кольца по a точен.
LaTeX
$$Function.Exact (Ideal.mulQuot a I) (Ideal.quotOfMul a I)$$
Lean4
/-- The sequence `R ⧸ I →ₗ[R] R ⧸ (a • I) →ₗ[R] R ⧸ (Ideal.span {a})` given by multiplication
by `a` then quotienting by the ideal generated by `a` is exact.
-/
theorem exact_mulQuot_quotOfMul {a : R} (I : Ideal R) : Function.Exact (Ideal.mulQuot a I) (Ideal.quotOfMul a I) :=
by
simp only [exact_iff]
have : ker (Ideal.quotOfMul a I) = a • ⊤ := by
simp only [← submodule_span_eq, quotOfMul, Submodule.factor, Submodule.mapQ, comp_id, Submodule.ker_liftQ,
Submodule.ker_mkQ, Submodule.map_span, Submodule.mkQ_apply, Quotient.mk_eq_mk, Set.image_singleton,
Quotient.smul_top]
simp [this, Ideal.mulQuot, Submodule.mapQ.eq_1, Submodule.range_liftQ, range_comp, Ideal.Quotient.smul_top,
← Ideal.submodule_span_eq, LinearMap.map_span]
