Marked nodal curves with unordered auxiliary marks #
A marked nodal curve carries marks (NodalGluing.Marking), labelled by an arbitrary type:
pairwise distinct points of its normalization, none of them a flag point. Some of the marks are
distinguished and keep their ordering, labelled by a type N; the others are auxiliary,
labelled by a type R, and only the set of them matters. An isomorphism of such curves is an
isomorphism of nodal curves f together with a permutation π of the auxiliary labels, such that
f fixes every distinguished label and carries the auxiliary mark j to the auxiliary mark
π j. These arrows form a groupoid, the label-permutation extension of the groupoid of
isomorphisms preserving every label (a finite extension when R is finite): the ordered
isomorphisms are exactly the arrows with π = 1.
Because the auxiliary marks are pairwise distinct, the permutation is determined by the map of
curves (AuxiliaryIso.toIso_injective), so the arrows carry no data beyond the map. The arrows
with a fixed permutation form a torsor for the group of ordered automorphisms of the source
(AuxiliaryIso.permFiberEquiv). Hence when that group is finite and there are finitely many
auxiliary labels, every set of arrows is finite (AuxiliaryIso.finite). The finiteness of the
ordered automorphism group is a hypothesis here: for stable marked curves it is a theorem of the
analytic theory, which this file does not prove.
Main definitions #
The marks NodalGluing.Marking d L on the nodal curve presented by d, labelled by L, are
defined in TauCeti.AlgebraicGeometry.Curves.NodalGluing.Basic.
NodalGluing.AuxiliaryIso I n m m': the arrows(π, f)between curves with marksm : Marking d (N ⊕ R)andm' : Marking d' (N ⊕ R), with identityAuxiliaryIso.refl, compositeAuxiliaryIso.trans((ρ, h) ∘ (π, f) = (ρ ∘ π, h ∘ f)) and inverseAuxiliaryIso.symm.NodalGluing.AuxiliaryAut I n m: the automorphism group of a curve with unordered auxiliary marks, with its permutation action on the auxiliary labels (AuxiliaryAut.auxiliaryPerm), its forgetful map to the automorphisms of the nodal curve (AuxiliaryAut.toAut) and the subgroup of ordered automorphisms (AuxiliaryAut.ordered).NodalGluing.AuxiliaryMarkedCurve I n N R: the bundled curves withNdistinguished andRauxiliary marks, with the groupoid structureunorderedAuxiliaryIsomorphismGroupoidgiven by the arrows(π, f).
References #
- Joel W. Robbin and Dietmar A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699, for marked nodal Riemann surfaces and their isomorphisms (Definition 3.2) and for the finiteness of the automorphism group of a stable marked curve.
- Enrico Arbarello, Maurizio Cornalba, Phillip A. Griffiths, Geometry of Algebraic Curves, Volume II, Chapter X, for pointed nodal curves and their isomorphisms.
Arrows with unordered auxiliary marks #
structure
TauCeti.NodalGluing.AuxiliaryIso
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
(m : Marking d (N ⊕ R))
(m' : Marking d' (N ⊕ R))
:
Type (max (max (max (max u_14 u_4) u_6) u_7) u_9)
An isomorphism of curves with unordered auxiliary marks. The marks are labelled by
N ⊕ R: the labels in N are distinguished and ordered, those in R are auxiliary. An arrow
is a pair (π, f) of a permutation π of the auxiliary labels and an isomorphism f of nodal
curves which fixes every distinguished label and carries the auxiliary mark j to the auxiliary
mark π j.
- toIso : Iso I n d d'
The isomorphism of nodal curves.
- perm : Equiv.Perm R
The permutation of the auxiliary labels.
The isomorphism fixes every distinguished label.
The isomorphism carries the auxiliary mark
jto the auxiliary markperm j.
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryIso.instEquivLikeSigma
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
:
EquivLike (AuxiliaryIso I n m m') ((i : ι) × X i) ((i : ι') × X' i)
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.coe_toIso
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
The underlying isomorphism of nodal curves acts as the arrow.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.apply_inl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(a : N)
:
An arrow fixes every distinguished label.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.apply_inr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(j : R)
:
An arrow carries the auxiliary mark j to the auxiliary mark e.perm j.
theorem
TauCeti.NodalGluing.AuxiliaryIso.perm_apply_eq_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(j k : R)
:
The permutation is determined by the map. The permutation of an arrow sends j to k
exactly when the arrow carries the auxiliary mark j to the auxiliary mark k.
theorem
TauCeti.NodalGluing.AuxiliaryIso.ext
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{e e' : AuxiliaryIso I n m m'}
(h : ∀ (x : (i : ι) × X i), e x = e' x)
:
Two arrows agreeing at every point of the normalization are equal.
theorem
TauCeti.NodalGluing.AuxiliaryIso.ext_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{e e' : AuxiliaryIso I n m m'}
:
theorem
TauCeti.NodalGluing.AuxiliaryIso.toIso_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
:
An arrow is determined by its isomorphism of nodal curves: the permutation of the auxiliary labels is recovered from the map, because the auxiliary marks are pairwise distinct.
theorem
TauCeti.NodalGluing.AuxiliaryIso.apply_point
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(l : N ⊕ R)
:
An arrow maps marks exactly to marks of the same kind.
theorem
TauCeti.NodalGluing.AuxiliaryIso.image_image_point_inr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(S : Set R)
:
An arrow carries the auxiliary marks labelled by a set S exactly to the auxiliary marks
labelled by the image of S under its permutation.
noncomputable def
TauCeti.NodalGluing.AuxiliaryIso.refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
(m : Marking d (N ⊕ R))
:
AuxiliaryIso I n m m
The identity arrow, with the identity permutation.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.refl_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(x : (i : ι) × X i)
:
The identity arrow fixes every point.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.toIso_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The identity arrow is the identity isomorphism of nodal curves.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.perm_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The identity arrow has the identity permutation.
noncomputable def
TauCeti.NodalGluing.AuxiliaryIso.symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
AuxiliaryIso I n m' m
The inverse arrow (π⁻¹, f⁻¹).
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.symm_apply_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(x : (i : ι) × X i)
:
The inverse arrow undoes the arrow.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.apply_symm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(y : (i : ι') × X' i)
:
The arrow undoes its inverse.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.toIso_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
The isomorphism of nodal curves underlying the inverse arrow is the inverse isomorphism.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.perm_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
The permutation of the inverse arrow is the inverse permutation.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.symm_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
The inverse of the inverse is the original arrow.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.symm_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The inverse of the identity arrow is the identity.
noncomputable def
TauCeti.NodalGluing.AuxiliaryIso.trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
:
AuxiliaryIso I n m m''
The composite (ρ, h) ∘ (π, f) = (ρ ∘ π, h ∘ f) of two arrows.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.trans_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
(x : (i : ι) × X i)
:
The composite acts by applying the first arrow, then the second.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.toIso_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
:
The isomorphism of nodal curves underlying a composite is the composite isomorphism.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.perm_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
:
The permutation of a composite is the composite of the permutations.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.symm_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
:
The inverse of a composite is the composite of the inverses in the opposite order.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.self_trans_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
An arrow followed by its inverse is the identity.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.symm_trans_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
The inverse of an arrow followed by it is the identity.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.trans_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
Composing with the identity on the right does nothing.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.refl_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e : AuxiliaryIso I n m m')
:
Composing with the identity on the left does nothing.
theorem
TauCeti.NodalGluing.AuxiliaryIso.trans_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{ι'' : Type u_10}
{Flag'' : Type u_11}
{X'' : ι'' → Type u_12}
[(i : ι'') → TopologicalSpace (X'' i)]
[(i : ι'') → ChartedSpace H (X'' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{d'' : FlagPairData ι'' Flag'' X''}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
{m'' : Marking d'' (N ⊕ R)}
{ι₃ : Type u_15}
{Flag₃ : Type u_16}
{X₃ : ι₃ → Type u_17}
[(i : ι₃) → TopologicalSpace (X₃ i)]
[(i : ι₃) → ChartedSpace H (X₃ i)]
{d₃ : FlagPairData ι₃ Flag₃ X₃}
{m₃ : Marking d₃ (N ⊕ R)}
(e : AuxiliaryIso I n m m')
(e' : AuxiliaryIso I n m' m'')
(e'' : AuxiliaryIso I n m'' m₃)
:
Composition of arrows is associative.
The automorphism group #
@[reducible, inline]
abbrev
TauCeti.NodalGluing.AuxiliaryAut
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
(m : Marking d (N ⊕ R))
:
Type (max (max (max (max u_14 u_6) u_4) u_6) u_4)
The automorphism group of a curve with unordered auxiliary marks: its arrows (π, f) to
itself, with composition as multiplication. These are the isomorphisms of the nodal curve fixing
the distinguished labels and permuting the auxiliary marks, each with the permutation it
induces.
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryAut.instOne
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
One (AuxiliaryAut I n m)
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryAut.instMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
Mul (AuxiliaryAut I n m)
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryAut.instInv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
Inv (AuxiliaryAut I n m)
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryAut.instGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
Group (AuxiliaryAut I n m)
theorem
TauCeti.NodalGluing.AuxiliaryAut.mul_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e e' : AuxiliaryAut I n m)
:
Multiplication of automorphisms is composition, the right factor acting first.
theorem
TauCeti.NodalGluing.AuxiliaryAut.one_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The unit automorphism is the identity arrow.
theorem
TauCeti.NodalGluing.AuxiliaryAut.inv_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
:
The inverse automorphism is the inverse arrow.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.mul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e e' : AuxiliaryAut I n m)
(x : (i : ι) × X i)
:
A product of automorphisms acts by composition.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.one_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(x : (i : ι) × X i)
:
The unit automorphism fixes every point.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.inv_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
(x : (i : ι) × X i)
:
The inverse automorphism acts as the inverse arrow.
def
TauCeti.NodalGluing.AuxiliaryAut.auxiliaryPerm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The permutation action of the automorphism group on the auxiliary labels.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.auxiliaryPerm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
:
The permutation action of an automorphism is its permutation.
def
TauCeti.NodalGluing.AuxiliaryAut.toAut
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The automorphism of the nodal curve underlying an automorphism with auxiliary marks.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.toAut_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
:
The underlying automorphism of the nodal curve is the underlying isomorphism.
theorem
TauCeti.NodalGluing.AuxiliaryAut.toAut_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
:
The automorphism group with auxiliary marks is a subgroup of the automorphism group of the nodal curve: an automorphism is determined by its map of curves.
noncomputable def
TauCeti.NodalGluing.AuxiliaryAut.ordered
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
(m : Marking d (N ⊕ R))
:
Subgroup (AuxiliaryAut I n m)
The ordered automorphisms: the automorphisms fixing every label, distinguished or auxiliary. They are the kernel of the permutation action on the auxiliary labels.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryAut.mem_ordered_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
:
An automorphism is ordered exactly when its permutation of the auxiliary labels is trivial.
theorem
TauCeti.NodalGluing.AuxiliaryAut.mem_ordered_iff_forall
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{d : FlagPairData ι Flag X}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
(e : AuxiliaryAut I n m)
:
An automorphism is ordered exactly when it fixes every mark.
Arrows with a fixed permutation, and finiteness #
noncomputable def
TauCeti.NodalGluing.AuxiliaryIso.permFiberEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e₀ : AuxiliaryIso I n m m')
:
The arrows with a fixed permutation form a torsor for the ordered automorphisms. Given
one arrow e₀, an arrow e with the same permutation differs from e₀ by the ordered
automorphism e₀⁻¹ ∘ e of the source, and every ordered automorphism g of the source gives the
arrow e₀ ∘ g with the permutation of e₀.
Instances For
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.coe_permFiberEquiv_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e₀ : AuxiliaryIso I n m m')
(e : { e : AuxiliaryIso I n m m' // e.perm = e₀.perm })
:
The ordered automorphism attached to an arrow e with the permutation of e₀ is
e₀⁻¹ ∘ e.
@[simp]
theorem
TauCeti.NodalGluing.AuxiliaryIso.coe_permFiberEquiv_symm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
(e₀ : AuxiliaryIso I n m m')
(g : ↥(AuxiliaryAut.ordered I n m))
:
The arrow attached to an ordered automorphism g is e₀ ∘ g.
instance
TauCeti.NodalGluing.AuxiliaryIso.finite
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{ι : Type u_4}
{Flag : Type u_5}
{X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)]
{ι' : Type u_7}
{Flag' : Type u_8}
{X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)]
[(i : ι') → ChartedSpace H (X' i)]
{d : FlagPairData ι Flag X}
{d' : FlagPairData ι' Flag' X'}
{N : Type u_13}
{R : Type u_14}
{m : Marking d (N ⊕ R)}
{m' : Marking d' (N ⊕ R)}
[Finite R]
[Finite ↥(AuxiliaryAut.ordered I n m)]
:
Finite (AuxiliaryIso I n m m')
Finiteness of the arrows. If there are finitely many auxiliary labels and the source has
finitely many ordered automorphisms, then there are finitely many arrows between two curves with
unordered auxiliary marks. In particular the automorphism group AuxiliaryAut I n m is then
finite.
The groupoid #
structure
TauCeti.NodalGluing.AuxiliaryMarkedCurve
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
(N : Type u_15)
(R : Type u_16)
:
Type (max (max (max (max (max (u + 1) u_15) u_16) u_3) (v + 1)) (w + 1))
A nodal curve with N distinguished and R auxiliary marks, bundled: normalization
components X i indexed by ι, flag pairs indexed by Flag, and marks labelled by N ⊕ R.
The model I and the smoothness n do not enter the data; they select the arrows of the
groupoid unorderedAuxiliaryIsomorphismGroupoid, which are the C^n arrows (π, f).
- ι : Type u
The index type of the normalization components.
- Flag : Type v
The index type of the flag pairs.
The normalization components.
- topologicalSpace (i : self.ι) : TopologicalSpace (self.X i)
The topology of each normalization component.
- chartedSpace (i : self.ι) : ChartedSpace H (self.X i)
The charts of each normalization component.
- data : FlagPairData self.ι self.Flag self.X
The gluing data at the flag pairs.
The distinguished and auxiliary marks.
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.NodalGluing.AuxiliaryMarkedCurve.unorderedAuxiliaryIsomorphismGroupoid
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{N : Type u_13}
{R : Type u_14}
:
CategoryTheory.Groupoid (AuxiliaryMarkedCurve I n N R)
The groupoid of curves with unordered auxiliary marks. Its arrows are the pairs (π, f)
of AuxiliaryIso, composed by (ρ, h) ∘ (π, f) = (ρ ∘ π, h ∘ f). Its objects are the same as
those of the groupoid of isomorphisms preserving every label, of which it is the
label-permutation extension, a finite extension when R is finite.
theorem
TauCeti.NodalGluing.AuxiliaryMarkedCurve.id_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{N : Type u_13}
{R : Type u_14}
(C : AuxiliaryMarkedCurve I n N R)
:
The identity arrow of the groupoid is the identity arrow (1, id).
theorem
TauCeti.NodalGluing.AuxiliaryMarkedCurve.comp_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{N : Type u_13}
{R : Type u_14}
{C C' C'' : AuxiliaryMarkedCurve I n N R}
(e : C ⟶ C')
(e' : C' ⟶ C'')
:
Composition in the groupoid is composition of arrows (π, f).
theorem
TauCeti.NodalGluing.AuxiliaryMarkedCurve.inv_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
{N : Type u_13}
{R : Type u_14}
{C C' : AuxiliaryMarkedCurve I n N R}
(e : C ⟶ C')
:
The inverse in the groupoid is the inverse arrow (π⁻¹, f⁻¹).