Finite PL homeomorphisms on compact plane polyhedra

This is the concrete PL category needed by Moise Chapters 5 and 6. A witness records a pure finite source complex on which an ambient homeomorphism is affine facewise. Common subdivision and pullback make these witnesses closed under symmetry and composition.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn (h : Plane ≃ₜ Plane) (A : Set Plane) : Type 1

An ambient homeomorphism is finitely PL on A, with an explicit pure source complex.

• complex : PlaneComplex

  The complex declaration.

• support_eq : self.complex.support = A
• pure : self.complex.IsPure2
• affineOn (s : Finset self.complex.Vertex) : s ∈ self.complex.simplexes → IsAffineOn (⇑h) (self.complex.cellCarrier s)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween (f : Plane → Plane) (A B : Set Plane) : Type 1

A finite PL homeomorphism between two compact plane polyhedra.

The underlying function need not be meaningful, continuous, or injective away from A; all geometric data is deliberately relative to the source support.

• complex : PlaneComplex

  The complex declaration.

• support_eq : self.complex.support = A
• pure : self.complex.IsPure2
• vertex_mem_support (v : self.complex.Vertex) : self.complex.position v ∈ self.complex.support
• affineOn (s : Finset self.complex.Vertex) : s ∈ self.complex.simplexes → IsAffineOn f (self.complex.cellCarrier s)
• injOn : Set.InjOn f A
• image_eq : f '' A = B

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.isPLOnSet {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : IsPLOnSet A f

Forget the explicit pure witness.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.continuousOn {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : ContinuousOn f A

def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.congrTarget {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {C : Set Plane} (hBC : B = C) : FinitePLHomeomorphBetween f A C

Reindex the certified target along a set equality.

Equations

• F.congrTarget hBC = { complex := F.complex, support_eq := ⋯, pure := ⋯, vertex_mem_support := ⋯, affineOn := ⋯, injOn := ⋯, image_eq := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.targetComplex {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : PlaneComplex

The target complex obtained by mapping every source face.

Equations

• F.targetComplex = F.complex.mapComplexOn f ⋯ ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.targetComplex_support {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : F.targetComplex.support = B

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.targetComplex_pure {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : F.targetComplex.IsPure2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.targetComplex_vertex_mem_support {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) (v : F.targetComplex.Vertex) : F.targetComplex.position v ∈ F.targetComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.inverseOn {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : Plane → Plane

A set-theoretic inverse, used only on the certified target polyhedron.

Equations

• F.inverseOn y = if hy : y ∈ B then Classical.choose ⋯ else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.inverseOn_mem {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {y : Plane} (hy : y ∈ B) : F.inverseOn y ∈ A

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.apply_inverseOn {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {y : Plane} (hy : y ∈ B) : f (F.inverseOn y) = y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.inverseOn_apply {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {x : Plane} (hx : x ∈ A) : F.inverseOn (f x) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.inverseOn_injOn {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) : Set.InjOn F.inverseOn B

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.inverseOn_affineOn_of_subdivides_targetComplex {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {R : PlaneComplex} (hR : R.Subdivides F.targetComplex) (s : Finset R.Vertex) : s ∈ R.simplexes → IsAffineOn F.inverseOn (R.cellCarrier s)

On a subdivision of the target complex, the certified inverse is affine facewise.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) (R : PlaneComplex) : Type 1

A common target refinement together with all data needed to pull it back through a finite PL homeomorphism. This is the relative-subdivision package used when a prescribed target mesh introduces new vertices on the boundary of a polygonal face.

• target : PlaneComplex

  The target declaration.

• target_support : self.target.support = B
• target_pure : self.target.IsPure2
• target_subdivides_certificate : self.target.Subdivides F.targetComplex
• target_subdivides_given : self.target.Subdivides R
• target_vertex_mem_support (v : self.target.Vertex) : self.target.position v ∈ self.target.support
• inverseAffine (s : Finset self.target.Vertex) : s ∈ self.target.simplexes → IsAffineOn F.inverseOn (self.target.cellCarrier s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.pullbackSubdivision {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) (R : PlaneComplex) (hRpure : R.IsPure2) (hRsupport : R.support = B) : F.PullbackSubdivision R

Pull a prescribed pure finite target mesh back through a certified finite PL homeomorphism. A common refinement is taken first, so no compatibility between the supplied mesh and the certificate's original target complex is required.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.inverseOn_injOn_target {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) : Set.InjOn F.inverseOn P.target.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.source {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) : PlaneComplex

The actual source complex obtained by mapping the common target refinement through the certified inverse. It has the same vertex and simplex labels as the target refinement.

Equations

• P.source = P.target.mapComplexOn F.inverseOn ⋯ ⋯ ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.source_simplexes {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) : P.source.simplexes = P.target.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.inverseOn_image_target {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} : F.inverseOn '' B = A

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.source_support {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) : P.source.support = A

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.source_pure {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) : P.source.IsPure2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.source_cellCarrier {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) (s : Finset P.target.Vertex) (hs : s ∈ P.target.simplexes) : P.source.cellCarrier s = F.inverseOn '' P.target.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.PullbackSubdivision.image_source_cellCarrier {f : Plane → Plane} {A B : Set Plane} {F : FinitePLHomeomorphBetween f A B} {R : PlaneComplex} (P : F.PullbackSubdivision R) (s : Finset P.target.Vertex) (hs : s ∈ P.target.simplexes) : f '' P.source.cellCarrier s = P.target.cellCarrier s

Corresponding source and target faces are carried exactly onto one another by the original map.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphBetween.transAmbient {f : Plane → Plane} {A B : Set Plane} (F : FinitePLHomeomorphBetween f A B) {h : Plane ≃ₜ Plane} (G : FinitePLHomeomorphOn h B) : FinitePLHomeomorphBetween (⇑h ∘ f) A (⇑h '' B)

Postcomposition by an ambient finite PL homeomorphism preserves finite PL cell homeomorphisms. A common target subdivision is pulled back through the first map.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.congrSet {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) {B : Set Plane} (hAB : A = B) : FinitePLHomeomorphOn h B

Reindex a finite PL witness along an equality of its underlying polyhedron.

Equations

• F.congrSet hAB = { complex := F.complex, support_eq := ⋯, pure := ⋯, affineOn := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.congrHomeomorph {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) {g : Plane ≃ₜ Plane} (hg : h = g) : FinitePLHomeomorphOn g A

Reindex a certificate along equality of ambient homeomorphisms.

Equations

• F.congrHomeomorph hg = hg ▸ F

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.isPLOnSet {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) : IsPLOnSet A ⇑h

Forget the explicit pure witness and retain the ordinary finite PL-on-set predicate.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.targetComplex {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) : PlaneComplex

The geometric target complex obtained by mapping source vertices and faces.

Equations

• F.targetComplex = F.complex.mapComplex ⇑h ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.targetComplex_support {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) : F.targetComplex.support = ⇑h '' A

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.targetComplex_pure {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) : F.targetComplex.IsPure2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.symm {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) : FinitePLHomeomorphOn h.symm (⇑h '' A)

The inverse homeomorphism is PL on the exact image polyhedron.

Equations

• F.symm = { complex := F.targetComplex, support_eq := ⋯, pure := ⋯, affineOn := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.refl (K : PlaneComplex) (hpure : K.IsPure2) : FinitePLHomeomorphOn (Homeomorph.refl Plane) K.support

Identity is affine on every face of an explicit pure complex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.refl K hpure = { complex := K, support_eq := ⋯, pure := hpure, affineOn := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.trans {h g : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) (G : FinitePLHomeomorphOn g (⇑h '' A)) : FinitePLHomeomorphOn (h.trans g) A

Finite PL witnesses compose. The proof takes a common target subdivision, pulls it back through the first homeomorphism, and composes the two affine witnesses face by face.

Equations

• F.trans G = { complex := ⋯.choose.toPlaneComplex.mapComplex ⇑h.symm ⋯ ⋯, support_eq := ⋯, pure := ⋯, affineOn := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.FinitePLHomeomorphOn.extendByIdentity {h : Plane ≃ₜ Plane} {A : Set Plane} (F : FinitePLHomeomorphOn h A) (hfix : Set.EqOn (⇑h) id Aᶜ) (K : PlaneComplex) (hKpure : K.IsPure2) : FinitePLHomeomorphOn h K.support

A finite PL homeomorphism supported on a compact patch is finite PL on every finite plane polyhedron. The source is cut by all barycentric lines of the patch. A resulting triangle which meets the patch interior lies in one patch triangle; on every other triangle continuity extends the identity from its interior to its closure.

Equations

• F.extendByIdentity hfix K hKpure = { complex := (K.toTriangleMesh.refineTo F.complex.toTriangleMesh).toPlaneComplex, support_eq := ⋯, pure := ⋯, affineOn := ⋯ }