Documentation

TauCeti.RingTheory.PowerSeries.MulDistinguished

Multiplicatively distinguished power series #

A power series g is multiplicatively distinguished of degree s at the radius c when it is distinguished of degree s in the sense of TauCeti.PowerSeries.IsDistinguished and its coefficient in degree s is a multiplicative unit (TauCeti.IsNormMulUnit): an invertible element by which left multiplication scales every norm exactly.

This is the divisor hypothesis of Weierstrass division and preparation over an ultrametric Banach ring whose norm need not be multiplicative, such as a coefficient ring with nilpotents. Its basic consequence is the multiplication estimate: multiplying a restricted series q by such a g on the left loses no norm, ‖g * q‖ = ‖g‖ * ‖q‖, and if q is distinguished of degree k then g * q is distinguished of degree s + k. No multiplicativity of the norm of R is assumed. When the norm of R is multiplicative, the extra condition says only that the distinguished coefficient is a unit.

Norm-preserving coefficient homomorphisms preserve distinguishedness, lowest dominant degrees and multiplicative distinguishedness, so these divisor hypotheses survive isometric coefficient extension.

Main definitions #

Main results #

References #

source
theorem PowerSeries.gaussNorm_map_of_norm_eq {R : Type u_1} [SeminormedRing R] {S : Type u_2} [SeminormedRing S] (φ : R →+* S) (hφ : ∀ (a : R), ‖φ a‖ = ‖a‖) (g : PowerSeries R) (c : ℝ) :
gaussNorm norm c ((map φ) g) = gaussNorm norm c g

A norm-preserving coefficient homomorphism preserves the Gauss norm at every radius.

source
theorem TauCeti.PowerSeries.IsDistinguished.map {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} {S : Type u_2} [SeminormedRing S] (hf : IsDistinguished c s g) (φ : R →+* S) (hφ : ∀ (a : R), ‖φ a‖ = ‖a‖) :
IsDistinguished c s ((PowerSeries.map φ) g)

A norm-preserving coefficient homomorphism preserves distinguishedness, with the same radius and degree. Neither completeness nor surjectivity is required.

source
theorem TauCeti.PowerSeries.IsLowestDominant.map {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} {S : Type u_2} [SeminormedRing S] (hf : IsLowestDominant c s g) (φ : R →+* S) (hφ : ∀ (a : R), ‖φ a‖ = ‖a‖) :
IsLowestDominant c s ((PowerSeries.map φ) g)

A norm-preserving coefficient homomorphism preserves the lowest dominant degree, at the same radius. Neither completeness nor surjectivity is required.

source
structure TauCeti.PowerSeries.IsMulDistinguished {R : Type u_1} [SeminormedRing R] (c : ℝ) (s : ℕ) (g : PowerSeries R) extends TauCeti.PowerSeries.IsDistinguished c s g :
Prop

g is multiplicatively distinguished of degree s at the radius c when it is distinguished of degree s at c and its coefficient in degree s is a multiplicative unit.

The first condition says that the Gauss norm of g at c is attained in degree s and that every later weighted coefficient norm is strictly smaller; earlier coefficients may tie. The second makes left multiplication by g lose no norm, without any multiplicativity assumption on the norm of the coefficient ring.

Instances For
    source
    theorem TauCeti.PowerSeries.isMulDistinguished_iff {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} :
    IsMulDistinguished c s g ↔ IsDistinguished c s g ∧ IsNormMulUnit ((PowerSeries.coeff s) g)

    A series is multiplicatively distinguished exactly when it is distinguished and its coefficient in the distinguished degree is a multiplicative unit.

    source
    theorem TauCeti.PowerSeries.isMulDistinguished_iff_isUnit {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} [NormMulClass R] :
    IsMulDistinguished c s g ↔ IsDistinguished c s g ∧ IsUnit ((PowerSeries.coeff s) g)

    Over a ring with multiplicative norm, a series is multiplicatively distinguished exactly when it is distinguished and its coefficient in the distinguished degree is a unit.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.nontrivial {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} (hg : IsMulDistinguished c s g) :
    Nontrivial R

    The coefficient ring of a multiplicatively distinguished series is nontrivial.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.trunc {R : Type u_1} [SeminormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} (hg : IsMulDistinguished c s g) :
    IsMulDistinguished c s ↑((PowerSeries.trunc (s + 1)) g)

    The truncation of a multiplicatively distinguished series just past its distinguished degree is again multiplicatively distinguished of that degree.

    source
    theorem TauCeti.PowerSeries.isMulDistinguished_X_sub_C {R : Type u_1} [SeminormedRing R] {c : ℝ} [NormOneClass R] (hc : 0 < c) {b : R} (hb : ‖b‖ ≤ c) :
    IsMulDistinguished c 1 (PowerSeries.X - PowerSeries.C b)

    A linear polynomial X - b whose root lies in the closed disc of radius c > 0 is multiplicatively distinguished of degree 1 at c, over a norm-one ring. The constant term may have the same weighted norm as the leading one.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.isDistinguished_mul {R : Type u_1} [SeminormedRing R] {c : ℝ} {s k : ℕ} {g q : PowerSeries R} [IsUltrametricDist R] (hg : IsMulDistinguished c s g) (hq : IsDistinguished c k q) (hc : 0 < c) :
    IsDistinguished c (s + k) (g * q)

    Distinguished degrees under multiplication by a multiplicatively distinguished series. If g is multiplicatively distinguished of degree s and q is distinguished of degree k at a positive radius, then g * q is distinguished of degree s + k.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.norm_mul_coeff {R : Type u_1} [SeminormedCommRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} (hg : IsMulDistinguished c s g) (x : R) :
    ‖x * (PowerSeries.coeff s) g‖ = ‖x‖ * ‖(PowerSeries.coeff s) g‖

    Right multiplication by the distinguished coefficient scales norms exactly.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.normOneClass {R : Type u_1} [NormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} (hg : IsMulDistinguished c s g) :
    NormOneClass R

    The norm of the coefficient ring of a multiplicatively distinguished series takes the value 1 at 1, since the distinguished coefficient is a nonzero multiplicative unit.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.map {R : Type u_1} [NormedRing R] {c : ℝ} {s : ℕ} {g : PowerSeries R} {S : Type u_2} [SeminormedRing S] (hf : IsMulDistinguished c s g) (φ : R →+* S) (hφ : ∀ (a : R), ‖φ a‖ = ‖a‖) :
    IsMulDistinguished c s ((PowerSeries.map φ) g)

    A norm-preserving coefficient homomorphism preserves multiplicative distinguishedness, even without a multiplicative coefficient norm or a surjectivity hypothesis.

    source
    theorem TauCeti.PowerSeries.isMulDistinguished_monomial {R : Type u_1} [NormedRing R] {c : ℝ} [Nontrivial R] (hc : 0 < c) {a : R} (ha : IsNormMulUnit a) (n : ℕ) :
    IsMulDistinguished c n ((PowerSeries.monomial n) a)

    A monomial whose coefficient is a multiplicative unit is multiplicatively distinguished of its degree at a positive radius, over a nontrivial ring.

    source
    theorem TauCeti.PowerSeries.isMulDistinguished_iff_gaussNorm_eq {R : Type u_1} [NormedRing R] {c : ℝ} {s : ℕ} [NormOneClass R] (hc : 0 < c) {p : Polynomial R} (hp : p.IsMonicOfDegree s) :
    IsMulDistinguished c s ↑p ↔ PowerSeries.gaussNorm norm c ↑p = c ^ s

    Weierstrass polynomials at a radius. Over a norm-one ring, a monic polynomial of degree s is multiplicatively distinguished of degree s at a positive radius c exactly when its Gauss norm at c is c ^ s, the weighted norm of its leading term. This is the normalisation of the polynomial factor in Weierstrass preparation. Lower coefficients may tie with the leading one, as for X - 1 at the radius 1.

    source
    theorem TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_mul {R : Type u_1} [NormedRing R] {c : ℝ} {s : ℕ} {g q : PowerSeries R} [IsUltrametricDist R] (hg : IsMulDistinguished c s g) (hc : 0 < c) (hq : PowerSeries.IsRestricted c q) :
    PowerSeries.gaussNorm norm c (g * q) = PowerSeries.gaussNorm norm c g * PowerSeries.gaussNorm norm c q

    The multiplication estimate. Left multiplication by a multiplicatively distinguished series multiplies the Gauss norm of a restricted series by the Gauss norm of the divisor, at a positive radius:

    ‖g * q‖ = ‖g‖ * ‖q‖.

    No multiplicativity of the norm of the coefficient ring is assumed.

    source
    theorem TauCeti.PowerSeries.gaussNorm_X_sub_C_mul {R : Type u_1} [NormedRing R] {c : ℝ} {q : PowerSeries R} [IsUltrametricDist R] [NormOneClass R] (hc : 0 < c) {a : R} (ha : ‖a‖ ≤ c) (hq : PowerSeries.IsRestricted c q) :
    PowerSeries.gaussNorm norm c ((PowerSeries.X - PowerSeries.C a) * q) = c * PowerSeries.gaussNorm norm c q

    Multiplying a restricted series by X - a, for a in the closed disc of radius c > 0, multiplies its Gauss norm at c by c.