English
The extension-hom construction respects composition of maps: toExtensionHom(f ∘ g) = toExtensionHom(f) ∘ toExtensionHom(g).
Русский
Конструкция extension-hom сохраняет композицию: toExtensionHom(f ∘ g) = toExtensionHom(f) ∘ toExtensionHom(g).
LaTeX
$$$\\mathrm{toExtensionHom}(f\\circ g) = \\mathrm{toExtensionHom}(f) \\circ \\mathrm{toExtensionHom}(g)$$$
Lean4
theorem ker_comp_eq_sup (Q : Generators S T ι') (P : Generators R S ι) :
(Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.ker :=
by
rw [← map_ofComp_ker Q P, Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
rw [← sup_assoc, Algebra.Generators.map_toComp_ker, ← RingHom.ker_eq_comap_bot]
apply le_antisymm (le_trans le_sup_right le_sup_left)
simp only [le_sup_left, sup_of_le_left, sup_le_iff, le_refl, and_true]
intro x hx
simp only [RingHom.mem_ker] at hx
rw [Generators.ker_eq_ker_aeval_val, RingHom.mem_ker, ← algebraMap_self_apply (MvPolynomial.aeval _ x)]
rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]
