English
Composition of quotient-factor bijections is compatible: the factor map for g ∘ f equals the composition of the maps for f and g.
Русский
Сопоставление факторов сохраняется под композициями: отображение факторов от g ∘ f равно композиции отображений f и g.
LaTeX
$$idealFactorsFunOfQuotHom_comp$$
Lean4
theorem idealFactorsFunOfQuotHom_comp {f : R ⧸ I →+* A ⧸ J} {g : A ⧸ J →+* B ⧸ L} (hf : Function.Surjective f)
(hg : Function.Surjective g) :
(idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) =
idealFactorsFunOfQuotHom (show Function.Surjective (g.comp f) from hg.comp hf) :=
by
refine OrderHom.ext _ _ (funext fun x => ?_)
rw [idealFactorsFunOfQuotHom, idealFactorsFunOfQuotHom, OrderHom.comp_coe, OrderHom.coe_mk, OrderHom.coe_mk,
Function.comp_apply, idealFactorsFunOfQuotHom, OrderHom.coe_mk, Subtype.mk_eq_mk, Subtype.coe_mk,
map_comap_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective, map_map]
