Projective orbit morphisms depend only on the chosen generator up to a unit #
Rescaling a unimodular vector by a unit preserves its projective orbit morphism. This identifies the morphisms constructed from different generators of a trivialized line, as scheme morphisms over arbitrary commutative rings, including nonreduced rings.
References #
- J. S. Milne, Algebraic Groups (2017), §§7.d–7.f.
@[simp]
theorem
TauCeti.Comodule.projectiveOrbitMap_units_smul
{R H M : Type u}
[CommRing R]
[CommRing H]
[HopfAlgebra R H]
[AddCommMonoid M]
[Module R M]
[Comodule R H M]
[Module.Finite R M]
[Module.Projective R M]
(m : M)
(c : Rˣ)
(hm : Module.IsUnimodular R m)
:
Unit rescaling of a unimodular vector does not change its projective orbit morphism.