Laurent expansions of rational functions

Main declarations

• RatFunc.laurent: the Laurent expansion of the rational function f at r, as an AlgHom.
• RatFunc.laurent_injective: the Laurent expansion at r is unique

Implementation details

Implemented as the quotient of two Taylor expansions, over domains. An auxiliary definition is provided first to make the construction of the AlgHom easier, which works on CommRing which are not necessarily domains.

theorem RatFunc.taylor_mem_nonZeroDivisors {R : Type u} [CommRing R] (r : R) (p : Polynomial R) (hp : p ∈ nonZeroDivisors (Polynomial R)) : ↑(Polynomial.taylor r) p ∈ nonZeroDivisors (Polynomial R)

def RatFunc.laurentAux {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) : RatFunc R →+* RatFunc R

The Laurent expansion of rational functions about a value. Auxiliary definition, usage when over integral domains should prefer RatFunc.laurent.

theorem RatFunc.laurentAux_ofFractionRing_mk {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : { x // x ∈ nonZeroDivisors (Polynomial R) }) : ↑(RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } = { toFractionRing := Localization.mk (↑(Polynomial.taylor r) p) { val := ↑(Polynomial.taylor r) ↑q, property := (_ : ↑(Polynomial.taylor r) ↑q ∈ nonZeroDivisors (Polynomial R)) } }

theorem RatFunc.laurentAux_div {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : Polynomial R) : ↑(RatFunc.laurentAux r) (↑(algebraMap (Polynomial R) (RatFunc R)) p / ↑(algebraMap (Polynomial R) (RatFunc R)) q) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p) / ↑(algebraMap ((fun x => Polynomial R) q) (RatFunc R)) (↑(Polynomial.taylor r) q)

@[simp]

theorem RatFunc.laurentAux_algebraMap {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) : ↑(RatFunc.laurentAux r) (↑(algebraMap (Polynomial R) (RatFunc R)) p) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p)

def RatFunc.laurent {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) : RatFunc R →ₐ[R] RatFunc R

The Laurent expansion of rational functions about a value.

theorem RatFunc.laurent_div {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : Polynomial R) : ↑(RatFunc.laurent r) (↑(algebraMap (Polynomial R) (RatFunc R)) p / ↑(algebraMap (Polynomial R) (RatFunc R)) q) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p) / ↑(algebraMap ((fun x => Polynomial R) q) (RatFunc R)) (↑(Polynomial.taylor r) q)

@[simp]

theorem RatFunc.laurent_algebraMap {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) : ↑(RatFunc.laurent r) (↑(algebraMap (Polynomial R) (RatFunc R)) p) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p)

@[simp]

theorem RatFunc.laurent_X {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) : ↑(RatFunc.laurent r) RatFunc.X = RatFunc.X + ↑RatFunc.C r

@[simp]

theorem RatFunc.laurent_C {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (x : R) : ↑(RatFunc.laurent r) (↑RatFunc.C x) = ↑RatFunc.C x

@[simp]

theorem RatFunc.laurent_at_zero {R : Type u} [CommRing R] [hdomain : IsDomain R] (f : RatFunc R) : ↑(RatFunc.laurent 0) f = f

theorem RatFunc.laurent_laurent {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (s : R) (f : RatFunc R) : ↑(RatFunc.laurent r) (↑(RatFunc.laurent s) f) = ↑(RatFunc.laurent (r + s)) f

theorem RatFunc.laurent_injective {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) : Function.Injective ↑(RatFunc.laurent r)