map_id_comp — Mathlib

English

For f₂, f₁, g₂, g₁ as in the statement, map (f₂ ∘ f₁) (g₂ ∘ g₁) equals (map f₂ g₂) ∘ (map f₁ g₁).

Русский

Для f₂, f₁, g₂, g₁ выполняется: map (f₂ ∘ f₁) (g₂ ∘ g₁) = (map f₂ g₂) ∘ (map f₁ g₁).

LaTeX

$$$ \\mathrm{map}(f_2 \\circ f_1) (g_2 \\circ g_1) = (\\mathrm{map} f_2 g_2) \\circ (\\mathrm{map} f_1 g_1) $$$

Lean4

theorem map_id_comp (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) :
    map (AlgHom.id S A) (g₂.comp g₁) = (map (AlgHom.id S A) g₂).comp (map (AlgHom.id S A) g₁) :=
  ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

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