PL fillings of intrinsic polygonal face boundaries

The simultaneous intrinsic graph replacement gives every maximal face a canonical map from the standard triangular frontier onto a simple polygonal circle. IntrinsicFaceExtension proves that this map is genuinely PL on one named finite subdivision. Polygonal Schoenflies now fills it by a finite PL homeomorphism, without changing any shared-edge boundary values.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FacePLFilling {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Type

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

• map : Plane → Plane

  The map declaration.

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_facePLFilling {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Nonempty (FacePLFilling t)

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePLFilling {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : FacePLFilling t

A fixed choice of the certified PL filling for downstream finite gluing.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePLFilling t = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePLFilling_eq_of_boundaryLift_eq {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {t u : K.Face} {p q : StandardFaceBoundary} (hpq : ↑(faceBoundaryLift t p) = ↑(faceBoundaryLift u q)) : (facePLFilling t).map ↑p = (facePLFilling u).map ↑q

Fillings of neighboring faces agree wherever their standard boundary lifts name the same intrinsic one-skeleton point. The equality is pointwise because both restrictions are the same global graph replacement map.