The one-sided-degenerate P2 disk model

The ordinary P2 model glues two polygons along a marked side, with at least one old side on each child. Cancellation in the Gallier--Xu normalization also uses the limiting case in which one child is a monogon. This file supplies a concrete model for that case.

The local target is a polynomial teardrop. The map

z ↦ (1 - z) ^ 2

is injective on the closed unit disk: translating by 1 puts the disk in a closed half-plane, on which squaring has no nontrivial antipodal pair. Its image is star-shaped at the cusp. A scaled copy receives the monogon, while the other child fills the collar between that copy and the full teardrop.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.norm_le_one {n : ℕ} (z : PolygonCell n) : ‖z.val‖ ≤ 1

Every polygon cell has the closed-unit-disk norm bound.

def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap {n : ℕ} (z : PolygonCell n) : ℂ

The polynomial disk used as the target of the degenerate two-child gluing.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap z = (1 - z.val) ^ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_teardropMap {n : ℕ} : Continuous teardropMap

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.eq_one_of_re_eq_one {n : ℕ} (z : PolygonCell n) (hre : z.val.re = 1) : z.val = 1

A point of the closed unit disk with real part 1 is the cusp point 1.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap_injective {n m : ℕ} {z : PolygonCell n} {w : PolygonCell m} (h : teardropMap z = teardropMap w) : z.val = w.val

Squaring after translation by 1 is injective on the closed unit disk.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.Teardrop : Set ℂ

The teardrop image, equipped with the subspace topology inherited from the plane.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.Teardrop = Set.range LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap

def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.toTeardrop (z : PolygonCell 1) : ↑Teardrop

The polynomial map as a map into its exact range.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.toTeardrop z = ⟨LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap z, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_toTeardrop : Continuous toTeardrop

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.toTeardrop_bijective : Function.Bijective toTeardrop

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropHomeomorph : PolygonCell 1 ≃ₜ ↑Teardrop

The closed disk is homeomorphic to its polynomial teardrop image.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropHomeomorph_apply_val (z : PolygonCell 1) : ↑(teardropHomeomorph z) = teardropMap z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.one_sub_smul_mem_closedBall (z : PolygonCell 1) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : ‖1 - ↑s * (1 - z.val)‖ ≤ 1

Contracting the translated disk toward its cusp stays in the translated disk.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.smul_teardropMap_mem_range (z : PolygonCell 1) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : ↑s * teardropMap z ∈ Set.range teardropMap

Every radial contraction of a teardrop point is again a teardrop point.

The monogon and collar maps

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap (z : PolygonCell 1) : ℂ

The monogon occupies the inner radial half of the teardrop.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap z = ↑2⁻¹ * LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_monogonMap : Continuous monogonMap

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap_mem_teardrop (z : PolygonCell 1) : monogonMap z ∈ Set.range teardropMap

Half of a teardrop point is still in the full teardrop.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight (z : PolygonCell 2) : ℝ

The nonnegative height of the upper circular boundary above a fixed real coordinate.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight z = √(1 - z.val.re ^ 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.re_sq_le_one (z : PolygonCell 2) : z.val.re ^ 2 ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight_nonneg (z : PolygonCell 2) : 0 ≤ chordHeight z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight_sq (z : PolygonCell 2) : chordHeight z ^ 2 = 1 - z.val.re ^ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.neg_chordHeight_le_im (z : PolygonCell 2) : -chordHeight z ≤ z.val.im

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.im_le_chordHeight (z : PolygonCell 2) : z.val.im ≤ chordHeight z

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue (z : PolygonCell 2) : ℂ

The lower unit-circle point on the vertical chord through a digon point, squared so that the two chord endpoints sweep the teardrop boundary once.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue z = (↑z.val.re - ↑(LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight z) * Complex.I) ^ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue_norm (z : PolygonCell 2) : ‖collarCircleValue z‖ = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint (z : PolygonCell 2) : PolygonCell 1

The collar's boundary-direction point, bundled as a point of the unit disk.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint z = { val := LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue z, property := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_chordHeight : Continuous chordHeight

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_collarCircleValue : Continuous collarCircleValue

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_collarCirclePoint : Continuous collarCirclePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardropMap_collarCirclePoint (z : PolygonCell 2) : teardropMap (collarCirclePoint z) = -4 * ↑(chordHeight z) ^ 2 * collarCircleValue z

The teardrop boundary value of the collar direction has an exact quadratic factor.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap (z : PolygonCell 2) : ℂ

The digon fills the radial collar between the half-size and full teardrop boundaries.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_collarMap : Continuous collarMap

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_eq_smul_teardropMap (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : collarMap z = ↑((3 * chordHeight z ^ 2 - chordHeight z * z.val.im) / (4 * chordHeight z ^ 2)) * teardropMap (collarCirclePoint z)

Away from the two chord tips, the collar map is a radial teardrop value with scale in [1/2, 1].

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarScale_nonneg (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : 0 ≤ (3 * chordHeight z ^ 2 - chordHeight z * z.val.im) / (4 * chordHeight z ^ 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarScale_le_one (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : (3 * chordHeight z ^ 2 - chordHeight z * z.val.im) / (4 * chordHeight z ^ 2) ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_mem_teardrop (z : PolygonCell 2) : collarMap z ∈ Set.range teardropMap

Exact compatibility on the fresh seam

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_eq_monogonMap_collarCirclePoint_of_im_eq (z : PolygonCell 2) (hy : z.val.im = chordHeight z) : collarMap z = monogonMap (collarCirclePoint z)

On the upper circular boundary of the digon, the collar meets the half-size teardrop occupied by the monogon.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.side_zero_digon_val (t : ↑unitInterval) : ((PolygonCell.side 0) t).val = ↑(Circle.exp (Real.pi * ↑t))

Side zero of the digon is the upper semicircle with its usual angle parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.side_zero_digon_im (t : ↑unitInterval) : ((PolygonCell.side 0) t).val.im = Real.sin (Real.pi * ↑t)

The imaginary coordinate on side zero of the digon.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight_side_zero_digon (t : ↑unitInterval) : chordHeight ((PolygonCell.side 0) t) = Real.sin (Real.pi * ↑t)

The chord height agrees with the imaginary coordinate on the upper digon side.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint_side_zero_digon_symm (t : ↑unitInterval) : collarCirclePoint ((PolygonCell.side 0) (unitInterval.symm t)) = (PolygonCell.side 0) t

Squaring the lower endpoint of an upper digon chord gives the corresponding monogon boundary point.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap_fresh_seam (t : ↑unitInterval) : monogonMap ((PolygonCell.side 0) t) = collarMap ((PolygonCell.side 0) (unitInterval.symm t))

The analytic child map respects the exact reversed fresh-side parameter used by P2.

Descending the base child pair to the teardrop

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.BaseChildPair : Type

The base one-sided-degenerate child pair: a monogon and a digon.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.BaseChildPair = LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildPair 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap : BaseChildPair → ↑Teardrop

Map both children into their complementary regions of the teardrop.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap (Sum.inl z) = ⟨LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap z, ⋯⟩
• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap (Sum.inr z) = ⟨LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap z, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.continuous_baseChildPairMap : Continuous baseChildPairMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap_inl (z : PolygonCell 1) : ↑(baseChildPairMap (Sum.inl z)) = monogonMap z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap_inr (z : PolygonCell 2) : ↑(baseChildPairMap (Sum.inr z)) = collarMap z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap_eq_of_generator {x y : BaseChildPair} (hxy : DiskSquare.ParamChildSeamGenerator 0 1 x y) : baseChildPairMap x = baseChildPairMap y

The child-pair map is constant on the generating fresh seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap_respects {x y : BaseChildPair} (hxy : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) x y) : baseChildPairMap x = baseChildPairMap y

The child-pair map is constant on the equivalence relation generated by the fresh seam.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingMap : C(DiskSquare.ParamChildGluing 0 1, ↑Teardrop)

The continuous analytic map induced on the one-sided-degenerate child quotient.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingMap_mk (x : BaseChildPair) : baseChildGluingMap (Quotient.mk'' x) = baseChildPairMap x

The collar has no hidden interior identifications

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarRadius (z : PolygonCell 2) : ℝ

The nonnegative radial magnitude used by the collar map.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.two_mul_chordHeight_sq_le_collarRadius (z : PolygonCell 2) : 2 * chordHeight z ^ 2 ≤ collarRadius z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarRadius_nonneg (z : PolygonCell 2) : 0 ≤ collarRadius z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarRadius_pos (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : 0 < collarRadius z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_eq_neg_radius_mul (z : PolygonCell 2) : collarMap z = -↑(collarRadius z) * collarCircleValue z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.norm_collarMap (z : PolygonCell 2) : ‖collarMap z‖ = collarRadius z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue_eq_of_collarMap_eq (z w : PolygonCell 2) (hz : chordHeight z ≠ 0) (hzw : collarMap z = collarMap w) : collarCircleValue z = collarCircleValue w

Equal non-tip collar values have the same boundary direction.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.lowerChordValue (z : PolygonCell 2) : ℂ

The lower unit-circle representatives used by the squaring map.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.lowerChordValue z = ↑z.val.re - ↑(LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight z) * Complex.I

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCircleValue_eq_lowerChordValue_sq (z : PolygonCell 2) : collarCircleValue z = lowerChordValue z ^ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.lowerChordValue_im (z : PolygonCell 2) : (lowerChordValue z).im = -chordHeight z

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.lowerChordValue_re (z : PolygonCell 2) : (lowerChordValue z).re = z.val.re

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.lowerChordValue_eq_of_collarCircleValue_eq (z w : PolygonCell 2) (hz : chordHeight z ≠ 0) (hzw : collarCircleValue z = collarCircleValue w) : lowerChordValue z = lowerChordValue w

Squaring is injective on the open lower semicircle used by non-tip collar chords.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_injective_of_chordHeight_ne_zero (z w : PolygonCell 2) (hz : chordHeight z ≠ 0) (hzw : collarMap z = collarMap w) : z = w

The collar is injective away from its two pinched tips.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight_eq_zero_of_collarRadius_eq_zero (z : PolygonCell 2) (hradius : collarRadius z = 0) : chordHeight z = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.eq_side_zero_or_side_one_of_chordHeight_eq_zero (z : PolygonCell 2) (hs : chordHeight z = 0) : z = (PolygonCell.side 0) 0 ∨ z = (PolygonCell.side 0) 1

The only zero-height digon points are the two endpoints of its upper side.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.inr_tip_eqv_inl_monogon_basepoint (z : PolygonCell 2) (hs : chordHeight z = 0) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) (Sum.inr z) (Sum.inl ((PolygonCell.side 0) 0))

Either collar tip is identified with the monogon basepoint by the generated seam relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPair_eqvGen_inr_inr_of_map_eq (z w : PolygonCell 2) (hzw : collarMap z = collarMap w) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) (Sum.inr z) (Sum.inr w)

Equality inside the collar is exactly equality modulo the two endpoint seam identifications.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.exists_side_zero_digon_eq_of_im_eq_chordHeight (z : PolygonCell 2) (hy : z.val.im = chordHeight z) : ∃ (t : ↑unitInterval), (PolygonCell.side 0) t = z

Every point on the upper circular boundary of the digon has a side-zero parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.teardrop_radial_scale_le_one (z q : PolygonCell 1) (hqnorm : ‖q.val‖ = 1) (hqcusp : q.val ≠ 1) {μ : ℝ} (hμ : 1 ≤ μ) (hscale : teardropMap z = ↑μ * teardropMap q) : μ ≤ 1

A disk point cannot lie radially beyond a non-cusp boundary point of the teardrop.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarScale_half_le (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : 2⁻¹ ≤ (3 * chordHeight z ^ 2 - chordHeight z * z.val.im) / (4 * chordHeight z ^ 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.norm_collarCirclePoint (z : PolygonCell 2) : ‖(collarCirclePoint z).val‖ = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint_ne_cusp (z : PolygonCell 2) (hs : chordHeight z ≠ 0) : (collarCirclePoint z).val ≠ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.eq_monogon_basepoint_of_monogonMap_eq_zero (z : PolygonCell 1) (hz : monogonMap z = 0) : z = (PolygonCell.side 0) 0

The half-size teardrop map reaches the cusp only at the monogon basepoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPair_eqvGen_inl_inr_of_map_eq (z : PolygonCell 1) (w : PolygonCell 2) (hzw : monogonMap z = collarMap w) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) (Sum.inl z) (Sum.inr w)

A monogon point and a collar point have the same image exactly along the declared seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.monogonMap_injective : Function.Injective monogonMap

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildPairMap_eqvGen_of_eq {x y : BaseChildPair} (hxy : baseChildPairMap x = baseChildPairMap y) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) x y

Equality under the analytic child-pair map is exactly the generated seam relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingMap_injective : Function.Injective ⇑baseChildGluingMap

Surjectivity onto the teardrop

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint_eq_cusp_of_chordHeight_eq_zero (z : PolygonCell 2) (hs : chordHeight z = 0) : (collarCirclePoint z).val = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.exists_collarMap_eq_smul_teardropMap (q : PolygonCell 1) (hqnorm : ‖q.val‖ = 1) (hqcusp : q.val ≠ 1) {a : ℝ} (haHalf : 2⁻¹ ≤ a) (haOne : a ≤ 1) : ∃ (w : PolygonCell 2), collarMap w = ↑a * teardropMap q

Every radial scale between one half and one is realized by a unique vertical chord in the digon collar, for any non-cusp teardrop boundary direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.exists_teardrop_boundary_scale (z : PolygonCell 1) (hz : z.val ≠ 1) : ∃ (q : PolygonCell 1) (a : ℝ), ‖q.val‖ = 1 ∧ q.val ≠ 1 ∧ 0 < a ∧ a ≤ 1 ∧ teardropMap z = ↑a * teardropMap q

Every non-cusp teardrop point lies on a unique radial segment from a non-cusp boundary direction, at a scale in (0, 1].

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingMap_surjective : Function.Surjective ⇑baseChildGluingMap

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingHomeomorph : DiskSquare.ParamChildGluing 0 1 ≃ₜ ↑Teardrop

A monogon glued along its entire side to one side of a digon is a closed disk.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseChildGluingHomeomorph_apply (q : DiskSquare.ParamChildGluing 0 1) : baseChildGluingHomeomorph q = baseChildGluingMap q

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseSourceChildGluingHomeomorph : PolygonCell 1 ≃ₜ DiskSquare.ParamChildGluing 0 1

The complete base equivalence from the unsplit monogon to the one-sided-degenerate child quotient.

Equations

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

Exact compatibility with the surviving digon side

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.side_one_digon_val (t : ↑unitInterval) : ((PolygonCell.side 1) t).val = ↑(Circle.exp (Real.pi * (1 + ↑t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.side_one_digon_im (t : ↑unitInterval) : ((PolygonCell.side 1) t).val.im = -Real.sin (Real.pi * ↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.chordHeight_side_one_digon (t : ↑unitInterval) : chordHeight ((PolygonCell.side 1) t) = Real.sin (Real.pi * ↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarCirclePoint_side_one_digon (t : ↑unitInterval) : collarCirclePoint ((PolygonCell.side 1) t) = (PolygonCell.side 0) t

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_eq_teardropMap_collarCirclePoint_of_im_eq_neg (z : PolygonCell 2) (hy : z.val.im = -chordHeight z) : collarMap z = teardropMap (collarCirclePoint z)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.collarMap_old_side (t : ↑unitInterval) : collarMap ((PolygonCell.side 1) t) = teardropMap ((PolygonCell.side 0) t)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.baseSourceChildGluingHomeomorph_side (t : ↑unitInterval) : baseSourceChildGluingHomeomorph ((PolygonCell.side 0) t) = Quotient.mk'' (Sum.inr ((PolygonCell.side 1) t))

In the base one-sided-degenerate P2 equivalence, the source side is exactly the surviving digon side.

Transport to an arbitrary positive surviving side count

def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights (r : ℕ) : List ℕ

Boundary weights which make side zero fill one digon semicircle and divide the other semicircle equally among the r old sides.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights r = r :: List.replicate r 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_length (r : ℕ) : (rightDegenerateWeights r).length = r + 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_sum (r : ℕ) : (rightDegenerateWeights r).sum = 2 * r

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_positive {r : ℕ} (hr : 0 < r) : WeightedCircle.Positive (rightDegenerateWeights r)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_ne_nil (r : ℕ) : rightDegenerateWeights r ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_get_zero (r : ℕ) : (rightDegenerateWeights r).get ⟨0, ⋯⟩ = r

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_take_succ (r : ℕ) (i : Fin r) : List.take (↑i + 1) (rightDegenerateWeights r) = r :: List.replicate (↑i) 1

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightDegenerateWeights_get_succ (r : ℕ) (i : Fin r) : (rightDegenerateWeights r).get ⟨↑i + 1, ⋯⟩ = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.oldSideParameter {r : ℕ} (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : ↑unitInterval

The common parameter occupied by old side i inside the surviving digon semicircle.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.oldSideParameter hr i t = ⟨(↑↑i + ↑t) / ↑r, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightBoundaryHomeomorph (r : ℕ) (hr : 0 < r) : Circle ≃ₜ Circle

Reparameterize the (r+1)-gon boundary as a digon boundary, assigning the entire first semicircle to the fresh side.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightCellHomeomorph (r : ℕ) (hr : 0 < r) : PolygonCell (r + 1) ≃ₜ PolygonCell 2

Radially extend the weighted boundary map from the surviving child to a digon.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.sourceCellHomeomorph (r : ℕ) : PolygonCell r ≃ₜ PolygonCell 1

Forget the side subdivision on the unsplit source disk.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.sourceCellHomeomorph r = LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.radialHomeomorph (Homeomorph.refl Circle)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightBoundaryHomeomorph_fresh (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (rightBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle 0 t)) = Circle.exp (PolygonCell.sideAngle 0 t)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightBoundaryHomeomorph_old (r : ℕ) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (rightBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle (i.addNat 1) t)) = Circle.exp (PolygonCell.sideAngle 1 (oldSideParameter hr i t))

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightCellHomeomorph_fresh (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (rightCellHomeomorph r hr) ((PolygonCell.side 0) t) = (PolygonCell.side 0) t

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightCellHomeomorph_old (r : ℕ) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (rightCellHomeomorph r hr) ((PolygonCell.side (i.addNat 1)) t) = (PolygonCell.side 1) (oldSideParameter hr i t)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.sourceCellHomeomorph_side (r : ℕ) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (sourceCellHomeomorph r) ((PolygonCell.side i) t) = (PolygonCell.side 0) (oldSideParameter hr i t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBaseHomeomorph (r : ℕ) (hr : 0 < r) : DiskSquare.ChildPair 0 r ≃ₜ BaseChildPair

Simultaneously straighten a one-sided-degenerate child pair to the base monogon--digon pair.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBaseHomeomorph_inl (r : ℕ) (hr : 0 < r) (z : PolygonCell 1) : (childPairBaseHomeomorph r hr) (Sum.inl z) = Sum.inl z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBaseHomeomorph_inr (r : ℕ) (hr : 0 < r) (z : PolygonCell (r + 1)) : (childPairBaseHomeomorph r hr) (Sum.inr z) = Sum.inr ((rightCellHomeomorph r hr) z)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.rightCellHomeomorph_symm_fresh (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (rightCellHomeomorph r hr).symm ((PolygonCell.side 0) t) = (PolygonCell.side 0) t

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBase_generator_map (r : ℕ) (hr : 0 < r) {x y : DiskSquare.ChildPair 0 r} (hxy : DiskSquare.ParamChildSeamGenerator 0 r x y) : DiskSquare.ParamChildSeamGenerator 0 1 ((childPairBaseHomeomorph r hr) x) ((childPairBaseHomeomorph r hr) y)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBase_generator_comap (r : ℕ) (hr : 0 < r) {x y : BaseChildPair} (hxy : DiskSquare.ParamChildSeamGenerator 0 1 x y) : DiskSquare.ParamChildSeamGenerator 0 r ((childPairBaseHomeomorph r hr).symm x) ((childPairBaseHomeomorph r hr).symm y)

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childPairBase_eqvGen_iff (r : ℕ) (hr : 0 < r) (x y : DiskSquare.ChildPair 0 r) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 r) x y ↔ Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 1) ((childPairBaseHomeomorph r hr) x) ((childPairBaseHomeomorph r hr) y)

The weighted child straightening identifies exactly the two generated seam relations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childGluingBaseHomeomorph (r : ℕ) (hr : 0 < r) : DiskSquare.ParamChildGluing 0 r ≃ₜ DiskSquare.ParamChildGluing 0 1

The arbitrary one-sided-degenerate child quotient is identified with the base monogon--digon quotient.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.childGluingBaseHomeomorph_mk (r : ℕ) (hr : 0 < r) (x : DiskSquare.ChildPair 0 r) : (childGluingBaseHomeomorph r hr) (Quotient.mk'' x) = Quotient.mk'' ((childPairBaseHomeomorph r hr) x)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.sourceChildGluingHomeomorph (r : ℕ) (hr : 0 < r) : PolygonCell r ≃ₜ DiskSquare.ParamChildGluing 0 r

The local source-to-children equivalence for any ordinary-valid right one-sided-degenerate P2 cut.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.P2DegenerateDisk.sourceChildGluingHomeomorph_side (r : ℕ) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (sourceChildGluingHomeomorph r hr) ((PolygonCell.side i) t) = Quotient.mk'' (Sum.inr ((PolygonCell.side (i.addNat 1)) t))

Every old source side is carried to the corresponding surviving-child side with its exact original parameter.