English
The composition of the algebra hom (↑(quotQuotEquivCommₐ R I J)) with quotQuotMkₐ R I J equals quotQuotMkₐ R J I.
Русский
Композицией алгебраических гомоморфизмов (↑(quotQuotEquivCommₐ R I J)) и quotQuotMkₐ R I J даётся отображение quotQuotMkₐ R J I.
LaTeX
$$$\text{AlgHom}.comp (↑(quotQuotEquivCommₐ R I J)) (quotQuotMkₐ R I J) = quotQuotMkₐ R J I$$$
Lean4
theorem factor_ker (H : I ≤ J) [I.IsTwoSided] [J.IsTwoSided] : RingHom.ker (factor H) = J.map (Ideal.Quotient.mk I) :=
by
ext x
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rcases Ideal.Quotient.mk_surjective x with ⟨r, hr⟩
rw [← hr] at h ⊢
simp only [factor, RingHom.mem_ker, lift_mk, eq_zero_iff_mem] at h
exact Ideal.mem_map_of_mem _ h
· rcases mem_image_of_mem_map_of_surjective _ Ideal.Quotient.mk_surjective h with ⟨r, hr, eq⟩
simpa [← eq, Ideal.Quotient.eq_zero_iff_mem] using hr
