map_comp — Mathlib

English

For f: P → P' and g: P' → P'', one has map(g ∘ f) = (map g) restricted to S composed with map f.

Русский

Для отображений f: P → P' и g: P' → P'' выполнено map(g ∘ f) = (map g) ∘ map f (с учетом скалярного ограничения).

LaTeX

$$$\\text{map}(g \\circ f) = (\\text{map } g).restrictScalars S \\circ_{\\ell} \\text{map } f$$$

Lean4

theorem map_comp (f : Hom P P') (g : Hom P' P'') : map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by ext;
  simp [Cotangent.map_comp]

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