English
There is a natural pointwise negation operation on submodules: for a submodule S, its negation -S is defined by taking negatives of all elements of S, and this operation is compatible with the submodule structure.
Русский
Существует естественное поэлементное отрицание подмодуля: для подмодуля S определено -S как множество { -x : x ∈ S }, и это сохраняет подмодульную структуру.
LaTeX
$$$\text{Negation on Submodule: }(-S) = \{ -x \mid x \in S \} \text{ yields a submodule.}$$$
Lean4
/-- The submodule with every element negated. Note if `R` is a ring and not just a semiring, this
is a no-op, as shown by `Submodule.neg_eq_self`.
Recall that When `R` is the semiring corresponding to the nonnegative elements of `R'`,
`Submodule R' M` is the type of cones of `M`. This instance reflects such cones about `0`.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseNeg : Neg (Submodule R M) where
neg
p :=
{ -p.toAddSubmonoid with
smul_mem' := fun r m hm => Set.mem_neg.2 <| smul_neg r m ▸ p.smul_mem r <| Set.mem_neg.1 hm }
