English
Let G be a group acting on a module M over a commutative semiring R, and consider the rays in M. There is a natural action of G on the ray space Module.Ray(R, M) given by g · [v] = [g · v], where [v] denotes the ray determined by v. This action respects the ray equivalence relation and, in particular, scales rays by invertible elements without creating or destroying nonzero rays.
Русский
Пусть G действует на модуль M над коммутативным полем R; пространство лучей Module.Ray(R, M) оборудовано естественным действием G, задаваемым g · [v] = [g · v], где [v] — луч, порожденный вектором v. Это действие сохраняет эквивалентность лучей и, в частности, при инвертируемых элементах не изменяет ненулевые лучи.
LaTeX
$$$\text{There is a } G\text{-action on } \mathrm{Module.Ray}(R,M)\text{ given by } g\cdot [v]=[g\cdot v].$$$
Lean4
/-- Any invertible action preserves the non-zeroness of rays. This is primarily of interest when
`G = Rˣ` -/
instance : MulAction G (Module.Ray R M)
where
smul r := Quotient.map (r • ·) fun _ _ h => h.smul _
mul_smul a b := Quotient.ind fun _ => congr_arg Quotient.mk' <| mul_smul a b _
one_smul := Quotient.ind fun _ => congr_arg Quotient.mk' <| one_smul _ _
