English
Let R be a ring, and E, F be R-modules. Consider the class of partial linear maps from E to F, each equipped with a domain which is a submodule of E. Define the sum of two partial linear maps f and g by (f + g).domain = dom(f) ∩ dom(g) and (f + g)(x) = f(x) + g(x) for x in dom(f) ∩ dom(g). The zero element is the map with domain = ⊤ and value 0 everywhere. Then this operation makes the class into an AddCommMonoid.
Русский
Пусть R — кольцо, E и F — модули над R. Рассмотрим множество частичных линейных отображений E → F, у которых область определения является подпространством E. Сложение двух частичных отображений f и g определяется как (f + g) с областью dom(f) ∩ dom(g) и значением (f + g)(x) = f(x) + g(x) для x в dom(f) ∩ dom(g). Нуль-отображение имеет область ⊤ и нулевые значения. Тогда эти операции образуют коммутативную моноидальную структуру.
LaTeX
$$$$\\text{There is a binary operation }+\\text{ on }\\mathrm{LinearPMap}(R,E,F) \\text{ given by } \n\\operatorname{dom}(f+g)=\\operatorname{dom}(f)\\cap\\operatorname{dom}(g),\\quad (f+g)(x)=f(x)+g(x)\\ (x\\in \\operatorname{dom}(f)\\cap\\operatorname{dom}(g)). \n\\text{Let }0\\text{ be the map with }\\operatorname{dom}(0)=\\top\\text{ and }0(x)=0. \n\\text{Then }(\\mathrm{LinearPMap}(R,E,F),+ ,0)\\text{ is an AddCommMonoid.} $$$$
Lean4
instance instAddCommMonoid : AddCommMonoid (E →ₗ.[R] F) :=
⟨fun f g => by
ext x y hxy
· simp only [add_domain, inf_comm]
· simp only [add_apply, add_comm]⟩
