map_ofComp_ker — Mathlib

English

Applying the extension-hom evaluation to an algebra-hom evaluation yields the same result as the original evaluation.

Русский

Применение оценки extension-hom к вычислению AlgHom дает тот же результат, что и исходная оценка.

LaTeX

$$$f^{\\mathrm{ext}}(x)=f(x)$$$

Lean4

theorem map_ofComp_ker (Q : Generators S T ι') (P : Generators R S ι) :
    Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker :=
  by
  ext x
  rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
  constructor
  · rintro ⟨x, hx, rfl⟩
    simp only [ker_eq_ker_aeval_val, RingHom.mem_ker] at hx ⊢
    rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_apply]
  · intro hx
    exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

Похожие утверждения