Power series as scalars on Hahn series #
If A⟦X⟧ is an S-algebra, the S-algebra structure on A⟦Γ⟧ is inherited from A⟦X⟧
through HahnSeries.ofPowerSeries. This file records that the resulting algebra actions form a
scalar tower S → A⟦X⟧ → A⟦Γ⟧.
Main results #
TauCeti.hahnSeries_isScalarTower_powerSeries: the algebra actions ofSonA⟦X⟧and on Hahn seriesA⟦Γ⟧form a scalar tower.
instance
TauCeti.hahnSeries_isScalarTower_powerSeries
{Γ : Type u_1}
{A : Type u_2}
{S : Type u_3}
[Semiring Γ]
[PartialOrder Γ]
[IsStrictOrderedRing Γ]
[CommSemiring A]
[CommSemiring S]
[Algebra S (PowerSeries A)]
:
IsScalarTower S (PowerSeries A) (HahnSeries Γ A)
If A⟦X⟧ is an S-algebra, the scalars of S on the Hahn series A⟦Γ⟧ factor through
A⟦X⟧. The S-algebra structure on A⟦Γ⟧ is the one inherited from A⟦X⟧.