English
The graph of a linear map f: M → M₂ is the submodule of M × M₂ consisting of all pairs (m, f(m)). It is closed under addition and scalar multiplication, hence a submodule of the product.
Русский
Граф линейного отображения f: M → M₂ — это подпомножество в M × M₂, состоящее из пар (m, f(m)); оно замкнуто по сложению и скалярному умножению, т.е. подмодуля произведения.
LaTeX
$$$\\text{graph}(f) = \\{(m, f(m)) : m\\in M\\} \\leqq\\; M \\times M_2$$$
Lean4
/-- Graph of a linear map. -/
def graph : Submodule R (M × M₂) where
carrier := {p | p.2 = f p.1}
add_mem' (ha : _ = _)
(hb : _ = _) := by
change _ + _ = f (_ + _)
rw [map_add, ha, hb]
zero_mem' := Eq.symm (map_zero f)
smul_mem' c x
(hx : _ = _) := by
change _ • _ = f (_ • _)
rw [map_smul, hx]
