Edge valence of a triangle complex embedded in a surface #
An abstract finite family of triangles can embed in a surface only if at most two maximal triangles meet along any two-vertex edge. The proof is the local invariance-of-domain argument used implicitly in Moise's gluing theorem: two pages around an edge already form a planar neighborhood, so a third page approaching the same edge would have to enter their open image.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.edge_valence_le_two_of_isEmbedding
{S : Type u_1}
[TopologicalSpace S]
[ChartedSpace (EuclideanHalfSpace 2) S]
{V : Type u_2}
[Fintype V]
[DecidableEq V]
(F : Finset (Finset V))
(hcard : ∀ t ∈ F, t.card = 3)
(ι : ↑(GeometricRealization V F) → S)
(hι : Topology.IsEmbedding ι)
(e : Finset V)
(hecard : e.card = 2)
:
A finite family of abstract triangles carried by an embedded barycentric realization in a surface has edge valence at most two.