map_comp — Mathlib

English

The range of the tensor product map is the join of the ranges of includeLeft ∘ f and includeRight ∘ g.

Русский

Образ отображения тензорного произведения равен объединению образов includeLeft ∘ f и includeRight ∘ g.

LaTeX

$$$ \\mathrm{range}(\\mathrm{map}\\; f\\; g) = \\mathrm{range}(\\mathrm{includeLeft} \\circ f) \\sqcup \\mathrm{range}(\\mathrm{includeRight} \\circ g) $$$

Lean4

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

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