Laurent expansions of rational functions #
Main declarations #
RatFunc.laurent
: the Laurent expansion of the rational functionf
atr
, as anAlgHom
.RatFunc.laurent_injective
: the Laurent expansion atr
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)
The Laurent expansion of rational functions about a value.
Auxiliary definition, usage when over integral domains should prefer RatFunc.laurent
.
Equations
- RatFunc.laurentAux r = RatFunc.mapRingHom { toFun := ⇑(Polynomial.taylor r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯
Instances For
theorem
RatFunc.laurentAux_ofFractionRing_mk
{R : Type u}
[CommRing R]
(r : R)
(p : Polynomial R)
(q : ↥(nonZeroDivisors (Polynomial R)))
:
(RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } = { toFractionRing := Localization.mk ((Polynomial.taylor r) p) ⟨(Polynomial.taylor r) ↑q, ⋯⟩ }
theorem
RatFunc.laurentAux_div
{R : Type u}
[CommRing R]
(r : R)
(p : Polynomial R)
(q : Polynomial R)
[IsDomain R]
:
(RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) / (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
@[simp]
theorem
RatFunc.laurentAux_algebraMap
{R : Type u}
[CommRing R]
(r : R)
(p : Polynomial R)
[IsDomain R]
:
(RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
The Laurent expansion of rational functions about a value.
Equations
- RatFunc.laurent r = RatFunc.mapAlgHom (AlgHom.ofLinearMap (Polynomial.taylor r) ⋯ ⋯) ⋯
Instances For
theorem
RatFunc.laurent_div
{R : Type u}
[CommRing R]
(r : R)
(p : Polynomial R)
(q : Polynomial R)
[IsDomain R]
:
(RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) / (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
@[simp]
theorem
RatFunc.laurent_algebraMap
{R : Type u}
[CommRing R]
(r : R)
(p : Polynomial R)
[IsDomain R]
:
(RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
@[simp]
theorem
RatFunc.laurent_X
{R : Type u}
[CommRing R]
(r : R)
[IsDomain R]
:
(RatFunc.laurent r) RatFunc.X = RatFunc.X + RatFunc.C r
@[simp]
theorem
RatFunc.laurent_C
{R : Type u}
[CommRing R]
(r : R)
[IsDomain R]
(x : R)
:
(RatFunc.laurent r) (RatFunc.C x) = RatFunc.C x
@[simp]
theorem
RatFunc.laurent_at_zero
{R : Type u}
[CommRing R]
(f : RatFunc R)
[IsDomain R]
:
(RatFunc.laurent 0) f = f
theorem
RatFunc.laurent_laurent
{R : Type u}
[CommRing R]
(r : R)
(s : R)
(f : RatFunc R)
[IsDomain R]
:
(RatFunc.laurent r) ((RatFunc.laurent s) f) = (RatFunc.laurent (r + s)) f