Rational fibers of projective orbit morphisms

The projective orbit morphism sends a rational group point to the line through its translate of the chosen vector. Two such images coincide exactly when those translates span the same line. In particular, its fiber over the identity image is the line stabilizer. This identifies the rational fibers used in the construction of homogeneous spaces from projective orbits.

The result concerns points of the underlying projective spectrum. It does not identify scheme-theoretic fibers or a quotient scheme. No smoothness or reducedness is required.

The construction uses Comodule.projectiveOrbitMap, its standard-open formulas, and Comodule.basePointsRepresentation.

References

• J. S. Milne, Algebraic Groups (2017), §§7.d–7.f.

@[simp]

theorem TauCeti.Comodule.comp_orbitCoordinates {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) (g : WithConv (H →ₐ[R] R)) : g.ofConv.comp (orbitCoordinates m) = SymmetricAlgebra.lift ((Module.Dual.eval R M) (((basePointsRepresentation M) g) m))

Evaluating orbit coordinates at a rational point evaluates homogeneous polynomials on the translated vector.

theorem TauCeti.Comodule.mem_projectiveOrbitMap_kernelPoint_iff {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) {s : SymmetricAlgebra k (Module.Dual k M)} {n : ℕ} (hn : 0 < n) (hs : s ∈ SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M) n) : s ∈ ((projectiveOrbitMap m hm) (AlgHom.kernelPoint g.ofConv)).asHomogeneousIdeal ↔ (SymmetricAlgebra.lift ((Module.Dual.eval k M) (((basePointsRepresentation M) g) m))) s = 0

A positive-degree homogeneous polynomial vanishes at the image of a rational group point precisely when it vanishes on the translated vector.

@[simp]

theorem TauCeti.Comodule.ι_mem_projectiveOrbitMap_kernelPoint_iff {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) (φ : Module.Dual k M) : (SymmetricAlgebra.ι k (Module.Dual k M)) φ ∈ ((projectiveOrbitMap m hm) (AlgHom.kernelPoint g.ofConv)).asHomogeneousIdeal ↔ φ (((basePointsRepresentation M) g) m) = 0

A linear homogeneous coordinate vanishes at a rational orbit image exactly when the corresponding functional annihilates the translated vector.

theorem TauCeti.Comodule.projectiveOrbitMap_kernelPoint_eq_iff_span_eq {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (p : M) (hp : Module.IsUnimodular k p) (g h : WithConv (H →ₐ[k] k)) : (projectiveOrbitMap m hm) (AlgHom.kernelPoint g.ofConv) = (projectiveOrbitMap p hp) (AlgHom.kernelPoint h.ofConv) ↔ k ∙ ((basePointsRepresentation M) g) m = k ∙ ((basePointsRepresentation M) h) p

Two rational projective orbit images coincide exactly when their translated vectors generate the same line. The vectors may be chosen independently.

theorem TauCeti.Comodule.projectiveOrbitMap_kernelPoint_eq_one_iff {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) (g : WithConv (H →ₐ[k] k)) : (projectiveOrbitMap m hm) (AlgHom.kernelPoint g.ofConv) = (projectiveOrbitMap m hm) (AlgHom.kernelPoint (Bialgebra.counitAlgHom k H)) ↔ Submodule.map ((basePointsRepresentation M) g) (k ∙ m) = k ∙ m

The rational fiber over the identity orbit image consists precisely of the points that carry the chosen line onto itself.