Stalks of the structure sheaf of a glued nodal curve

Let d be flag-pair gluing data on finitely many flag pairs, whose normalization components X i are Hausdorff charted spaces on a common complex model. The holomorphic structure sheaf of the glued curve NodalGluing.GluedCurve d is the quotient sheaf holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d) on the disjoint union Σ i, X i: holomorphic functions on the normalization with equal values at the two points of each flag pair. This file identifies its stalks.

• NodalGluing.quotientStalkBranchEquiv: at a point of the normalization which is not a flag point, the stalk of the glued curve is the holomorphic stalk of the normalization.
• NodalGluing.quotientStalkToNodeEquiv: at the node nodeOfFlag d f of a flag pair f, the stalk of the glued curve is the branch-pair node ring at fstPoint d f and sndPoint d f, the ring of pairs of holomorphic germs on the two branches with equal values at the node.

Both follow from the corresponding local statements for quotients of a complex manifold, holomorphicStructureSheaf.quotientStalkBranch_bijective and holomorphicStructureSheaf.quotientStalkToNode_bijective: finitely many flag points form a closed set, so near a flag pair nothing but its two points is identified.

References

• Joel W. Robbin and Dietmar A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), for the normalization description of nodal Riemann surfaces.

theorem TauCeti.NodalGluing.quotientStalkBranch_bijective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T1Space (X i)] {x : (i : ι) × X i} (hx : x ∉ flagPointSet d) : Function.Bijective ⇑(holomorphicStructureSheaf.quotientStalkBranch I (gluedRelSetoid d) ⟦x⟧ x ⋯)

Stalks at smooth points of a glued nodal curve. Away from the flag points, restriction to the normalization identifies the stalks of the glued curve with the holomorphic stalks of the normalization.

theorem TauCeti.NodalGluing.quotientStalkToNode_bijective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T2Space (X i)] (f : Flag) : Function.Bijective ⇑(holomorphicStructureSheaf.quotientStalkToNode I (gluedRelSetoid d) (fstPoint d f) (sndPoint d f) ⋯)

Stalks at the nodes of a glued nodal curve. At the node of a flag pair, the restrictions to the two branches identify the stalk of the glued curve with the branch-pair node ring.

noncomputable def TauCeti.NodalGluing.quotientStalkBranchEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T1Space (X i)] {x : (i : ι) × X i} (hx : x ∉ flagPointSet d) : ↑((holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d)).presheaf.stalk ⟦x⟧) ≃+* ↑((holomorphicStructureSheaf I ((i : ι) × X i)).presheaf.stalk x)

Away from the flag points, the stalk of the glued curve is the holomorphic stalk of the normalization.

@[simp]

theorem TauCeti.NodalGluing.quotientStalkBranchEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T1Space (X i)] {x : (i : ι) × X i} (hx : x ∉ flagPointSet d) (g : ↑((holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d)).presheaf.stalk ⟦x⟧)) : (quotientStalkBranchEquiv I d hx) g = (holomorphicStructureSheaf.quotientStalkBranch I (gluedRelSetoid d) ⟦x⟧ x ⋯) g

The stalk isomorphism at a smooth point is restriction to the branch.

noncomputable def TauCeti.NodalGluing.quotientStalkToNodeEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T2Space (X i)] (f : Flag) : ↑((holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d)).presheaf.stalk (nodeOfFlag d f)) ≃+* ↥(holomorphicStructureSheaf.nodeLocalRing I I (fstPoint d f) (sndPoint d f))

The stalk of the glued curve at the node of a flag pair is the branch-pair node ring.

@[simp]

theorem TauCeti.NodalGluing.quotientStalkToNodeEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)] (d : FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T2Space (X i)] (f : Flag) (g : ↑((holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d)).presheaf.stalk (nodeOfFlag d f))) : (quotientStalkToNodeEquiv I d f) g = (holomorphicStructureSheaf.quotientStalkToNode I (gluedRelSetoid d) (fstPoint d f) (sndPoint d f) ⋯) ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf.quotientSheaf I (gluedRelSetoid d)).presheaf.stalkSpecializes ⋯)) g)

The stalk isomorphism at a node is the pair of branch restrictions, after identifying the node with the class of the first point of the flag pair.