English
Given an algebra homomorphism e: K1 →ₐ[A] K2 and f: L1 →ₐ[B] L2, the induced maps commute with the base algebra maps on x ∈ K1: algebraMap_K2_L2 (e x) = f (algebraMap_K1_L1 x).
Русский
Дано гомоморфизм алгебр e: K1 →ₐ[A] K2 и f: L1 →ₐ[B] L2, отображение в соответствующих местах согласуется с базовыми алгебраическими отображениями: algebraMap_K2_L2 (e x) = f (algebraMap_K1_L1 x).
LaTeX
$$algHom_commutes (e : K1 →ₐ[A] K2) (f : L1 →ₐ[B] L2) (x : K1) : algebraMap K2 L2 (e x) = f (algebraMap K1 L1 x)$$
Lean4
theorem algHom_commutes (e : K₁ →ₐ[A] K₂) (f : L₁ →ₐ[B] L₂) (x : K₁) :
algebraMap K₂ L₂ (e x) = f (algebraMap K₁ L₁ x) :=
by
obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective (A := A) x
simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L₁,
AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
