Isomorphisms of nodal curves presented by flag-pair data

A nodal curve presented by flag-pair data d : FlagPairData ι Flag X is the quotient of the disjoint union Σ i, X i of its normalization components by the flag pairs. An isomorphism of two such curves is given on the normalizations: it is a diffeomorphism of the disjoint unions of the components which carries the two points of a flag pair exactly to the two points of a flag pair. For complex curves (𝕜 = ℂ and n = ∞) the diffeomorphism is a biholomorphism, so an isomorphism consists of component biholomorphisms together with the compatible maps of the dual graph.

This file defines these isomorphisms, extracts the combinatorial maps they induce, descends them to the glued curves and assembles the automorphism group.

Main definitions

• NodalGluing.Iso I n d d': a C^n diffeomorphism (Σ i, X i) ≃ₘ^n⟮I, I⟯ (Σ i, X' i) such that two points are the two points of a flag pair of d' exactly when their preimages are the two points of a flag pair of d.
• NodalGluing.Iso.branchEquiv: the induced bijection of branches Flag × Bool ≃ Flag' × Bool, characterized by flagPoint d' (e.branchEquiv p) = e (flagPoint d p). It commutes with exchanging the two branches of a node (branchEquiv_swap), so it may interchange them.
• NodalGluing.Iso.edgeEquiv: the induced bijection of nodes Flag ≃ Flag'.
• NodalGluing.Iso.vertexEquiv: for connected components, the induced bijection of components ι ≃ ι', compatible with the branches (fst_flagPoint_branchEquiv).
• NodalGluing.Iso.gluedCurveHomeomorph: the descended homeomorphism of glued curves.
• NodalGluing.Aut I n d: the automorphism group, with its actions on branches (Aut.branchPerm), nodes (Aut.edgePerm), components (Aut.vertexPerm) and the glued curve (Aut.toGluedCurveHomeomorph).

Main results

• NodalGluing.Iso.gluedCurveHomeomorph_mk, gluedCurveHomeomorph_nodeOfFlag: descent commutes with the quotient maps and sends the node of f to the node of e.edgeEquiv f; in particular it preserves the node set (image_gluedCurveHomeomorph_nodeSet).
• NodalGluing.Iso.gluedCurveHomeomorph_injective: descent is faithful as soon as the points which are not flag points are dense in the normalization, as they are for curves. So an isomorphism of normalizations is determined by the map of glued curves it induces.

References

• Joel W. Robbin and Dietmar A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699: a nodal Riemann surface is a surface with a set of unordered pairs of distinct points, and an isomorphism is a biholomorphism of the surfaces carrying the nodal pairs exactly to the nodal pairs.
• Enrico Arbarello, Maurizio Cornalba, Phillip A. Griffiths, Geometry of Algebraic Curves, Volume II, Chapter X, for the dual graph of a nodal curve and the action of automorphisms on it.

structure TauCeti.NodalGluing.Iso {𝕜 : 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') : Type (max (max (max u_4 u_6) u_7) u_9)

An isomorphism of nodal curves presented by flag-pair data. A C^n diffeomorphism of the disjoint unions of the normalization components which carries the two points of a flag pair of d exactly to the two points of a flag pair of d'. Over ℂ with n = ∞ this is a biholomorphism of the normalizations matching the nodes.

• toDiffeomorph : Diffeomorph I I ((i : ι) × X i) ((i : ι') × X' i) n

  The diffeomorphism of the normalizations.

• flagRel_apply_iff' (x y : (i : ι) × X i) : flagRel d' (self.toDiffeomorph x) (self.toDiffeomorph y) ↔ flagRel d x y

  Two points are the two points of a flag pair of d exactly when their images are the two points of a flag pair of d'.

@[instance_reducible]

noncomputable instance TauCeti.NodalGluing.Iso.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'} : EquivLike (Iso I n d d') ((i : ι) × X i) ((i : ι') × X' i)

@[simp]

theorem TauCeti.NodalGluing.Iso.coe_toDiffeomorph {𝕜 : 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'} (e : Iso I n d d') : ⇑e.toDiffeomorph = ⇑e

The underlying diffeomorphism of an isomorphism acts as the isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.coe_mk {𝕜 : 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'} (f : Diffeomorph I I ((i : ι) × X i) ((i : ι') × X' i) n) (hf : ∀ (x y : (i : ι) × X i), flagRel d' (f x) (f y) ↔ flagRel d x y) : ⇑{ toDiffeomorph := f, flagRel_apply_iff' := hf } = ⇑f

An isomorphism built from a diffeomorphism acts as that diffeomorphism.

theorem TauCeti.NodalGluing.Iso.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'} {e e' : Iso I n d d'} (h : ∀ (x : (i : ι) × X i), e x = e' x) : e = e'

Two isomorphisms agreeing at every point of the normalization are equal.

theorem TauCeti.NodalGluing.Iso.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'} {e e' : Iso I n d d'} : e = e' ↔ ∀ (x : (i : ι) × X i), e x = e' x

@[simp]

theorem TauCeti.NodalGluing.Iso.flagRel_apply_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'} (e : Iso I n d d') (x y : (i : ι) × X i) : flagRel d' (e x) (e y) ↔ flagRel d x y

An isomorphism carries the two points of a flag pair exactly to the two points of a flag pair.

theorem TauCeti.NodalGluing.Iso.continuous {𝕜 : 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'} (e : Iso I n d d') : Continuous ⇑e

An isomorphism is continuous on the normalizations.

noncomputable def TauCeti.NodalGluing.Iso.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) : Iso I n d d

The identity isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.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} (x : (i : ι) × X i) : (Iso.refl I n d) x = x

The identity isomorphism fixes every point.

@[simp]

theorem TauCeti.NodalGluing.Iso.refl_toDiffeomorph {𝕜 : 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} : (Iso.refl I n d).toDiffeomorph = Diffeomorph.refl I ((i : ι) × X i) n

The underlying diffeomorphism of the identity isomorphism is the identity.

noncomputable def TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : Iso I n d' d

The inverse isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') (x : (i : ι) × X i) : e.symm (e x) = x

The inverse isomorphism undoes the isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') (y : (i : ι') × X' i) : e (e.symm y) = y

The isomorphism undoes its inverse.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : e.symm.symm = e

The inverse of the inverse is the original isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.symm_toDiffeomorph {𝕜 : 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'} (e : Iso I n d d') : e.symm.toDiffeomorph = e.toDiffeomorph.symm

The underlying diffeomorphism of the inverse is the inverse diffeomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.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} : (Iso.refl I n d).symm = Iso.refl I n d

The inverse of the identity isomorphism is the identity.

theorem TauCeti.NodalGluing.Iso.symm_apply_eq {𝕜 : 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'} (e : Iso I n d d') {x : (i : ι) × X i} {y : (i : ι') × X' i} : e.symm y = x ↔ y = e x

The inverse isomorphism sends y to x exactly when the isomorphism sends x to y.

theorem TauCeti.NodalGluing.Iso.eq_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'} (e : Iso I n d d') {x : (i : ι) × X i} {y : (i : ι') × X' i} : x = e.symm y ↔ e x = y

The isomorphism sends x to y exactly when the inverse sends y to x.

noncomputable def TauCeti.NodalGluing.Iso.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''} (e : Iso I n d d') (e' : Iso I n d' d'') : Iso I n d d''

The composite of two isomorphisms.

@[simp]

theorem TauCeti.NodalGluing.Iso.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''} (e : Iso I n d d') (e' : Iso I n d' d'') (x : (i : ι) × X i) : (e.trans e') x = e' (e x)

The composite acts by applying the first isomorphism, then the second.

@[simp]

theorem TauCeti.NodalGluing.Iso.trans_toDiffeomorph {𝕜 : 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''} (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').toDiffeomorph = e.toDiffeomorph.trans e'.toDiffeomorph

The underlying diffeomorphism of a composite is the composite of the diffeomorphisms.

@[simp]

theorem TauCeti.NodalGluing.Iso.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''} (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').symm = e'.symm.trans e.symm

The inverse of a composite is the composite of the inverses in the opposite order.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : e.trans e.symm = Iso.refl I n d

An isomorphism followed by its inverse is the identity.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : e.symm.trans e = Iso.refl I n d'

The inverse of an isomorphism followed by it is the identity.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : e.trans (Iso.refl I n d') = e

Composing with the identity on the right does nothing.

@[simp]

theorem TauCeti.NodalGluing.Iso.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'} (e : Iso I n d d') : (Iso.refl I n d).trans e = e

Composing with the identity on the left does nothing.

theorem TauCeti.NodalGluing.Iso.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''} {ι₃ : Type u_13} {Flag₃ : Type u_14} {X₃ : ι₃ → Type u_15} [(i : ι₃) → TopologicalSpace (X₃ i)] [(i : ι₃) → ChartedSpace H (X₃ i)] {d₃ : FlagPairData ι₃ Flag₃ X₃} (e : Iso I n d d') (e' : Iso I n d' d'') (e'' : Iso I n d'' d₃) : (e.trans e').trans e'' = e.trans (e'.trans e'')

Composition of isomorphisms is associative.

@[simp]

theorem TauCeti.NodalGluing.Iso.apply_mem_flagPointSet_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'} (e : Iso I n d d') (x : (i : ι) × X i) : e x ∈ flagPointSet d' ↔ x ∈ flagPointSet d

An isomorphism maps flag points exactly to flag points.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedRel_apply_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'} (e : Iso I n d d') (x y : (i : ι) × X i) : gluedRel d' (e x) (e y) ↔ gluedRel d x y

An isomorphism respects the equivalence relation generated by the flag pairs.

Branches, nodes and components

noncomputable def TauCeti.NodalGluing.Iso.branchEquiv {𝕜 : 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'} (e : Iso I n d d') : Flag × Bool ≃ Flag' × Bool

The branch map. The bijection of branches induced by an isomorphism: the flag point selected by p is carried to the flag point selected by e.branchEquiv p.

@[simp]

theorem TauCeti.NodalGluing.Iso.flagPoint_branchEquiv {𝕜 : 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'} (e : Iso I n d d') (p : Flag × Bool) : flagPoint d' (e.branchEquiv p) = e (flagPoint d p)

The characteristic property of the branch map.

theorem TauCeti.NodalGluing.Iso.branchEquiv_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'} (e : Iso I n d d') (p : Flag × Bool) (q : Flag' × Bool) : e.branchEquiv p = q ↔ e (flagPoint d p) = flagPoint d' q

The branch map sends p to q exactly when the isomorphism sends the flag point of p to the flag point of q.

@[simp]

theorem TauCeti.NodalGluing.Iso.branchEquiv_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} : (Iso.refl I n d).branchEquiv = Equiv.refl (Flag × Bool)

The identity isomorphism fixes every branch.

@[simp]

theorem TauCeti.NodalGluing.Iso.branchEquiv_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'} (e : Iso I n d d') : e.symm.branchEquiv = e.branchEquiv.symm

The branch map of the inverse is the inverse of the branch map.

@[simp]

theorem TauCeti.NodalGluing.Iso.branchEquiv_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''} (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').branchEquiv = e.branchEquiv.trans e'.branchEquiv

The branch map of a composite is the composite of the branch maps.

theorem TauCeti.NodalGluing.Iso.branchEquiv_swap {𝕜 : 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'} (e : Iso I n d d') (p : Flag × Bool) : e.branchEquiv (p.1, !p.2) = ((e.branchEquiv p).1, !(e.branchEquiv p).2)

The branch map respects the nodes. The two branches of a node are carried to the two branches of a node: exchanging the branches commutes with the branch map.

noncomputable def TauCeti.NodalGluing.Iso.edgeEquiv {𝕜 : 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'} (e : Iso I n d d') : Flag ≃ Flag'

The node map. The bijection of nodes (flag pairs) induced by an isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Iso.fst_branchEquiv {𝕜 : 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'} (e : Iso I n d d') (p : Flag × Bool) : (e.branchEquiv p).1 = e.edgeEquiv p.1

The branch map lies over the node map.

theorem TauCeti.NodalGluing.Iso.edgeEquiv_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'} (e : Iso I n d d') (f : Flag) (b : Bool) : e.edgeEquiv f = (e.branchEquiv (f, b)).1

The node map sends a node to the node of the image of either of its branches.

@[simp]

theorem TauCeti.NodalGluing.Iso.edgeEquiv_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} : (Iso.refl I n d).edgeEquiv = Equiv.refl Flag

The identity isomorphism fixes every node.

@[simp]

theorem TauCeti.NodalGluing.Iso.edgeEquiv_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''} (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').edgeEquiv = e.edgeEquiv.trans e'.edgeEquiv

The node map of a composite is the composite of the node maps.

@[simp]

theorem TauCeti.NodalGluing.Iso.edgeEquiv_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'} (e : Iso I n d d') : e.symm.edgeEquiv = e.edgeEquiv.symm

The node map of the inverse is the inverse of the node map.

theorem TauCeti.NodalGluing.Iso.fst_apply_eq_fst_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'} [∀ (i : ι), PreconnectedSpace (X i)] (e : Iso I n d d') {x y : (i : ι) × X i} (h : x.fst = y.fst) : (e x).fst = (e y).fst

An isomorphism maps each connected component of the normalization into a single component.

noncomputable def TauCeti.NodalGluing.Iso.vertexEquiv {𝕜 : 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'} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] (e : Iso I n d d') : ι ≃ ι'

The component map. For connected components, the bijection of components induced by an isomorphism: the component i is carried onto the component e.vertexEquiv i.

@[simp]

theorem TauCeti.NodalGluing.Iso.fst_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'} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] (e : Iso I n d d') (x : (i : ι) × X i) : (e x).fst = e.vertexEquiv x.fst

The characteristic property of the component map.

theorem TauCeti.NodalGluing.Iso.fst_flagPoint_branchEquiv {𝕜 : 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'} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] (e : Iso I n d d') (p : Flag × Bool) : (flagPoint d' (e.branchEquiv p)).fst = e.vertexEquiv (flagPoint d p).fst

The graph maps are compatible. The component carrying the image of a branch is the image of the component carrying that branch.

theorem TauCeti.NodalGluing.Iso.vertexEquiv_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'} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] (e : Iso I n d d') (i : ι) (j : ι') : e.vertexEquiv i = j ↔ ∃ (x : X i), (e ⟨i, x⟩).fst = j

The component map sends i to j exactly when some point of the component i is sent into the component j.

@[simp]

theorem TauCeti.NodalGluing.Iso.vertexEquiv_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} [∀ (i : ι), ConnectedSpace (X i)] : (Iso.refl I n d).vertexEquiv = Equiv.refl ι

The identity isomorphism fixes every component.

@[simp]

theorem TauCeti.NodalGluing.Iso.vertexEquiv_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''} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] [∀ (i : ι''), ConnectedSpace (X'' i)] (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').vertexEquiv = e.vertexEquiv.trans e'.vertexEquiv

The component map of a composite is the composite of the component maps.

@[simp]

theorem TauCeti.NodalGluing.Iso.vertexEquiv_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'} [∀ (i : ι), ConnectedSpace (X i)] [∀ (i : ι'), ConnectedSpace (X' i)] (e : Iso I n d d') : e.symm.vertexEquiv = e.vertexEquiv.symm

The component map of the inverse is the inverse of the component map.

Descent to the glued curves

noncomputable def TauCeti.NodalGluing.Iso.gluedCurveHomeomorph {𝕜 : 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'} (e : Iso I n d d') : GluedCurve d ≃ₜ GluedCurve d'

Descent. The homeomorphism of glued curves induced by an isomorphism of nodal curves.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_mk {𝕜 : 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'} (e : Iso I n d d') (x : (i : ι) × X i) : e.gluedCurveHomeomorph ⟦x⟧ = ⟦e x⟧

The descended homeomorphism commutes with the quotient maps.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_nodeOfFlag {𝕜 : 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'} (e : Iso I n d d') (f : Flag) : e.gluedCurveHomeomorph (nodeOfFlag d f) = nodeOfFlag d' (e.edgeEquiv f)

The descended homeomorphism sends the node of f to the node of e.edgeEquiv f.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_mem_nodeSet_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'} (e : Iso I n d d') (q : GluedCurve d) : e.gluedCurveHomeomorph q ∈ nodeSet d' ↔ q ∈ nodeSet d

The descended homeomorphism maps nodes exactly to nodes.

theorem TauCeti.NodalGluing.Iso.image_gluedCurveHomeomorph_nodeSet {𝕜 : 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'} (e : Iso I n d d') : ⇑e.gluedCurveHomeomorph '' nodeSet d = nodeSet d'

The descended homeomorphism maps the node set onto the node set.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_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} : (Iso.refl I n d).gluedCurveHomeomorph = Homeomorph.refl (GluedCurve d)

Descent sends the identity to the identity.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_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''} (e : Iso I n d d') (e' : Iso I n d' d'') : (e.trans e').gluedCurveHomeomorph = e.gluedCurveHomeomorph.trans e'.gluedCurveHomeomorph

Descent sends a composite to the composite of the descended homeomorphisms.

@[simp]

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_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'} (e : Iso I n d d') : e.symm.gluedCurveHomeomorph = e.gluedCurveHomeomorph.symm

Descent sends the inverse to the inverse homeomorphism.

theorem TauCeti.NodalGluing.Iso.gluedCurveHomeomorph_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'} [∀ (i : ι'), T2Space (X' i)] (hd : Dense (flagPointSet d)ᶜ) : Function.Injective gluedCurveHomeomorph

Descent is faithful. If the points of the normalization which are not flag points are dense, then an isomorphism of nodal curves is determined by the homeomorphism of glued curves it induces. The density hypothesis holds for curves, whose components have no isolated points, by Dense.sdiff_finite.

@[reducible, inline]

abbrev TauCeti.NodalGluing.Aut {𝕜 : 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) : Type (max u_6 u_4)

The automorphism group of a nodal curve presented by flag-pair data: its isomorphisms with itself, with composition as multiplication.

@[instance_reducible]

noncomputable instance TauCeti.NodalGluing.Aut.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} : One (Aut I n d)

@[instance_reducible]

noncomputable instance TauCeti.NodalGluing.Aut.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} : Mul (Aut I n d)

@[instance_reducible]

noncomputable instance TauCeti.NodalGluing.Aut.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} : Inv (Aut I n d)

@[instance_reducible]

noncomputable instance TauCeti.NodalGluing.Aut.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} : Group (Aut I n d)

theorem TauCeti.NodalGluing.Aut.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} (e e' : Aut I n d) : e * e' = Iso.trans e' e

Multiplication of automorphisms is composition, the right factor acting first.

theorem TauCeti.NodalGluing.Aut.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} : 1 = Iso.refl I n d

The unit automorphism is the identity.

theorem TauCeti.NodalGluing.Aut.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} (e : Aut I n d) : e⁻¹ = Iso.symm e

The inverse automorphism is the inverse isomorphism.

@[simp]

theorem TauCeti.NodalGluing.Aut.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} (e e' : Aut I n d) (x : (i : ι) × X i) : (e * e') x = e (e' x)

A product of automorphisms acts by composition.

@[simp]

theorem TauCeti.NodalGluing.Aut.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} (x : (i : ι) × X i) : 1 x = x

The unit automorphism fixes every point.

@[simp]

theorem TauCeti.NodalGluing.Aut.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} (e : Aut I n d) (x : (i : ι) × X i) : e⁻¹ x = (Iso.symm e) x

The inverse automorphism acts as the inverse isomorphism.

noncomputable def TauCeti.NodalGluing.Aut.branchPerm {𝕜 : 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} : Aut I n d →* Equiv.Perm (Flag × Bool)

The branch action of the automorphism group: its action on the branches at the nodes.

@[simp]

theorem TauCeti.NodalGluing.Aut.branchPerm_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} (e : Aut I n d) : branchPerm e = Iso.branchEquiv e

The branch action of an automorphism is its branch map.

noncomputable def TauCeti.NodalGluing.Aut.edgePerm {𝕜 : 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} : Aut I n d →* Equiv.Perm Flag

The action of the automorphism group on the nodes.

@[simp]

theorem TauCeti.NodalGluing.Aut.edgePerm_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} (e : Aut I n d) : edgePerm e = Iso.edgeEquiv e

The node action of an automorphism is its node map.

noncomputable def TauCeti.NodalGluing.Aut.vertexPerm {𝕜 : 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} [∀ (i : ι), ConnectedSpace (X i)] : Aut I n d →* Equiv.Perm ι

The action of the automorphism group on the components, when they are connected.

@[simp]

theorem TauCeti.NodalGluing.Aut.vertexPerm_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} [∀ (i : ι), ConnectedSpace (X i)] (e : Aut I n d) : vertexPerm e = Iso.vertexEquiv e

The component action of an automorphism is its component map.

noncomputable def TauCeti.NodalGluing.Aut.toGluedCurveHomeomorph {𝕜 : 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} : Aut I n d →* GluedCurve d ≃ₜ GluedCurve d

The action of the automorphism group on the glued curve, by descent.

@[simp]

theorem TauCeti.NodalGluing.Aut.toGluedCurveHomeomorph_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} (e : Aut I n d) : toGluedCurveHomeomorph e = Iso.gluedCurveHomeomorph e

An automorphism acts on the glued curve by its descended homeomorphism.

theorem TauCeti.NodalGluing.Aut.toGluedCurveHomeomorph_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} [∀ (i : ι), T2Space (X i)] (hd : Dense (flagPointSet d)ᶜ) : Function.Injective ⇑toGluedCurveHomeomorph

The automorphism group acts faithfully on the glued curve when the points which are not flag points are dense in the normalization.