The constant coordinate of a power basis #
An R-algebra S with a power basis 1, x, …, x ^ (d - 1) retracts onto R: the coordinate
along x ^ 0 = 1 is an R-linear map S → R sending 1 to 1. So R · 1 is a direct summand of
S, which is what it takes to descend a span over S back to a span over R
(TauCeti.mem_of_mem_span_of_mem_closure).
Main statements #
PowerBasis.exists_linearMap_apply_one: an algebra with a power basis retracts onto its scalars.
theorem
PowerBasis.exists_linearMap_apply_one
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Nontrivial S]
[Algebra R S]
(pb : PowerBasis R S)
:
An algebra with a power basis retracts onto its scalars: the coordinate along
pb.gen ^ 0 = 1 is an R-linear map S → R sending 1 to 1.