Documentation

TauCeti.Geometry.Manifold.Complex.StructureSheaf.MeromorphicGerm

Meromorphic germs form the fraction field of holomorphic germs #

Let a : โ„‚ and let ๐’ช_a be the stalk at a of the holomorphic structure sheaf of โ„‚, an integral domain. Restricting a holomorphic germ to the punctured neighbourhoods of a gives a punctured meromorphic germ, which defines an injective ring homomorphism TauCeti.holomorphicStructureSheaf.toMeromorphicGerms a : ๐’ช_a โ†’+* meromorphicGerms โ„‚ a (toMeromorphicGerms_injective: by continuity a holomorphic germ is determined by its values off a). This file proves:

References #

source
noncomputable def TauCeti.holomorphicStructureSheaf.toMeromorphicGerms (a : โ„‚) :
โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a) โ†’+* โ†ฅ(meromorphicGerms โ„‚ a)

Restricting a holomorphic germ at a : โ„‚ to the punctured neighbourhoods of a gives a meromorphic germ at a.

Instances For
    source
    @[simp]
    theorem TauCeti.holomorphicStructureSheaf.coe_toMeromorphicGerms (a : โ„‚) (s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)) :
    โ†‘((toMeromorphicGerms a) s) = (toFilterGerm (modelWithCornersSelf โ„‚ โ„‚) โ„‚ a (nhdsWithin a {a}แถœ) โ‹ฏ) s
    source
    theorem TauCeti.holomorphicStructureSheaf.toMeromorphicGerms_injective (a : โ„‚) :
    Function.Injective โ‡‘(toMeromorphicGerms a)

    A holomorphic germ at a : โ„‚ is determined by its values on a punctured neighbourhood.

    source
    theorem TauCeti.holomorphicStructureSheaf.exists_toMeromorphicGerms_eq_of_analyticAt {a : โ„‚} {f : โ„‚ โ†’ โ„‚} (hf : AnalyticAt โ„‚ f a) :
    โˆƒ (s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)), โ†‘((toMeromorphicGerms a) s) = โ†‘f

    A function analytic at a : โ„‚ has a holomorphic germ at a, whose punctured germ is that of the function.

    source
    theorem TauCeti.holomorphicStructureSheaf.exists_toMeromorphicGerms_eq_iff {a : โ„‚} {f : โ„‚ โ†’ โ„‚} (hf : MeromorphicAt f a) :
    (โˆƒ (s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)), โ†‘((toMeromorphicGerms a) s) = โ†‘f) โ†” 0 โ‰ค meromorphicOrderAt f a

    A function meromorphic at a : โ„‚ has the punctured germ of a holomorphic germ at a exactly when its order at a is nonnegative.

    source
    theorem TauCeti.holomorphicStructureSheaf.mem_range_toMeromorphicGerms_iff_exists_tendsto {a : โ„‚} {ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)} :
    ฯ† โˆˆ (toMeromorphicGerms a).range โ†” โˆƒ (c : โ„‚), (โ†‘ฯ†).Tendsto (nhds c)

    Regular germs are those with a limit. A meromorphic germ at a comes from a holomorphic germ exactly when it has a limit along the punctured neighbourhoods of a.

    source
    theorem TauCeti.holomorphicStructureSheaf.exists_eq_toMeromorphicGerms_div (a : โ„‚) (ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)) :
    โˆƒ (h : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)) (p : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)) (n : โ„•), (โ†‘((toMeromorphicGerms a) p) = โ†‘fun (z : โ„‚) => (z - a) ^ n) โˆง ฯ† = (toMeromorphicGerms a) h / (toMeromorphicGerms a) p

    Every meromorphic germ at a : โ„‚ is the quotient of a holomorphic germ by a power of the coordinate z - a.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.holomorphicStructureSheaf.instAlgebraCarrierStalkCommRingCatPresheafComplexModelWithCornersSelfSubtypeGermNhdsWithinComplSetSingletonMemSubringMeromorphicGerms (a : โ„‚) :
    Algebra โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a) โ†ฅ(meromorphicGerms โ„‚ a)

    Meromorphic germs at a : โ„‚ form an algebra over the holomorphic germs at a, through toMeromorphicGerms.

    source
    @[simp]
    theorem TauCeti.holomorphicStructureSheaf.algebraMap_meromorphicGerms (a : โ„‚) :
    algebraMap โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a) โ†ฅ(meromorphicGerms โ„‚ a) = toMeromorphicGerms a
    source
    instance TauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms (a : โ„‚) :
    IsFractionRing โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a) โ†ฅ(meromorphicGerms โ„‚ a)

    The field of meromorphic germs at a : โ„‚ is the fraction field of the ring of holomorphic germs at a.

    The principal part and the regular part #

    source
    noncomputable def TauCeti.holomorphicStructureSheaf.regularPart (a : โ„‚) :
    โ†ฅ(meromorphicGerms โ„‚ a) โ†’+ โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)

    The regular part of a meromorphic germ ฯ† at a : โ„‚: the holomorphic germ which, restricted to the punctured neighbourhoods of a, is ฯ† - P((z - a)โปยน), where P is the principal part of ฯ†. It is additive in ฯ†.

    Instances For
      source
      @[simp]
      theorem TauCeti.holomorphicStructureSheaf.principalPart_toMeromorphicGerms {a : โ„‚} (s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)) :
      meromorphicGerms.principalPart ((toMeromorphicGerms a) s) = 0

      The principal part of a holomorphic germ vanishes.

      source
      theorem TauCeti.holomorphicStructureSheaf.toMeromorphicGerms_regularPart {a : โ„‚} (ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)) :
      (toMeromorphicGerms a) ((regularPart a) ฯ†) = ฯ† - (meromorphicGerms.evalInvSub a) (meromorphicGerms.principalPart ฯ†)

      On the punctured neighbourhoods of a, the regular part of ฯ† is ฯ† minus its principal part.

      source
      theorem TauCeti.holomorphicStructureSheaf.evalInvSub_principalPart_add_toMeromorphicGerms_regularPart {a : โ„‚} (ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)) :
      (meromorphicGerms.evalInvSub a) (meromorphicGerms.principalPart ฯ†) + (toMeromorphicGerms a) ((regularPart a) ฯ†) = ฯ†

      Principal part splitting. A meromorphic germ at a : โ„‚ is the sum of its principal part P((z - a)โปยน) and its regular part.

      source
      theorem TauCeti.holomorphicStructureSheaf.evalInvSub_add_toMeromorphicGerms_eq_iff {a : โ„‚} {ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)} {P : Polynomial โ„‚} (hP : P.coeff 0 = 0) {s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)} :
      (meromorphicGerms.evalInvSub a) P + (toMeromorphicGerms a) s = ฯ† โ†” meromorphicGerms.principalPart ฯ† = P โˆง (regularPart a) ฯ† = s

      Uniqueness of the principal part splitting. A meromorphic germ ฯ† at a : โ„‚ is P((z - a)โปยน) + s, with P a polynomial without constant term and s a holomorphic germ, exactly when P is the principal part and s is the regular part of ฯ†.

      source
      @[simp]
      theorem TauCeti.holomorphicStructureSheaf.regularPart_toMeromorphicGerms {a : โ„‚} (s : โ†‘((holomorphicStructureSheaf (modelWithCornersSelf โ„‚ โ„‚) โ„‚).presheaf.stalk a)) :
      (regularPart a) ((toMeromorphicGerms a) s) = s

      The regular part of a holomorphic germ is the germ itself.

      source
      theorem TauCeti.holomorphicStructureSheaf.mem_range_toMeromorphicGerms_iff_principalPart_eq_zero {a : โ„‚} {ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)} :
      ฯ† โˆˆ (toMeromorphicGerms a).range โ†” meromorphicGerms.principalPart ฯ† = 0

      A meromorphic germ at a comes from a holomorphic germ exactly when its principal part vanishes.

      source
      @[simp]
      theorem TauCeti.holomorphicStructureSheaf.toMeromorphicGerms_regularPart_evalInvSub {a : โ„‚} (P : Polynomial โ„‚) :
      (toMeromorphicGerms a) ((regularPart a) ((meromorphicGerms.evalInvSub a) P)) = (meromorphicGerms.evalInvSub a) (Polynomial.C (P.coeff 0))

      On the punctured neighbourhoods of a, the regular part of a polynomial in the inverse coordinate is its constant term.

      source
      @[simp]
      theorem TauCeti.holomorphicStructureSheaf.regularPart_evalInvSub {a : โ„‚} {P : Polynomial โ„‚} (hP : P.coeff 0 = 0) :
      (regularPart a) ((meromorphicGerms.evalInvSub a) P) = 0

      A polynomial without constant term in the inverse coordinate has regular part zero.

      source
      theorem TauCeti.holomorphicStructureSheaf.coe_toMeromorphicGerms_regularPart {a : โ„‚} {ฯ† : โ†ฅ(meromorphicGerms โ„‚ a)} {h : โ„‚ โ†’ โ„‚} (hh : AnalyticAt โ„‚ h a) {N : โ„•} (hฯ† : โ†‘ฯ† = โ†‘fun (z : โ„‚) => ((z - a) ^ N)โปยน * h z) :
      โ†‘((toMeromorphicGerms a) ((regularPart a) ฯ†)) = โ†‘((Function.swap dslope a)^[N] h)

      The regular part through Taylor's formula. If ฯ† is the germ of (z - a)โปแดบ h z with h analytic at a, then the regular part of ฯ† is the holomorphic germ of the remainder (swap dslope a)^[N] h in Taylor's formula h z = ฮฃ_{j<N} c_j (z - a) ^ j + (z - a) ^ N (swap dslope a)^[N] h z.