Documentation

TauCeti.RingTheory.HahnSeries.Map

Coefficientwise maps of Hahn series #

A ring homomorphism f : R →+* S induces the ring homomorphism R⟦Γ⟧ →+* S⟦Γ⟧ applying f to every coefficient. Mathlib provides the underlying map HahnSeries.map and its compatibility with addition, multiplication and monomials; this file bundles it as a ring homomorphism, records that it commutes with exponent embeddings and with the inclusion of power series, and shows that an injective coefficient map preserves supports and orders.

For Laurent series R⸨X⸩ = R⟦ℤ⟧ this is the base change of the coefficients, for instance along a field embedding K → L, under which formal substitution and the other coefficient-level constructions on Laurent series are natural.

Main definitions #

Main results #

Implementation notes #

The descent applies a K-linear functional f : L → K to every coefficient. Since φ and ℓ have coefficients in K, this sends c • φ ℓⁱ to f c • φ ℓⁱ, so it turns the relation over L into the one whose coefficients are the images of those of P and Q under f. Choosing f with f of the leading coefficient of Q equal to 1 keeps the new Q nonzero.

source
theorem HahnSeries.map_embDomain {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {S : Type u_4} [Zero R] [Zero S] {F : Type u_6} [FunLike F R S] [ZeroHomClass F R S] [PartialOrder Γ] [PartialOrder Γ'] (f : Γ ↪o Γ') (x : HahnSeries Γ R) (g : F) :
(embDomain f x).map g = embDomain f (x.map g)

Coefficientwise maps commute with exponent embeddings.

source
@[simp]
theorem HahnSeries.support_map_of_injective {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [Zero R] [Zero S] {F : Type u_6} [FunLike F R S] [ZeroHomClass F R S] [PartialOrder Γ] (x : HahnSeries Γ R) {g : F} (hg : Function.Injective ⇑g) :
(x.map g).support = x.support

An injective coefficient map preserves the support.

source
@[simp]
theorem HahnSeries.orderTop_map_of_injective {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [Zero R] [Zero S] {F : Type u_6} [FunLike F R S] [ZeroHomClass F R S] [LinearOrder Γ] (x : HahnSeries Γ R) {g : F} (hg : Function.Injective ⇑g) :
(x.map g).orderTop = x.orderTop

An injective coefficient map preserves orderTop.

source
@[simp]
theorem HahnSeries.order_map_of_injective {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [Zero R] [Zero S] {F : Type u_6} [FunLike F R S] [ZeroHomClass F R S] [LinearOrder Γ] [Zero Γ] (x : HahnSeries Γ R) {g : F} (hg : Function.Injective ⇑g) :
(x.map g).order = x.order

An injective coefficient map preserves the order of a nonzero series, and the junk value 0 of the order of 0.

source
def HahnSeries.mapRingHom {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] (f : R →+* S) :
HahnSeries Γ R →+* HahnSeries Γ S

The ring homomorphism R⟦Γ⟧ →+* S⟦Γ⟧ applying a ring homomorphism f : R →+* S to every coefficient.

Instances For
    source
    theorem HahnSeries.mapRingHom_apply {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] (f : R →+* S) (x : HahnSeries Γ R) :
    (mapRingHom f) x = x.map f
    source
    @[simp]
    theorem HahnSeries.coeff_mapRingHom {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] (f : R →+* S) (x : HahnSeries Γ R) (g : Γ) :
    ((mapRingHom f) x).coeff g = f (x.coeff g)
    source
    @[simp]
    theorem HahnSeries.mapRingHom_id {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] :
    mapRingHom (RingHom.id R) = RingHom.id (HahnSeries Γ R)
    source
    theorem HahnSeries.mapRingHom_comp {Γ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) :
    mapRingHom (g.comp f) = (mapRingHom g).comp (mapRingHom f)
    source
    theorem HahnSeries.mapRingHom_injective {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) :
    Function.Injective ⇑(mapRingHom f)
    source
    theorem HahnSeries.mem_map_rangeS {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [Semiring S] {f : R →+* S} {x : HahnSeries Γ S} :
    x ∈ (mapRingHom f).rangeS ↔ ∀ (g : Γ), x.coeff g ∈ f.rangeS

    A Hahn series is in the range of a coefficientwise map exactly when all its coefficients are in the range of the coefficient map. Compare Polynomial.mem_map_rangeS.

    source
    @[simp]
    theorem HahnSeries.map_ofPowerSeries {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [Semiring Γ] [PartialOrder Γ] [IsStrictOrderedRing Γ] [Semiring R] [Semiring S] (f : R →+* S) (p : PowerSeries R) :
    ((ofPowerSeries Γ R) p).map f = (ofPowerSeries Γ S) ((PowerSeries.map f) p)

    Coefficientwise maps commute with the inclusion of power series into Hahn series.

    source
    theorem HahnSeries.map_smul_mapRingHom_algebraMap {Γ : Type u_1} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] {K : Type u_6} {L : Type u_7} [CommSemiring K] [CommSemiring L] [Algebra K L] (f : L →ₗ[K] K) (c : L) (x : HahnSeries Γ K) :
    (c • (mapRingHom (algebraMap K L)) x).map f = f c • x

    Applying a K-linear functional f : L → K to every coefficient of c • x, for a series x with coefficients in K, gives f c • x.

    source
    theorem HahnSeries.exists_mul_eval₂_C_eq_eval₂_C_of_mapRingHom {Γ : Type u_1} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] {K : Type u_6} {L : Type u_7} [Field K] [CommRing L] [Algebra K L] {φ ℓ : HahnSeries Γ K} {P Q : Polynomial L} (hQ : Q ≠ 0) (h : (mapRingHom (algebraMap K L)) φ * Polynomial.eval₂ C ((mapRingHom (algebraMap K L)) ℓ) Q = Polynomial.eval₂ C ((mapRingHom (algebraMap K L)) ℓ) P) :
    ∃ (P' : Polynomial K) (Q' : Polynomial K), Q' ≠ 0 ∧ φ * Polynomial.eval₂ C ℓ Q' = Polynomial.eval₂ C ℓ P'

    Descent of algebraic relations to the coefficient field. Let L be an algebra over a field K, for instance a field extension, and let φ and ℓ be series with coefficients in K. If φ Q(ℓ) = P(ℓ) over L for polynomials P, Q over L with Q ≠ 0, then φ Q'(ℓ) = P'(ℓ) for polynomials P', Q' over K with Q' ≠ 0. Polynomials are evaluated through the constant series HahnSeries.C, which does not depend on a choice of algebra structure on the series.