algEquiv_commutes — Mathlib

English

For algebra equivalences e: K1 ≃ₐ[A] K2 and f: L1 ≃ₐ[B] L2, and x ∈ K1, the algebra maps commute: algebraMap_K2_L2 (e x) = f (algebraMap_K1_L1 x).

Русский

Для эквивалентностей алгебры e: K1 ≃ₐ[A] K2 и f: L1 ≃ₐ[B] L2, и элемента x ∈ K1, выполняется согласование отображений: algebraMap_K2_L2 (e x) = f (algebraMap_K1_L1 x).

LaTeX

$$algEquiv_commutes (e : K1 ≃ₐ[A] K2) (f : L1 ≃ₐ[B] L2) (x : K1) : algebraMap K2 L2 (e x) = f (algebraMap K1 L1 x)$$

Lean4

theorem algEquiv_commutes (e : K₁ ≃ₐ[A] K₂) (f : L₁ ≃ₐ[B] L₂) (x : K₁) :
    algebraMap K₂ L₂ (e x) = f (algebraMap K₁ L₁ x) := by exact algHom_commutes e.toAlgHom f.toAlgHom _

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