Cellwise assembly for locally finite PL face fillings

This file transports every polygonal Schoenflies filling back to its native abstract face. A single compatibility package records the three geometric facts needed for global assembly: filled interiors are pairwise disjoint, the replacement graph misses every filled interior, and the family of filled closed regions is locally finite. Under these conditions the transported maps form a genuine locally finite triangle complex in the plane.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FacePLFilling.faceMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f : K.Face} (F : FacePLFilling f) : ↑(K.ClosedFace f) → Plane

A standard-triangle filling transported back to the native simplex of its source face.

Equations

• F.faceMap x = F.map ↑((K.facePlaneHomeomorph f) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FacePLFilling.continuous_faceMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f : K.Face} (F : FacePLFilling f) : Continuous F.faceMap

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FacePLFilling.injective_faceMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f : K.Face} (F : FacePLFilling f) : Function.Injective F.faceMap

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FacePLFilling.range_faceMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f : K.Face} (F : FacePLFilling f) : Set.range F.faceMap = (facePolygonalCircle f).closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FacePLFilling.mapsTo_interiorRegion {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f : K.Face} (F : FacePLFilling f) : Set.MapsTo F.map (interior standardFaceRegion) (facePolygonalCircle f).interiorRegion

The relative interior of a filled source face maps into the bounded complementary region of its polygonal boundary.

Boundary recognition from global barycentric coordinates

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_faceVertex_eq_of_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) {v : K.Vertex} (hv : v ∈ K.faceVertices f) : ∃ (i : ZMod 3), K.faceVertex f i = v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_faceEdge_eq_of_subset {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) : ∃ (i : ZMod 3), K.faceEdge f i = e

Every abstract edge contained in a maximal face is one of its three cyclic edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceChart_mem_frontier_of_extended_eq {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {f g : K.Face} (hfg : K.faceVertices f ≠ K.faceVertices g) {x : ↑(K.ClosedFace f)} {y : ↑(K.ClosedFace g)} (hxy : extendFaceCoordinates (K.faceVertices f) x = extendFaceCoordinates (K.faceVertices g) y) : ↑((K.facePlaneHomeomorph f) x) ∈ frontier standardFaceRegion

If equal global barycentric coordinates are represented on distinct vertex triples, the standard coordinate on the first triangle lies on its frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryLift_facePlaneHomeomorph {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (x : ↑(K.ClosedFace f)) (hp : ↑((K.facePlaneHomeomorph f) x) ∈ frontier standardFaceRegion) : ↑(faceBoundaryLift f ⟨↑((K.facePlaneHomeomorph f) x), hp⟩) = PlaneGraphRealization.faceToSupport f x

Lifting the standard coordinate of a boundary point recovers its original ambient support point.

Global cellwise compatibility

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CellwiseCompatibility {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Prop

The geometric conditions under which the independently chosen polygonal face fillings assemble to a locally finite plane complex. The first field rules out duplicate maximal-face labels; the remaining fields say that different filled cells meet only along the replacement graph and remain locally finite.

• faceVertices_injective : Function.Injective K.faceVertices
• graphAvoidsInteriors (f : K.Face) : Disjoint (Set.range G.graphReplacementMap) (facePolygonalCircle f).interiorRegion
• interiorsDisjoint (f g : K.Face) : f ≠ g → Disjoint (facePolygonalCircle f).interiorRegion (facePolygonalCircle g).interiorRegion
• closedRegions_mem_region (f : K.Face) : (facePolygonalCircle f).closedRegion ⊆ G.region
• locallyFiniteClosedRegions : LocallyFinite fun (f : K.Face) => {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CellwiseCompatibility.distinct_faceVertices {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) {f g : K.Face} (hfg : f ≠ g) : K.faceVertices f ≠ K.faceVertices g

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CellwiseCompatibility.faceMap_eq_iff {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) {f g : K.Face} {x : ↑(K.ClosedFace f)} {y : ↑(K.ClosedFace g)} : (facePLFilling f).faceMap x = (facePLFilling g).faceMap y ↔ extendFaceCoordinates (K.faceVertices f) x = extendFaceCoordinates (K.faceVertices g) y

The transported chosen fillings have exactly the same overlap relation as the original abstract triangles.

The assembled replacement complex

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementComplex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) : LocallyFiniteTriangleComplex ↑G.region

Replace every face of a locally finite complex by its coherent polygonal Schoenflies filling. The abstract vertices and faces are unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementComplex_faceVertices {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) : (polygonalReplacementComplex H).faceVertices f = K.faceVertices f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementComplex_faceMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) (x : ↑(K.ClosedFace f)) : ↑((polygonalReplacementComplex H).faceMap f x) = (facePLFilling f).faceMap x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementComplex_faceCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) : (polygonalReplacementComplex H).faceCarrier f = {q : ↑G.region | ↑q ∈ (facePolygonalCircle f).closedRegion}

The canonical homeomorphism onto the replacement

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : K.Face

A chosen maximal face containing a point of the support.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportFace p = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_faceCarrier_supportFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : ↑p ∈ K.faceCarrier (supportFace p)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportFacePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : ↑(K.ClosedFace (supportFace p))

Chosen barycentric coordinates for a support point in its chosen maximal face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportFacePoint p = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_supportFacePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : K.faceMap (supportFace p) (supportFacePoint p) = ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceInSupport_eq_preimage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : PlaneGraphRealization.faceInSupport f = Subtype.val ⁻¹' K.faceCarrier f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.locallyFinite_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : LocallyFinite PlaneGraphRealization.faceInSupport

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceImageInRegion {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : Set ↑G.region

The image of one source face, regarded as a subset of the permitted open plane region.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_faceImagesInRegion {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.faceImageInRegion

Source faces remain locally finite after passing through a realization which is closed relative to its perturbation region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.iUnion_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : ⋃ (f : K.Face), PlaneGraphRealization.faceInSupport f = Set.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isEmbedding_faceToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} [T2Space S] (f : K.Face) : Topology.IsEmbedding (PlaneGraphRealization.faceToSupport f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceToSupportHomeomorph {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} [T2Space S] (f : K.Face) : ↑(K.ClosedFace f) ≃ₜ ↑(PlaneGraphRealization.faceInSupport f)

A closed abstract face is homeomorphic to its carrier inside the whole support.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceToSupportHomeomorph f = ⋯.toHomeomorph

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceToSupportHomeomorph_apply {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} [T2Space S] (f : K.Face) (x : ↑(K.ClosedFace f)) : ↑((faceToSupportHomeomorph f) x) = PlaneGraphRealization.faceToSupport f x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) : ↑K.support → ↑(polygonalReplacementComplex H).support

The coherent cellwise filling as a map into the support of the assembled plane complex.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_faceToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) (x : ↑(K.ClosedFace f)) : polygonalReplacementMap H (PlaneGraphRealization.faceToSupport f x) = PlaneGraphRealization.faceToSupport f x

On every named source face, the global replacement map is the chosen face filling.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMapOnFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) (f : K.Face) : ↑(PlaneGraphRealization.faceInSupport f) → ↑(polygonalReplacementComplex H).support

The source face formula, expressed on a carrier subtype.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_polygonalReplacementMapOnFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) (f : K.Face) : Continuous (polygonalReplacementMapOnFace H f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_eqOn_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) (f : K.Face) (p : ↑(PlaneGraphRealization.faceInSupport f)) : polygonalReplacementMap H ↑p = polygonalReplacementMapOnFace H f p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_polygonalReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) : Continuous (polygonalReplacementMap H)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementInverse {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) : ↑(polygonalReplacementComplex H).support → ↑K.support

Read the old face map in coordinates chosen from a point of the replacement support.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementInverse_faceToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) (x : ↑(K.ClosedFace f)) : polygonalReplacementInverse H (PlaneGraphRealization.faceToSupport f x) = PlaneGraphRealization.faceToSupport f x

On every replacement face, the inverse is the original face parametrization.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementInverseOnFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) : ↑(PlaneGraphRealization.faceInSupport f) → ↑K.support

The inverse face formula on one replacement carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_polygonalReplacementInverseOnFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) : Continuous (polygonalReplacementInverseOnFace H f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementInverse_eqOn_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (f : K.Face) (p : ↑(PlaneGraphRealization.faceInSupport f)) : polygonalReplacementInverse H ↑p = polygonalReplacementInverseOnFace H f p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_polygonalReplacementInverse {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) : Continuous (polygonalReplacementInverse H)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementInverse_apply_map {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (p : ↑K.support) : polygonalReplacementInverse H (polygonalReplacementMap H p) = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_apply_inverse {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) (p : ↑(polygonalReplacementComplex H).support) : polygonalReplacementMap H (polygonalReplacementInverse H p) = p

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) : ↑K.support ≃ₜ ↑(polygonalReplacementComplex H).support

The source support and its coherent polygonal replacement are canonically homeomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph_mem_faceCarrier_iff {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} [T2Space S] (H : CellwiseCompatibility G) (f : K.Face) (p : ↑K.support) : ↑((polygonalReplacementHomeomorph H) p) ∈ (polygonalReplacementComplex H).faceCarrier f ↔ ↑p ∈ K.faceCarrier f

The canonical replacement homeomorphism preserves every named closed face exactly. This is stronger than preservation of the total support and is the bridge used when a finite family of replacement faces is pulled back to a finite source subcomplex.