Documentation

LeanPool.ClassificationOfSurfaces.Moise.ChartPatch

A fixed polygonal patch inside the Rado chart models #

The four-triangle diamond below has vertices (+-3/4,0) and (0,+-3/4). It lies in the open unit disk and contains the closed radius-1/2 disk in its interior. Its right half gives the corresponding half-disk patch. These strict margins are the concrete base geometry for the Rado induction.

source
noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondLinearEquiv :
Plane ≃ₗ[ℝ] Plane

The anisotropic linear equivalence carrying Moise's fixed diamond, with vertices (+-1,0),(0,+-2), to the radius-3/4 axis diamond.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondAffineEquiv :
    Plane ≃ᵃ[ℝ] Plane

    Affine form of chartDiamondLinearEquiv.

    Equations
    Instances For
      source
      @[simp]
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondAffineEquiv_apply_zero (p : Plane) :
      (chartDiamondAffineEquiv p).ofLp 0 = 3 / 4 * p.ofLp 0
      source
      @[simp]
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondAffineEquiv_apply_one (p : Plane) :
      (chartDiamondAffineEquiv p).ofLp 1 = 3 / 8 * p.ofLp 1
      source
      @[simp]
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondAffineEquiv_symm_apply_zero (p : Plane) :
      (chartDiamondAffineEquiv.symm p).ofLp 0 = 4 / 3 * p.ofLp 0
      source
      @[simp]
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondAffineEquiv_symm_apply_one (p : Plane) :
      (chartDiamondAffineEquiv.symm p).ofLp 1 = 8 / 3 * p.ofLp 1
      source
      noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondMesh :
      TriangleMesh

      The fixed four-triangle chart patch.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondComplex :
        PlaneComplex

        The fixed chart patch as a pure plane complex.

        Equations
        Instances For
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondComplex_pure :
          chartDiamondComplex.IsPure2
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondComplex_support :
          chartDiamondComplex.support = ⇑chartDiamondAffineEquiv '' diamondPatch
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartDiamondComplex_support_subset_ball :
          chartDiamondComplex.support ⊆ Metric.ball 0 1

          The whole polygonal patch lies strictly inside the open unit disk.

          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.closedBall_half_subset_interior_chartDiamond :
          Metric.closedBall 0 (1 / 2) ⊆ interior chartDiamondComplex.support

          The closed radius-1/2 disk is contained in the interior of the polygonal patch.

          source
          @[reducible, inline]
          noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondMesh :
          TriangleMesh

          The two-triangle right half of the fixed chart diamond.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondComplex :
            PlaneComplex

            The right-half chart patch as a pure plane complex.

            Equations
            Instances For
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondComplex_pure :
              chartHalfDiamondComplex.IsPure2
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondComplex_support :
              chartHalfDiamondComplex.support = ⇑chartDiamondAffineEquiv '' diamondRightRegion
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondComplex_support_subset_modelRegion :
              chartHalfDiamondComplex.support ⊆ ChartKind.halfDisk.modelRegion
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondRightRegion_eq_patch_inter_nonneg :
              diamondRightRegion = diamondPatch ∩ {p : Plane | 0 ≤ p.ofLp 0}
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.halfCore_subset_chartHalfDiamond_support :
              ChartKind.halfDisk.modelCore ⊆ chartHalfDiamondComplex.support

              The closed radius-1/2 half-disk core is covered by the two-triangle half patch.

              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamond_support_eq_inter_halfPlane :
              chartHalfDiamondComplex.support = chartDiamondComplex.support ∩ HalfPlaneSet
              source
              def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondRightVertex :
              chartHalfDiamondComplex.Vertex

              In barycentric coordinates on the fixed half-diamond, the normal coordinate is exactly the weight of its unique positive-normal vertex, up to the fixed positive scale.

              Equations
              Instances For
                source
                theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamond_baryEval_coordZero (x : ↑(GeometricRealization chartHalfDiamondComplex.Vertex chartHalfDiamondComplex.cells)) :
                (chartHalfDiamondComplex.baryEval ↑x).ofLp 0 = 3 / 4 * ↑x chartHalfDiamondRightVertex
                source
                theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamond_baryEval_coordZero_eq_zero_iff (x : ↑(GeometricRealization chartHalfDiamondComplex.Vertex chartHalfDiamondComplex.cells)) :
                (chartHalfDiamondComplex.baryEval ↑x).ofLp 0 = 0 ↔ ↑x chartHalfDiamondRightVertex = 0
                source
                def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondUpperBoundaryEdge :
                Finset chartHalfDiamondComplex.Vertex

                The chartHalfDiamondUpperBoundaryEdge declaration.

                Equations
                Instances For
                  source
                  def LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamondLowerBoundaryEdge :
                  Finset chartHalfDiamondComplex.Vertex

                  The chartHalfDiamondLowerBoundaryEdge declaration.

                  Equations
                  Instances For
                    source
                    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartHalfDiamond_coordZero_iff_boundaryEdgeCarrier (x : ↑(GeometricRealization chartHalfDiamondComplex.Vertex chartHalfDiamondComplex.cells)) :
                    (chartHalfDiamondComplex.baryEval ↑x).ofLp 0 = 0 ↔ (∀ v ∉ chartHalfDiamondUpperBoundaryEdge, ↑x v = 0) ∨ ∀ v ∉ chartHalfDiamondLowerBoundaryEdge, ↑x v = 0
                    source
                    @[reducible, inline]
                    noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex :
                    ChartKind → PlaneComplex

                    The finite polygonal patch assigned to a disk or half-disk chart model.

                    Equations
                    Instances For
                      source
                      def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.IsModelBoundary (k : ChartKind) :
                      Plane → Prop

                      The model-boundary condition appropriate to a chart kind. A disk chart has no boundary stratum; in a half-disk chart it is the zero normal-coordinate line.

                      Equations
                      Instances For
                        source
                        noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchBoundaryEdges (k : ChartKind) :
                        Finset (Finset k.patchComplex.Vertex)

                        The explicit edge family carrying the model boundary in the fixed chart patch.

                        Equations
                        Instances For
                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_isModelBoundary_iff (k : ChartKind) (x : ↑(GeometricRealization k.patchComplex.Vertex k.patchComplex.cells)) :
                          k.IsModelBoundary (k.patchComplex.baryEval ↑x) ↔ ∃ e ∈ k.patchBoundaryEdges, ∀ v ∉ e, ↑x v = 0

                          The fixed patch meets its model boundary exactly in the carrier of patchBoundaryEdges.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_isModelBoundary_facewise (k : ChartKind) (t : Finset k.patchComplex.Vertex) :
                          t ∈ k.patchComplex.cells → ∃ b ⊆ t, b.card ≤ 2 ∧ ∀ (x : ↑(GeometricRealization k.patchComplex.Vertex k.patchComplex.cells)), (∀ v ∉ t, ↑x v = 0) → (k.IsModelBoundary (k.patchComplex.baryEval ↑x) ↔ ∀ v ∉ b, ↑x v = 0)

                          Facewise exposed form of the fixed patch boundary. Every patch triangle meets the model boundary in an intrinsic face of cardinality at most two.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.mem_patchComplex_edges_of_mem_patchBoundaryEdges (k : ChartKind) {e : Finset k.patchComplex.Vertex} (he : e ∈ k.patchBoundaryEdges) :
                          e ∈ k.patchComplex.cells.biUnion fun (t : Finset k.patchComplex.Vertex) => Finset.powersetCard 2 t

                          Every explicitly designated patch-boundary edge is an edge of the patch complex.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_pure (k : ChartKind) :
                          k.patchComplex.IsPure2
                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanTriangles_isDualConnected :
                          TriangleFamily.IsDualConnected diamondFanTriangles

                          The four triangles in the fixed disk-chart patch have a connected dual graph.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiamondTriangles_isDualConnected :
                          TriangleFamily.IsDualConnected ({t ∈ diamondFanTriangles | 1 ∈ t})

                          The two triangles in the fixed half-disk-chart patch have a connected dual graph.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_isDualConnected (k : ChartKind) :
                          TriangleFamily.IsDualConnected k.patchComplex.cells

                          Every fixed chart patch starts with a connected dual graph.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_support_subset_modelRegion (k : ChartKind) :
                          k.patchComplex.support ⊆ k.modelRegion
                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelCore_subset_patchComplex_support (k : ChartKind) :
                          k.modelCore ⊆ k.patchComplex.support
                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelCore_subset_interior_patchInRegion (k : ChartKind) :
                          {p : ↑k.modelRegion | ↑p ∈ k.modelCore} ⊆ interior {p : ↑k.modelRegion | ↑p ∈ k.patchComplex.support}

                          In model-region topology, the fixed chart core lies in the interior of the fixed polygonal patch. In the half-disk case this is relative interior, so edge-line core points are included.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanTriangles_edge_valence (e : Finset (Fin 5)) (he : e.card = 2) :
                          {t ∈ diamondFanTriangles | e ⊆ t}.card ≤ 2

                          Finite valence check for the four-triangle diamond fan.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiamondTriangles_edge_valence (e : Finset (Fin 5)) :
                          {t ∈ {t ∈ diamondFanTriangles | 1 ∈ t} | e ⊆ t}.card ≤ 2

                          Finite valence check for the two-triangle half-diamond fan.

                          source
                          theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchComplex_edge_valence (k : ChartKind) (e : Finset k.patchComplex.Vertex) (he : e.card = 2) :
                          {t ∈ k.patchComplex.cells | e ⊆ t}.card ≤ 2