PL fillings of locally finite polygonal face boundaries

The globally coherent graph replacement gives every maximal face a PL map from the standard triangular frontier onto a simple polygonal circle. Polygonal Schoenflies fills that map by a finite PL homeomorphism without changing its shared-edge boundary values.

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

A certified finite PL filling of the canonical polygonal boundary of one locally finite face.

• map : Plane → Plane

  The map declaration.

• eqOn_boundary : Set.EqOn self.map (faceBoundaryMap f) (frontier standardFaceRegion)
• continuousOn : ContinuousOn self.map standardFaceRegion
• injectiveOn : Set.InjOn self.map standardFaceRegion
• image_eq : self.map '' standardFaceRegion = (facePolygonalCircle f).closedRegion
• isPLOnSet : IsPLOnSet standardFaceRegion self.map
• certificate : Nonempty (FinitePLHomeomorphBetween self.map standardFaceRegion (facePolygonalCircle f).closedRegion)

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

Polygonal Schoenflies fills the canonical face boundary by a finite PL homeomorphism.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePLFilling {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : FacePLFilling f

A fixed certified PL filling for downstream locally finite gluing.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePLFilling f = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePLFilling_eq_of_boundaryLift_eq {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {f g : K.Face} {p q : StandardFaceBoundary} (hpq : faceBoundaryLift f p = faceBoundaryLift g q) : (facePLFilling f).map ↑p = (facePLFilling g).map ↑q

Fillings of neighboring faces agree whenever their boundary lifts name the same global one-skeleton point.