Fuchsian groups and orbifold Riemann surfaces

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

DefinitionTauCeti.ModularGroup.jBiholomorph#

The normalized modular invariant identifies the compactified level-one modular quotient biholomorphically with the Riemann sphere.

TauCeti.ModularGroup.jBiholomorph :
  Diffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ)
    psl2zToPSL2R.range.CompactifiedQuotient (OnePoint ℂ) ↑⊤

Lean

Formalized in Tau Ceti as TauCeti.ModularGroup.jBiholomorph.

Sources

• Tau Ceti documentation: TauCeti.ModularGroup.jBiholomorph
• Source of TauCeti.ModularGroup.jBiholomorph in TauCeti/Analysis/Complex/Fuchsian/LevelOne/Sphere.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.ModularGroup.jBiholomorph

Uses 6 · Used by 1

Statement usesA degree-one map is a biholomorphism · Subgroup.CompactifiedQuotient

Proof usesDescent of an invariant map to the orbit space · The identity theorem for Riemann surfaces · Rouché's theorem for a disc, classical form · Shimizu's inequality at two cusps

Used byThe uniformization theorem

TheoremPoincaré's presentation theorem#

The group of a locally finite fundamental polygon is presented by the side generators, the side relations, and the finite-vertex cycle relations.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective {n : ℕ} [NeZero n]
  {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ)
  (hlf : LocallyFinite fun γ => ↑γ • P.carrier)
  (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) :
  Function.Bijective ⇑(σ.relatorQuotientTo hmap)

Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective.

Other forms

Poincaré's presentation theorem, as a description of the relations. Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ker_lift_generatorsIn_eq_normalClosure_relators.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ker_lift_generatorsIn_eq_normalClosure_relators
  {n : ℕ} [NeZero n] {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ)
  (hlf : LocallyFinite fun γ => ↑γ • P.carrier)
  (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) :
  (FreeGroup.lift (σ.generatorsIn hmap)).ker = Subgroup.normalClosure σ.relators

Poincaré's presentation theorem. Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_injective.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_injective {n : ℕ} [NeZero n]
  {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ)
  (hlf : LocallyFinite fun γ => ↑γ • P.carrier)
  (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) :
  Function.Injective ⇑(σ.relatorQuotientTo hmap)

Sources

• Tau Ceti documentation: TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective
• Source of TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective in TauCeti/Analysis/Complex/UpperHalfPlane/Polygon/SidePairing/Presentation.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective · TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ker_lift_generatorsIn_eq_normalClosure_relators · TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_injective

Uses 1 · Used by 2

Proof usesMacbeath's theorem

Used byDirichlet presentations of cocompact Fuchsian groups · The presentation part of Poincaré's polygon theorem

TheoremDirichlet presentations of cocompact Fuchsian groups#

Let Γ ≤ PSL(2, ℝ) be discrete with compact orbit space, and let p ∈ ℍ have trivial stabilizer. The Dirichlet domain of Γ centred at p is a compact convex polygon P with a side pairing by elements of Γ, and Γ is presented by the side-pairing maps, subject to the side relations and the vertex-cycle relations.

Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace
  (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ]
  [CompactSpace (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)] {p : UpperHalfPlane}
  (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) :
  ∃ n,
    ∃ (x : NeZero n),
      ∃ P σ,
        ∃ (hmap : ∀ (i : Fin n), σ.map i ∈ Γ),
          P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧
            Function.Bijective ⇑(σ.relatorQuotientTo hmap)

Lean

Formalized in Tau Ceti as Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace.

Sources

• Tau Ceti documentation: Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace
• Source of Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace in TauCeti/Analysis/Complex/Fuchsian/DirichletDomain/SidePairing.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace

Uses 2

Proof usesThe Gauss–Bonnet formula · Poincaré's presentation theorem

TheoremThe orbifold area formula for a fundamental polygon#

Let the translates of a side-paired convex n-gon P by a group Γ containing the side-pairing maps be locally finite, with disjoint interiors. Then the covolume of Γ is 2π ((n - k) / 2 - 1 - V + ∑ₑ (1 - 1 / mₑ)), where k is the number of self-paired sides, V the number of finite vertex cycles, and e runs over the elliptic orbits of Γ, with stabilizer orders mₑ.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq_two_pi_mul {n : ℕ} [NeZero n]
  {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ)
  (hlf : LocallyFinite fun γ => ↑γ • P.carrier)
  (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) :
  MeasureTheory.covolume (↥Γ) UpperHalfPlane MeasureTheory.volume =
    ENNReal.ofReal
      (2 * Real.pi *
        ((↑n - ↑(Nat.card { i // σ.pair i = i })) / 2 - 1 - ↑(Nat.card σ.FiniteVertexCycle) +
          ∑ᶠ (e : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) (_ : e ∈ Γ.ellipticOrbits),
            (1 - (↑(TauCeti.cardStabilizerOnOrbit e))⁻¹)))

Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq_two_pi_mul.

Sources

• Tau Ceti documentation: TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq_two_pi_mul
• Source of TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq_two_pi_mul in TauCeti/Analysis/Complex/Fuchsian/Polygon/Area.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq_two_pi_mul

Uses 1

Proof usesThe Gauss–Bonnet formula

TheoremThe number of cusps of a locally finite fundamental polygon#

The number of cusp orbits of Γ is the number of ideal vertex cycles of P.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit {n : ℕ} [NeZero n]
  {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ)
  (hlf : LocallyFinite fun γ => ↑γ • P.carrier)
  (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) :
  Nat.card Γ.CuspOrbit = Nat.card σ.IdealVertexCycle

Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit.

Sources

• Tau Ceti documentation: TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit
• Source of TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit in TauCeti/Analysis/Complex/Fuchsian/Cusp/VertexCycle.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit

Uses 2

Proof usesShimizu's inequality at two cusps · Subgroup.CompactifiedQuotient

DefinitionA degree-one map is a biholomorphism#

construct a biholomorphism from a finite holomorphic map of degree one from a compact Riemann surface to a connected one.

TauCeti.RiemannSurface.biholomorphOfDegreeEqOne.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y]
  [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y]
  [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y]
  (f : TauCeti.RiemannSurface.FiniteHolomorphicMap X Y)
  (hf : TauCeti.RiemannSurface.degree ↑f = 1) :
  Diffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) X Y ↑⊤

Lean

Formalized in Tau Ceti as TauCeti.RiemannSurface.biholomorphOfDegreeEqOne.

Sources

• Tau Ceti documentation: TauCeti.RiemannSurface.biholomorphOfDegreeEqOne
• Source of TauCeti.RiemannSurface.biholomorphOfDegreeEqOne in TauCeti/Analysis/Complex/RiemannSurface/Degree.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.RiemannSurface.biholomorphOfDegreeEqOne

Uses 3 · Used by 2

Proof usesThe open mapping theorem · Osgood's lemma · Rouché's theorem for a disc, classical form

Used byTauCeti.ModularGroup.jBiholomorph · The uniformization theorem

TheoremThe degree of a finite-index map of compactified Fuchsian quotients is the index#

For Δ ≤ Γ discrete of finite index, the map X(Δ) → X(Γ) induced by the inclusion has degree [Γ : Δ].

Subgroup.degree_compactifiedQuotientMap
  {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ)
  [Δ.IsFiniteRelIndex Γ] :
  TauCeti.RiemannSurface.degree (Subgroup.compactifiedQuotientMap h) = (Δ.subgroupOf Γ).index

Lean

Formalized in Tau Ceti as Subgroup.degree_compactifiedQuotientMap.

Sources

• Tau Ceti documentation: Subgroup.degree_compactifiedQuotientMap
• Source of Subgroup.degree_compactifiedQuotientMap in TauCeti/Analysis/Complex/Fuchsian/Compactification/Degree.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.degree_compactifiedQuotientMap

Uses 4

Statement usesSubgroup.CompactifiedQuotient

Proof usesDescent of an invariant map to the orbit space · Rouché's theorem for a disc, classical form · Shimizu's inequality at two cusps

TheoremJørgensen's inequality#

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup and let A, B ∈ SL(2, ℝ) lift elements of Γ. Unless B conjugates the class of A to itself or to its inverse, |tr² A - 4| + |tr [A, B] - 2| ≥ 1.

Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
  {B : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ]
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hA : ↑A ∈ Γ) (hB : ↑B ∈ Γ) (h₁ : ↑B * ↑A * (↑B)⁻¹ ≠ ↑A)
  (h₂ : ↑B * ↑A * (↑B)⁻¹ ≠ (↑A)⁻¹) : 1 ≤ |(↑A).trace ^ 2 - 4| + |(↑⁅A, B⁆).trace - 2|

Lean

Formalized in Tau Ceti as Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two.

Other forms

Jørgensen's inequality for a dilation. Formalized in Tau Ceti as Subgroup.one_le_four_mul_sinh_sq_mul_of_dilation_mem.

Subgroup.one_le_four_mul_sinh_sq_mul_of_dilation_mem
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {s : ℝ}
  {B : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ]
  (hD : ↑(Matrix.SpecialLinearGroup.dilation s) ∈ Γ) (hB : ↑B ∈ Γ)
  (h₁ :
    ↑B * ↑(Matrix.SpecialLinearGroup.dilation s) * (↑B)⁻¹ ≠ ↑(Matrix.SpecialLinearGroup.dilation s))
  (h₂ :
    ↑B * ↑(Matrix.SpecialLinearGroup.dilation s) * (↑B)⁻¹ ≠
      ↑(Matrix.SpecialLinearGroup.dilation (-s))) :
  1 ≤ 4 * Real.sinh (s / 2) ^ 2 * (1 + |↑B 0 1 * ↑B 1 0|)

Jørgensen's inequality for an element fixing a point. Formalized in Tau Ceti as Subgroup.one_le_four_sub_trace_sq_mul_cosh_sq_of_smul_eq_self.

Subgroup.one_le_four_sub_trace_sq_mul_cosh_sq_of_smul_eq_self
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ]
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} {B : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ}
  {z : UpperHalfPlane} (hA : ↑A ∈ Γ) (hB : B ∈ Γ) (hAz : A • z = z) (hA₁ : ↑A ≠ 1)
  (hBz : B • z ≠ z) : 1 ≤ (4 - (↑A).trace ^ 2) * Real.cosh (dist (B • z) z / 2) ^ 2

Jørgensen's inequality for elliptic elements. Formalized in Tau Ceti as Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_abs_trace_lt_two.

Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_abs_trace_lt_two
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
  {B : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ]
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hA : ↑A ∈ Γ) (hB : ↑B ∈ Γ) (hell : |(↑A).trace| < 2)
  (h₁ : ↑B * ↑A * (↑B)⁻¹ ≠ ↑A) : 1 ≤ |(↑A).trace ^ 2 - 4| + |(↑⁅A, B⁆).trace - 2|

Jørgensen's inequality for hyperbolic elements. Formalized in Tau Ceti as Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_two_lt_abs_trace.

Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_two_lt_abs_trace
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
  {B : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ]
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hA : ↑A ∈ Γ) (hB : ↑B ∈ Γ) (hhyp : 2 < |(↑A).trace|)
  (h₁ : ↑B * ↑A * (↑B)⁻¹ ≠ ↑A) (h₂ : ↑B * ↑A * (↑B)⁻¹ ≠ (↑A)⁻¹) :
  1 ≤ |(↑A).trace ^ 2 - 4| + |(↑⁅A, B⁆).trace - 2|

Jørgensen's inequality for parabolic elements. Formalized in Tau Ceti as Subgroup.one_le_abs_trace_commutatorElement_sub_two_of_isParabolic.

Subgroup.one_le_abs_trace_commutatorElement_sub_two_of_isParabolic
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
  {B : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ]
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hA : ↑A ∈ Γ) (hB : ↑B ∈ Γ)
  (hpar : Matrix.ProjectiveSpecialLinearGroup.IsParabolic ↑A) (h₁ : ↑B * ↑A * (↑B)⁻¹ ≠ ↑A) :
  1 ≤ |(↑⁅A, B⁆).trace - 2|

Sources

• Tau Ceti documentation: Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two
• Source of Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two in TauCeti/Analysis/Complex/Fuchsian/Jorgensen.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two · Subgroup.one_le_four_mul_sinh_sq_mul_of_dilation_mem · Subgroup.one_le_four_sub_trace_sq_mul_cosh_sq_of_smul_eq_self · Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_abs_trace_lt_two · Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two_of_two_lt_abs_trace · Subgroup.one_le_abs_trace_commutatorElement_sub_two_of_isParabolic

Uses 1 · Used by 2

Proof usesShimizu's lemma

Used byThe converse of Poincaré's polygon theorem · The Margulis lemma for Fuchsian groups

TheoremThe Margulis lemma for Fuchsian groups#

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup and let g, h ∈ Γ both move a point z ∈ ℍ a distance at most 1 / 4. If g fixes no point of ℍ, that is, if g is parabolic or hyperbolic, then h g h⁻¹ = g or h g h⁻¹ = g⁻¹.

Subgroup.conj_eq_or_conj_eq_inv_of_dist_le
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ]
  {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hh : h ∈ Γ)
  (hfix : ∀ (w : UpperHalfPlane), g • w ≠ w) {z : UpperHalfPlane} (hgz : dist (g • z) z ≤ 1 / 4)
  (hhz : dist (h • z) z ≤ 1 / 4) : h * g * h⁻¹ = g ∨ h * g * h⁻¹ = g⁻¹

Lean

Formalized in Tau Ceti as Subgroup.conj_eq_or_conj_eq_inv_of_dist_le.

Sources

• Tau Ceti documentation: Subgroup.conj_eq_or_conj_eq_inv_of_dist_le
• Source of Subgroup.conj_eq_or_conj_eq_inv_of_dist_le in TauCeti/Analysis/Complex/Fuchsian/Margulis.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.conj_eq_or_conj_eq_inv_of_dist_le

Uses 1 · Used by 1

Proof usesJørgensen's inequality

Used byThe converse of Poincaré's polygon theorem

InductiveSubgroup.CompactifiedQuotient#

The compactified quotient of Γ ≤ PSL(2, ℝ): the coarse orbit space Γ \ ℍ with one point adjoined for each cusp orbit of Γ.

Subgroup.CompactifiedQuotient (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Type

Lean

Formalized in Tau Ceti as Subgroup.CompactifiedQuotient.

Sources

• Tau Ceti documentation: Subgroup.CompactifiedQuotient
• Source of Subgroup.CompactifiedQuotient in TauCeti/Analysis/Complex/Fuchsian/Compactification/Basic.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.CompactifiedQuotient

Used by 5

Used byCompactness from a Dirichlet domain with a bounded cusp truncation · TauCeti.ModularGroup.jBiholomorph · The degree of a finite-index map of compactified Fuchsian quotients is the index · The number of cusps of a locally finite fundamental polygon · The uniformization theorem

TheoremCompactness from a Dirichlet domain with a bounded cusp truncation#

If a discrete subgroup Γ has finitely many cusp orbits, and some Dirichlet domain of Γ is bounded after removing finitely many cusp horodiscs of positive heights, then the quotient Γ \ ℍ with its cusp orbits adjoined is compact.

Subgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation.{u_1}
  (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ]
  {ι : Type u_1} [Finite ι] [Finite Γ.CuspOrbit] (p : UpperHalfPlane) (D : ι → Γ.CuspDatum)
  {A : ι → ℝ} (hA : ∀ (i : ι), 0 < A i)
  (hb :
    Bornology.IsBounded
      (TauCeti.dirichletDomain (↥Γ) p \ ⋃ i, TauCeti.Subgroup.CuspDatum.horodisc (D i) (A i))) :
  CompactSpace Γ.CompactifiedQuotient

Lean

Formalized in Tau Ceti as Subgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation.

Sources

• Tau Ceti documentation: Subgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation
• Source of Subgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation in TauCeti/Analysis/Complex/Fuchsian/DirichletDomain/Polygon.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation

Uses 3

Statement usesSubgroup.CompactifiedQuotient

Proof usesThe Gauss–Bonnet formula · Shimizu's inequality at two cusps

DefinitionTauCeti.thickPart#

The ε-thick part of an action on a metric space: the points moved a distance at least ε by every nonidentity element. For 0 < ε it excludes every point with nontrivial stabilizer.

TauCeti.thickPart.{u_1, u_2} (G : Type u_1) {X : Type u_2} [Group G] [PseudoMetricSpace X]
  [MulAction G X] (ε : ℝ) : Set X

Lean

Formalized in Tau Ceti as TauCeti.thickPart.

Sources

• Tau Ceti documentation: TauCeti.thickPart
• Source of TauCeti.thickPart in TauCeti/Topology/MetricSpace/ThickPart.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.thickPart

Used by 2

Used byThe converse of Poincaré's polygon theorem · The thick part of the quotient of a cofinite group is compact

TheoremThe thick part of the quotient of a cofinite group is compact#

For a cofinite Γ ≤ PSL(2, ℝ) and ε > 0, the image in Γ \ ℍ of the points moved a hyperbolic distance at least ε by every nonidentity element of Γ is compact.

Subgroup.IsCofinite.isCompact_image_thickPart
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) {ε : ℝ}
  (hε : 0 < ε) :
  IsCompact (Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) '' TauCeti.thickPart (↥Γ) ε)

Lean

Formalized in Tau Ceti as Subgroup.IsCofinite.isCompact_image_thickPart.

Sources

• Tau Ceti documentation: Subgroup.IsCofinite.isCompact_image_thickPart
• Source of Subgroup.IsCofinite.isCompact_image_thickPart in TauCeti/Analysis/Complex/Fuchsian/DirichletDomain/Thick.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanSubgroup.IsCofinite.isCompact_image_thickPart

Uses 1

Statement usesTauCeti.thickPart

StructureTauCeti.IsLocalTiling#

A local tiling by a closed path-connected tile P: for each x ∈ P, N x is a set of local neighbours, the elements h such that h • P is one of the tiles around x. The identity is a neighbour, x ∈ h • P for each neighbour h, the neighbours of x seen from the tile h • P are the translates h⁻¹ • N x, and each point of P lies in a tiling chart made of its own neighbours.

TauCeti.IsLocalTiling.{u_1, u_2} {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X]
  [TopologicalSpace X] (P : Set X) (N : X → Set G) : Prop

Lean

Formalized in Tau Ceti as TauCeti.IsLocalTiling.

Sources

• Tau Ceti documentation: TauCeti.IsLocalTiling
• Source of TauCeti.IsLocalTiling in TauCeti/Topology/Algebra/GroupAction/LocalTiling.lean
• Tau Ceti roadmap status: Fuchsian groups and orbifold Riemann surfaces

LeanTauCeti.IsLocalTiling

Used by 3

Used byThe discreteness part of Poincaré's polygon theorem · The fundamental-set part of Poincaré's polygon theorem · The presentation part of Poincaré's polygon theorem

TheoremThe converse of Poincaré's polygon theorem#

Every cofinite Γ ≤ PSL(2, ℝ) arises from Poincaré's polygon theorem. For a centre p with trivial stabilizer, the Dirichlet domain of Γ centred at p is the carrier of a convex polygon with finitely many vertices and a side pairing whose maps generate Γ. The cycle transformation of each finite vertex has finite order m and the interior angles along its cycle add up to 2π / m, and the cycle transformation of each ideal vertex is parabolic. These are the hypotheses of TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic.

Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite)
  {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) :
  ∃ n,
    ∃ (x : NeZero n),
      ∃ P σ,
        P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧
          Subgroup.closure (Set.range σ.map) = Γ ∧
            (∀ (j : Fin n) (z : UpperHalfPlane),
                P.vertex j = Sum.inl z →
                  ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) ∧
              ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic

Lean

Formalized in Tau Ceti as Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq.

Sources

• Tau Ceti documentation: Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq
• Source of Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq in TauCeti/Analysis/Complex/Fuchsian/DirichletDomain/Cofinite.lean

LeanSubgroup.IsCofinite.exists_sidePairing_closure_range_map_eq

Uses 5

Proof usesThe Gauss–Bonnet formula · Jørgensen's inequality · The Margulis lemma for Fuchsian groups · Shimizu's inequality at two cusps · TauCeti.thickPart

TheoremShimizu's lemma#

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup containing the translation z ↦ z + w with w ≠ 0, and let A ∈ SL(2, ℝ) lift an element of Γ. If the lower-left entry of A does not vanish, that is, if the element does not fix ∞, then that entry has absolute value at least |w|⁻¹. Both lifts of the element give the same absolute value.

Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ}
  {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ] (hw : w ≠ 0)
  (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ) (hA : ↑A ∈ Γ) (hA0 : ↑A 1 0 ≠ 0) :
  |w|⁻¹ ≤ |↑A 1 0|

Lean

Formalized in Tau Ceti as Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem.

Other forms

Shimizu's lemma for two parabolic fixed points, geometric form. Formalized in Tau Ceti as Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem.

Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ} [DiscreteTopology ↥Γ]
  {w' : ℝ} (hw : w ≠ 0) (hw' : w' ≠ 0)
  (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ)
  {h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ}
  (hh : h * Matrix.ProjectiveSpecialLinearGroup.upperRightHom w' * h⁻¹ ∈ Γ)
  (hinf : h • OnePoint.infty ≠ OnePoint.infty) (z : UpperHalfPlane) : (h • z).im * z.im ≤ |w * w'|

Shimizu's lemma, geometric form. Formalized in Tau Ceti as Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem.

Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem
  {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ} [DiscreteTopology ↥Γ]
  (hw : w ≠ 0) (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ)
  {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ)
  (hginf : g • OnePoint.infty ≠ OnePoint.infty) (z : UpperHalfPlane) : (g • z).im * z.im ≤ w ^ 2

Sources

• Tau Ceti documentation: Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem
• Source of Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem in TauCeti/Analysis/Complex/Fuchsian/Shimizu.lean

LeanSubgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem · Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem · Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem

Used by 2

Used byJørgensen's inequality · Shimizu's inequality at two cusps

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.