Documentation

TauCeti.Geometry.Manifold.Complex.StructureSheaf.Node.LocalRing

The local ring of a node #

A node of a nodal complex curve is obtained by gluing a point p of one normalized component to a point q of another (or of the same) component. A function near the node is a pair of holomorphic germs, one on each branch, taking the same value at the node. This file defines the local ring of the node in exactly this form, directly from the holomorphic stalks of the two branches and without any hypersurface chart:

The definition and these properties hold for complex manifolds of any dimension. On complex curves a centered chart at each branch point gives the two coordinate germs nodeLocalRing.fstCoordinate and nodeLocalRing.sndCoordinate: a coordinate of one branch, extended by zero on the other. Their product is zero, so the node ring is not an integral domain, and together they generate the maximal ideal (nodeLocalRing.maximalIdeal_eq_span_coordinate). The kernel of each branch restriction is generated by the coordinate of the other branch. These are the relations xy = 0 and π”ͺ = (x, y) of the analytic local ring β„‚{x, y}/(xy) of the plane node, here derived from the branch description.

The fibre product of the two stalk evaluations is the concrete form of the pullback in CommRingCat described by Mathlib's CommRingCat.pullbackCone.

References #

source
noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
Subring (↑((holomorphicStructureSheaf I X).presheaf.stalk p) Γ— ↑((holomorphicStructureSheaf J Y).presheaf.stalk q))

The local ring of the node obtained by gluing p to q: pairs of holomorphic germs at the two branch points with equal values, under componentwise operations.

Instances For
    source
    @[simp]
    theorem TauCeti.holomorphicStructureSheaf.mem_nodeLocalRing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk p) Γ— ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) :
    f ∈ nodeLocalRing I J p q ↔ (eval I X p) f.1 = (eval J Y q) f.2

    A pair of branch germs is a germ at the node exactly when the two germs have equal values.

    source
    noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
    β†₯(nodeLocalRing I J p q) β†’+* ↑((holomorphicStructureSheaf I X).presheaf.stalk p)

    Restriction of a germ at the node to its branch at p.

    Instances For
      source
      noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
      β†₯(nodeLocalRing I J p q) β†’+* ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)

      Restriction of a germ at the node to its branch at q.

      Instances For
        source
        noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
        β†₯(nodeLocalRing I J p q) β†’+* β„‚

        The value of a germ at the node.

        Instances For
          source
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
          (fst I J p q) f = (↑f).1

          The first branch restriction is the first component of the pair of germs.

          source
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
          (snd I J p q) f = (↑f).2

          The second branch restriction is the second component of the pair of germs.

          source
          @[simp]
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
          (holomorphicStructureSheaf.eval I X p) ((fst I J p q) f) = (eval I J p q) f

          The value at the node is the value of the first branch germ at p.

          source
          @[simp]
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
          (holomorphicStructureSheaf.eval J Y q) ((snd I J p q) f) = (eval I J p q) f

          The value at the node is the value of the second branch germ at q.

          source
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.ext {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {f g : β†₯(nodeLocalRing I J p q)} (hfst : (fst I J p q) f = (fst I J p q) g) (hsnd : (snd I J p q) f = (snd I J p q) g) :
          f = g

          A germ at the node is determined by its two branch germs.

          source
          theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.ext_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {f g : β†₯(nodeLocalRing I J p q)} :
          f = g ↔ (fst I J p q) f = (fst I J p q) g ∧ (snd I J p q) f = (snd I J p q) g
          source
          def TauCeti.holomorphicStructureSheaf.nodeLocalRing.mk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (g : ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : (holomorphicStructureSheaf.eval I X p) f = (holomorphicStructureSheaf.eval J Y q) g) :
          β†₯(nodeLocalRing I J p q)

          Two branch germs with equal values glue to a germ at the node.

          Instances For
            source
            @[simp]
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_mk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (g : ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : (holomorphicStructureSheaf.eval I X p) f = (holomorphicStructureSheaf.eval J Y q) g) :
            (fst I J p q) (mk f g h) = f

            The first branch germ of a glued germ.

            source
            @[simp]
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_mk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (g : ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : (holomorphicStructureSheaf.eval I X p) f = (holomorphicStructureSheaf.eval J Y q) g) :
            (snd I J p q) (mk f g h) = g

            The second branch germ of a glued germ.

            source
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_surjective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
            Function.Surjective ⇑(fst I J p q)

            Every holomorphic germ on the first branch extends to a germ at the node.

            source
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_surjective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
            Function.Surjective ⇑(snd I J p q)

            Every holomorphic germ on the second branch extends to a germ at the node.

            source
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.finite_subtype {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
            (nodeLocalRing I J p q).subtype.Finite

            The product of the branch stalks is finite over the node ring.

            source
            theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval_surjective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
            Function.Surjective ⇑(eval I J p q)

            Every complex number is the value at the node of some germ.

            source
            noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.lift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {R : Type u_5} [CommRing R] (Ο† : R β†’+* ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (ψ : R β†’+* ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : βˆ€ (r : R), (holomorphicStructureSheaf.eval I X p) (Ο† r) = (holomorphicStructureSheaf.eval J Y q) (ψ r)) :
            R β†’+* β†₯(nodeLocalRing I J p q)

            The universal property of the node ring as a fibre product: two ring homomorphisms to the branch stalks with equal values at the node combine into a ring homomorphism to the node ring.

            Instances For
              source
              @[simp]
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_lift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {R : Type u_5} [CommRing R] (Ο† : R β†’+* ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (ψ : R β†’+* ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : βˆ€ (r : R), (holomorphicStructureSheaf.eval I X p) (Ο† r) = (holomorphicStructureSheaf.eval J Y q) (ψ r)) (r : R) :
              (fst I J p q) ((lift Ο† ψ h) r) = Ο† r

              The first branch germ of a lifted element.

              source
              @[simp]
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_lift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {R : Type u_5} [CommRing R] (Ο† : R β†’+* ↑((holomorphicStructureSheaf I X).presheaf.stalk p)) (ψ : R β†’+* ↑((holomorphicStructureSheaf J Y).presheaf.stalk q)) (h : βˆ€ (r : R), (holomorphicStructureSheaf.eval I X p) (Ο† r) = (holomorphicStructureSheaf.eval J Y q) (ψ r)) (r : R) :
              (snd I J p q) ((lift Ο† ψ h) r) = ψ r

              The second branch germ of a lifted element.

              source
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.ringHom_ext {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {R : Type u_5} [CommRing R] {Ο† ψ : R β†’+* β†₯(nodeLocalRing I J p q)} (hfst : (fst I J p q).comp Ο† = (fst I J p q).comp ψ) (hsnd : (snd I J p q).comp Ο† = (snd I J p q).comp ψ) :
              Ο† = ψ

              Ring homomorphisms to the node ring agree when both of their branch restrictions agree.

              source
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.lift_fst_comp_snd_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} {R : Type u_5} [CommRing R] (Ο† : R β†’+* β†₯(nodeLocalRing I J p q)) :
              lift ((fst I J p q).comp Ο†) ((snd I J p q).comp Ο†) β‹― = Ο†

              A ring homomorphism to the node ring is the lift of its two branch restrictions.

              source
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.isUnit_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
              IsUnit f ↔ (eval I J p q) f β‰  0

              A germ at the node is a unit exactly when its value at the node is nonzero.

              source
              instance TauCeti.holomorphicStructureSheaf.nodeLocalRing.isLocalHom_eval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              IsLocalHom (eval I J p q)

              Evaluation at the node detects units.

              source
              instance TauCeti.holomorphicStructureSheaf.nodeLocalRing.instIsLocalRing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              IsLocalRing β†₯(nodeLocalRing I J p q)

              The node ring is a local ring.

              source
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.nonunits_eq_ker_eval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              nonunits β†₯(nodeLocalRing I J p q) = ↑(RingHom.ker (eval I J p q))

              The nonunits of the node ring are exactly the germs vanishing at the node.

              source
              @[simp]
              theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.maximalIdeal_eq_ker_eval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              IsLocalRing.maximalIdeal β†₯(nodeLocalRing I J p q) = RingHom.ker (eval I J p q)

              The maximal ideal of the node ring consists of the germs vanishing at the node.

              source
              instance TauCeti.holomorphicStructureSheaf.nodeLocalRing.isLocalHom_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              IsLocalHom (fst I J p q)

              Restricting a germ at the node to its first branch is a local homomorphism.

              source
              instance TauCeti.holomorphicStructureSheaf.nodeLocalRing.isLocalHom_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} :
              IsLocalHom (snd I J p q)

              Restricting a germ at the node to its second branch is a local homomorphism.

              source
              noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.residueFieldEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners β„‚ E H) {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners β„‚ E' H') {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (p : X) (q : Y) :
              IsLocalRing.ResidueField β†₯(nodeLocalRing I J p q) ≃+* β„‚

              Evaluation identifies the residue field of the node ring with β„‚.

              Instances For
                source
                @[simp]
                theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.residueFieldEquiv_residue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners β„‚ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace β„‚ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners β„‚ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] {p : X} {q : Y} (f : β†₯(nodeLocalRing I J p q)) :
                (residueFieldEquiv I J p q) ((IsLocalRing.residue β†₯(nodeLocalRing I J p q)) f) = (eval I J p q) f

                The residue-field comparison sends the residue of a germ to its value at the node.

                Branch coordinates at a node of complex curves #

                source
                noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.fstCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q)

                A centered coordinate of the first branch, extended by zero on the second branch.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_fstCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                  (fst (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (fstCoordinate he hp) = e.holomorphicCoordinateGerm he p hp

                  The first branch germ of the first coordinate is the chart coordinate.

                  source
                  @[simp]
                  theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval_fstCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                  (eval (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (fstCoordinate he hp) = 0

                  The first branch coordinate vanishes at the node.

                  source
                  @[simp]
                  theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_fstCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                  (snd (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (fstCoordinate he hp) = 0

                  The first coordinate vanishes on the second branch.

                  source
                  theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fstCoordinate_ne_zero {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                  fstCoordinate he hp β‰  0

                  The first branch coordinate is nonzero.

                  source
                  theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.ker_snd_eq_span_fstCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) :
                  RingHom.ker (snd (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) = Ideal.span {fstCoordinate he hp}

                  The germs at the node vanishing on the second branch are the multiples of the first branch coordinate.

                  source
                  noncomputable def TauCeti.holomorphicStructureSheaf.nodeLocalRing.sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                  β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q)

                  A centered coordinate of the second branch, extended by zero on the first branch.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fst_sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    (fst (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (sndCoordinate he' hq) = 0

                    The second coordinate vanishes on the first branch.

                    source
                    @[simp]
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.snd_sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    (snd (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (sndCoordinate he' hq) = e'.holomorphicCoordinateGerm he' q hq

                    The second branch germ of the second coordinate is the chart coordinate.

                    source
                    @[simp]
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.eval_sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    (eval (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) (sndCoordinate he' hq) = 0

                    The second branch coordinate vanishes at the node.

                    source
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.sndCoordinate_ne_zero {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    sndCoordinate he' hq β‰  0

                    The second branch coordinate is nonzero.

                    source
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.ker_fst_eq_span_sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    RingHom.ker (fst (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) = Ideal.span {sndCoordinate he' hq}

                    The germs at the node vanishing on the first branch are the multiples of the second branch coordinate.

                    source
                    @[simp]
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.fstCoordinate_mul_sndCoordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    fstCoordinate he hp * sndCoordinate he' hq = 0

                    The two branch coordinates multiply to zero: the node equation xy = 0.

                    source
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.not_isDomain {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} :
                    Β¬IsDomain β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q)

                    The node ring has zero divisors, so it is not an integral domain.

                    source
                    @[simp]
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.mem_nonZeroDivisors_iff {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] (p : X) (q : Y) (f : β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q)) :
                    f ∈ nonZeroDivisors β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) ↔ (fst (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) f β‰  0 ∧ (snd (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) f β‰  0

                    A node germ is a nonzerodivisor exactly when both branch restrictions are nonzero.

                    source
                    theorem TauCeti.holomorphicStructureSheaf.nodeLocalRing.maximalIdeal_eq_span_coordinate {X Y : Type} [TopologicalSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] [TopologicalSpace Y] [ChartedSpace β„‚ Y] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 Y] {p : X} {q : Y} {e : OpenPartialHomeomorph X β„‚} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 X) (hp : p ∈ e.source) {e' : OpenPartialHomeomorph Y β„‚} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf β„‚ β„‚) 1 Y) (hq : q ∈ e'.source) :
                    IsLocalRing.maximalIdeal β†₯(nodeLocalRing (modelWithCornersSelf β„‚ β„‚) (modelWithCornersSelf β„‚ β„‚) p q) = Ideal.span {fstCoordinate he hp, sndCoordinate he' hq}

                    The maximal ideal of the node ring is generated by the two branch coordinates.