Normalization on the punctured Markoff surface

Scaling every original Markoff coordinate by three gives an equivalence with the normalized punctured surface when three is invertible. The assembly-specific small-order sets transported through this equivalence are defined in BGS.Markoff.Assembly.PuncturedSmallOrderCount.

def BGS.Markoff.puncturedNormalizationEquiv (R : Type u) [CommRing R] [Invertible 3] : PuncturedMarkoffSurface R ≃ ↑(normalizedPuncturedSurface R)

Scaling by three identifies the action carrier of original punctured Markoff points with the subtype of normalized punctured Markoff points.

Equations

• BGS.Markoff.puncturedNormalizationEquiv R = (BGS.Markoff.puncturedSurfaceEquiv R).trans ((BGS.Markoff.normalizationEquiv R).subtypeEquiv ⋯)

@[simp]

theorem BGS.Markoff.puncturedNormalizationEquiv_coe {R : Type u} [CommRing R] [Invertible 3] (x : PuncturedMarkoffSurface R) : ↑((puncturedNormalizationEquiv R) x) = toNormalized ↑↑x

noncomputable def BGS.Markoff.originalPuncturedFinsetOfNormalized {R : Type u} [CommRing R] [Invertible 3] (S : Finset ↑(normalizedPuncturedSurface R)) : Finset (PuncturedMarkoffSurface R)

Pull a finite set of normalized punctured points back to original punctured coordinates.

Equations

• BGS.Markoff.originalPuncturedFinsetOfNormalized S = Finset.map (BGS.Markoff.puncturedNormalizationEquiv R).symm.toEmbedding S

@[simp]

theorem BGS.Markoff.mem_originalPuncturedFinsetOfNormalized_iff {R : Type u} [CommRing R] [Invertible 3] {S : Finset ↑(normalizedPuncturedSurface R)} {x : PuncturedMarkoffSurface R} : x ∈ originalPuncturedFinsetOfNormalized S ↔ (puncturedNormalizationEquiv R) x ∈ S

theorem BGS.Markoff.originalPuncturedFinsetOfNormalized_card {R : Type u} [CommRing R] [Invertible 3] (S : Finset ↑(normalizedPuncturedSurface R)) : (originalPuncturedFinsetOfNormalized S).card = S.card

Pullback through normalization preserves the exact cardinality of every finite set.