The gluing quotient of a nodal curve at its flag pairs #
A nodal curve is obtained by gluing smooth curves at pairs of points. The gluing data is recorded by flag pairs: a flag pair names two normalization components together with the point of each of them that is identified. This file builds the underlying topological space of such a curve, the gluing quotient, and records its basic properties.
The model is the following.
FlagPairDatais the gluing data: an arbitrary family of normalization componentsX i(indexed by the typeι) together with an arbitrary family of flag pairsf : Flag. A flag pair names the two componentsfst f,snd fand the pointsfstPt f,sndPt fof them that are identified. The data carry one hypothesis: the flag points are pairwise distinct (flagPointOf_injective'). The two points of one flag pair are different, and no point of the disjoint union occurs in two different flag pairs. This is what makes the data the data of a nodal curve and not of an arbitrary gluing of curves along points. Finiteness of the flag pairs is not assumed by the data: it is assumed, as[Finite Flag], by the finiteness of the flag points and of the node set, and -- together with the hypotheses that the components carry a topology and that they are T₁ -- by the closedness of the node set, the openness of the complement of the node set, the open embedding of the quotient map away from the flag points and the homeomorphism of the complement of the node set. The closedness of the generated relation and the Hausdorffness of the glued space ask the components to be Hausdorff. The number of components is not assumed to be finite either: the compactness of the glued space is not a separate declaration, it follows by instance inference from[Finite ι]together with[∀ i, CompactSpace (X i)].Σ i, X iis the disjoint union of the normalization components, with the coproduct topology. It is Hausdorff as soon as the components are (Mathlib'sSigma.t2Space).flagRelis the generating relation: the two points of one flag pair are related.- A flag point belongs to a unique flag pair (
eq_of_flagPoint_mem): two flag pairs never share a point of the disjoint union. Consequently any chain of flag pairs reduces to equality or to a single generating step (eq_of_flagRel_of_flagRel). Marking d Lrecords marks on the curve labelled byL: pairwise distinct points of the disjoint union, none of them a flag point. The flag points and marks lying on the componentX iare its special points (Marking.specialPoints).gluedRelis the equivalence relation generated by the flag pairs: it is "the two points are equal, or they are the two points of one flag pair", which isx = y ∨ flagRel d x y. It is symmetric and transitive (gluedRel_symm,gluedRel_trans), hence an equivalence relation (gluedRel_equivalence), and it relates two points only when they are equal or when both of them are flag points (eq_or_mem_flagPointSet_of_gluedRel). It is also exactly the equivalence closureRelation.EqvGenof the generating relation (gluedRel_iff_eqvGen). As a setoid it glues the two points of each flag pair (gluedRelSetoid_fstPoint_sndPoint), and glues the first point of a flag pair to nothing else (eq_or_eq_of_gluedRelSetoid_fstPoint).GluedCurveis the quotient of the disjoint union by that relation: the underlying space of the nodal curve. It is theQuotientof the disjoint union by the setoidgluedRelSetoid, with the quotient topology: a subset of the glued curve is open exactly when its inverse image under the quotient mapQuotient.mk (gluedRelSetoid d)is open in the disjoint union. The quotient map is continuous (continuous_quotient_mk') and identifies two points exactly when the generated relation relates them (Mathlib'sQuotient.eq). The glued curve is a quotient, so it has a lifting property: a map out of the disjoint union that takes the same value on the two points of every flag pair descends to a map out of the glued curve (GluedCurve.lift,GluedCurve.lift_mk,GluedCurve.continuous_lift).nodeSetis the image of the flag points in the glued curve. It is the image of the flag pairs undernodeOfFlag(nodeSet_eq_range_nodeOfFlag), it is finite (nodeSet_finite) and it is closed (isClosed_nodeSet). A point of the glued curve is a node exactly when it is the node of a flag pair (mem_nodeSet). The mapnodeOfFlagsends a flag pair to its node; two flag pairs have the same node exactly when they are the same flag pair (nodeOfFlag_inj), sonodeOfFlagis injective (nodeOfFlag_injective).- the complement of the node set is written
(nodeSet d)ᶜthroughout. It is open (isOpen_compl_nodeSet), and it is the image of the components minus their flag points under the quotient map (image_quotient_mk_compl). The quotient map restricts to a homeomorphism from the disjoint union of the normalization components minus their flag points onto the complement of the node set, because it is an open embedding there (quotientMapOnComplNodeSetHomeomorph).
The node set and its complement are intended to be the singular locus and the smooth locus of the nodal curve. This file only builds the underlying topological space, so the two names are names: nothing here is a statement about singularities or about smoothness.
References #
- Enrico Arbarello, Maurizio Cornalba, Phillip A. Griffiths, Geometry of Algebraic Curves, Volume II (Grundlehren der mathematischen Wissenschaften 331, Springer, 2007), Chapter X, "Nodal curves", for a nodal curve as obtained by gluing the normalization components at pairs of points, and for its dual graph.
- Qing Liu, Algebraic Geometry and Arithmetic Curves (Oxford Graduate Texts in Mathematics 6, 2002), §4.1, in particular §4.1.2 on the normalization, for the normalization of a curve and the finite map it induces to the curve.
TauCeti/Topology/Constructions/FiniteGluing.lean, the topological carrier of a nodal curve: the quotient of the normalization by the relation identifying each node flag with its partner. The closedness, the Hausdorffness and the open embedding of the quotient map used above are taken from that file.TauCeti/AlgebraicGeometry/Curves/DualGraph/Basic.lean, the dual graph of a nodal curve.
The point of the disjoint union selected by a flag pair and a boolean: false selects the
first point of the flag pair, true the second. This is the function whose injectivity is the
hypothesis on the gluing data.
Instances For
The flag point selected by false is the first point of the flag pair.
The flag point selected by true is the second point of the flag pair.
The gluing data of a nodal curve: the flag pairs at which the normalization components are
glued. A flag pair f names the two components fst f and snd f together with the points
fstPt f and sndPt f of those components that are identified.
The field flagPointOf_injective' says that the flag points are pairwise distinct: the two points
of one flag pair are different, and no point of the disjoint union occurs in two different flag
pairs. This is the hypothesis that makes the data the data of a nodal curve rather than of an
arbitrary gluing of curves along points.
The structure is bare gluing data: index maps and points on arbitrary types, with no topology and no curve structure.
- fst : Flag → ι
The first component glued at a flag pair.
- snd : Flag → ι
The second component glued at a flag pair.
- fstPt (f : Flag) : X (self.fst f)
The point of the first component at a flag pair.
- sndPt (f : Flag) : X (self.snd f)
The point of the second component at a flag pair.
- flagPointOf_injective' : Function.Injective (flagPointOf self.fst self.snd self.fstPt self.sndPt)
The flag points are pairwise distinct: the two points of one flag pair are different, and no point of the disjoint union occurs in two different flag pairs.
Instances For
The first point of a flag pair, as a point of the disjoint union of the components.
Instances For
The second point of a flag pair, as a point of the disjoint union of the components.
Instances For
The two points of a flag pair, selected by a boolean: false selects the first point of the
flag pair, true the second.
Instances For
The flag points are pairwise distinct. The points of the disjoint union that are glued -- the flag points -- are pairwise distinct: the two points of one flag pair are different, and no point occurs in two different flag pairs.
Two flag pairs with the same first point are the same flag pair.
Two flag pairs with the same second point are the same flag pair.
The first point of a flag pair is never the second point of a flag pair: a flag pair never pairs a point with itself.
The generating relation of the gluing: two points of the disjoint union are related when they
are the two points of one flag pair. Its characterisation is flagRel_def.
Instances For
The generating relation, characterised. Two points of the disjoint union are related by the generating relation exactly when they are the two points of one flag pair, in either order.
The generating relation is symmetric.
The flag pairs form a matching. Two flag relations that meet in a point glue the same two points: the flag points being pairwise distinct forces the two flag pairs to be equal, so every chain of flag pairs reduces to equality or to a single generating step.
The equivalence relation generated by the flag pairs. Two points of the disjoint union are
glued together exactly when they are equal, or when they are the two points of one flag pair.
Because the flag points are pairwise distinct, every chain of flag pairs reduces to equality or to
a single generating step, so this is exactly the relation generated by the flag pairs. Its
characterisation is gluedRel_def.
Instances For
The generated relation, characterised. Two points of the disjoint union are related by the generated relation exactly when they are equal or when they are the two points of one flag pair.
The glued relation is symmetric.
The glued relation is transitive.
The generating relation is contained in the glued relation.
The relation between two flag points. Two flag points of the disjoint union are related
by gluedRel exactly when they belong to the same flag pair.
The glued relation, as an equivalence relation.
The generated relation is the equivalence closure of the generating relation. The
equivalence relation gluedRel generated by the flag pairs is exactly Relation.EqvGen of the
generating relation flagRel: two points of the disjoint union are glued together precisely when
the generating relation relates them, or when they are equal.
The points of the disjoint union that occur in a flag pair: the range of the flag points.
Instances For
A point of the disjoint union is a flag point when it occurs in a flag pair.
The flag point set is the range of the flag points.
Flag points are the points glued to another point. A point of the disjoint union is a flag point exactly when the generating relation relates it to some point.
The partner of a flag point. The generating relation relates the flag points selected by
p and q exactly when they are the two points of one flag pair: q is p with its boolean
negated.
The flag points of d form a finite set.
Marks on a nodal curve presented by flag-pair data, labelled by L: pairwise distinct
points of the normalization, none of which is a flag point. These are the smooth marks of the
curve: their images in the glued curve avoid the nodes.
- point : L → (i : ι) × X i
The point of the normalization carrying a label.
- point_injective : Function.Injective self.point
Distinct labels mark distinct points.
- point_notMem_flagPointSet (l : L) : self.point l ∉ flagPointSet d
No mark is a flag point.
Instances For
The special points of the component i of a marked nodal curve: the points of X i which
are flag points or marks. They are the special flags on that component counted by the stability
condition 2 g_i - 2 + n_i > 0, the node branches being counted as flags.
Instances For
A point of the component i is special exactly when it is a flag point or a mark.
The generated relation relates two points of the disjoint union only when they are equal or when both of them are flag points.
The generated relation as a setoid: the equivalence relation on the disjoint union of the normalization components that glues the points of the flag pairs together.
Instances For
The relation of the setoid is the generated relation.
The two points of a flag pair are glued.
The first point of a flag pair is glued only to itself and to the second point.
The glued space. The quotient of the disjoint union of the normalization components by the generated relation: the underlying topological space of the nodal curve. The topology is the quotient topology, i.e. the finest topology making the quotient map continuous.
Instances For
The lifting property of the glued curve. A map out of the disjoint union of the normalization components that takes the same value on the two points of every flag pair descends to a map out of the glued curve: the glued curve is the quotient of the disjoint union by the relation identifying the two points of each flag pair.
Instances For
The lift is the original map on the representatives. The lift of g to the glued curve
agrees with g on the image of a point of the disjoint union.
The lift is unique. A map out of the glued curve that agrees with g on the images
of the points of the disjoint union is the lift of g.
A continuous map descends to a continuous map. The lift of a continuous map out of the disjoint union that is constant on the two points of every flag pair is continuous.
The node set. The image of the flag points in the glued curve. It is intended to be the singular locus of the nodal curve, but this file only builds the underlying topological space.
Instances For
The node set is the image of the flag points under the quotient map.
The node point of a flag pair: the image of its first point in the glued curve.
Instances For
The first point of a flag pair is sent to its node.
The second point of a flag pair is sent to the same node as the first one.
The flag point selected by p is sent to the node of its flag pair p.1.
The fibres of the flag-pair map. Two flag pairs have the same node exactly when they are
equal, so every non-empty fibre of nodeOfFlag is a singleton. The fibres over the points that
are not nodes are empty.
The flag-pair map to the node set is injective. Distinct flag pairs give distinct nodes, because the flag points are pairwise distinct.
The membership of the node set. A point of the glued curve is a node exactly when it is the node of a flag pair.
The node set is the image of the flag pairs. The node set of the glued curve is the image
of the flag pairs under nodeOfFlag.
The node set of the glued curve is finite: it is the image of the finite set of flag points.
The preimage of the node set. The quotient map sends a point of the disjoint union to a node exactly when that point is a flag point: the preimage of the node set is the flag point set.
The generated relation identifies only flag points. Two distinct points of the disjoint union are related by the generated relation only when the first of them is a flag point.
Flag pairs are the distinct points with the same image. Two points of the disjoint union are the two points of a flag pair exactly when they are distinct and are identified in the glued curve.
The quotient map is injective off the flag points. A point of the disjoint union which is not a flag point is the only point in its class in the glued curve.
The node set is closed. The node set of the glued curve is a closed subset of it, so its complement is open.
The complement of the node set is open, being the complement of the closed node set.
The image of the components minus their flag points. The quotient map sends the disjoint union of the normalization components minus their flag points onto the complement of the node set in the glued curve.
The generated relation is closed. The equivalence relation generated by the flag pairs is a closed subset of the product of the disjoint union of the normalization components with itself.
The glued space is Hausdorff. The quotient of the disjoint union of the normalization components by the generated relation is a Hausdorff space, when the components are Hausdorff and when there are finitely many flag pairs.
The quotient map is an open embedding away from the flag points. The quotient map restricted to the disjoint union of the normalization components minus their flag points is an open embedding.
The bundled homeomorphism of the complement of the node set. The quotient map, restricted to the points of the disjoint union that are not flag points, is a homeomorphism from them onto the complement of the node set in the glued curve.
Instances For
The bundled homeomorphism acts by the quotient map. On the complement of the flag points, the homeomorphism of the complement of the node set is the quotient map: it sends a point to its class in the glued curve.
The inverse of the bundled homeomorphism lands in the same class. The inverse of the homeomorphism of the complement of the node set sends a point of the complement to a point of the disjoint union that represents it in the glued curve.
Neighbourhoods of flag points #
Around a point with arbitrarily small connected punctured neighbourhoods there are arbitrarily small neighbourhoods meeting no other flag point whose punctured versions are connected.
If the flag points have connected punctured neighbourhoods, then the points which are not flag points are dense.