Documentation

TauCeti.Analysis.Complex.UpperHalfPlane.Geodesic.Reflection

Reflections in hyperbolic geodesics #

Reflection in the imaginary axis sends x + iy to -x + iy; it is the action of Mathlib's UpperHalfPlane.J : GL (Fin 2) ℝ. Conjugating this isometry by the projective Möbius action gives reflection in the oriented geodesic geodesicLine g. The resulting map fixes that line pointwise, exchanges its right and left half-planes, and depends only on the line as a set.

These reflections are the orientation-reversing generators used to construct hyperbolic reflection groups. Products of adjacent reflections are orientation preserving and supply the side-pairing transformations for triangle groups.

Conjugation by J is the automorphism pslConjJ of PSL(2, ℝ) (from TauCeti/Analysis/Complex/UpperHalfPlane/PSL/ConjJ.lean), and J intertwines each g with pslConjJ g. Hence the product of two geodesic reflections is the action of an element of PSL(2, ℝ), geodesicReflectionComp g h. Since the vertices of polygons may be ideal, reflections are also extended to ℍ ∪ ∂ℍ, where J acts on ∂ℍ = ℝ ∪ {∞} by x ↦ -x: extGeodesicReflection g fixes the line of g with its ideal endpoints, reverses orientation (the left side of the geodesic from p to q goes to the left side of the geodesic from the image of q to the image of p), and preserves angles. Reflecting a point c to the left of a line from a to b lands it to the left of the geodesic from c to a when the angle at a is acute; this is the convexity condition for gluing a triangle to its mirror image.

Main declarations #

References #

source
theorem TauCeti.UpperHalfPlane.isometry_J_smul :
Isometry fun (x : UpperHalfPlane) => UpperHalfPlane.J • x

The orientation-reversing involution UpperHalfPlane.J : z ↦ -conj z acts on ℍ by an isometry.

source
noncomputable def TauCeti.UpperHalfPlane.imaginaryAxisReflection :
UpperHalfPlane ≃ᵢ UpperHalfPlane

Reflection in the imaginary axis of the upper half-plane, x + iy ↦ -x + iy, packaged as an isometry. It is the action of Mathlib's orientation-reversing involution UpperHalfPlane.J : GL (Fin 2) ℝ (imaginaryAxisReflection_apply).

Instances For
    source
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_apply (z : UpperHalfPlane) :
    imaginaryAxisReflection z = UpperHalfPlane.J • z

    Reflection in the imaginary axis is the action of UpperHalfPlane.J.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_re (z : UpperHalfPlane) :
    (imaginaryAxisReflection z).re = -z.re

    Reflection in the imaginary axis negates the real part.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_im (z : UpperHalfPlane) :
    (imaginaryAxisReflection z).im = z.im

    Reflection in the imaginary axis preserves the imaginary part.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_imaginaryAxisReflection (z : UpperHalfPlane) :
    imaginaryAxisReflection (imaginaryAxisReflection z) = z

    Reflection in the imaginary axis is an involution.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_symm :
    imaginaryAxisReflection.symm = imaginaryAxisReflection

    Reflection in the imaginary axis is its own inverse.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_apply_eq_self_iff (z : UpperHalfPlane) :
    imaginaryAxisReflection z = z ↔ z.re = 0

    A point is fixed by reflection in the imaginary axis exactly when it lies on that axis.

    source
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_pslS_smul (z : UpperHalfPlane) :
    imaginaryAxisReflection (pslS • z) = pslS • imaginaryAxisReflection z

    Reflection in the imaginary axis commutes with the involution pslS : z ↦ -1/z.

    source
    theorem TauCeti.UpperHalfPlane.imaginaryAxisReflection_dilation_smul (s : ℝ) (z : UpperHalfPlane) :
    imaginaryAxisReflection (Matrix.SpecialLinearGroup.dilation s • z) = Matrix.SpecialLinearGroup.dilation s • imaginaryAxisReflection z

    Reflection in the imaginary axis commutes with the dilations z ↦ exp s * z.

    source
    noncomputable def TauCeti.UpperHalfPlane.geodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
    UpperHalfPlane ≃ᵢ UpperHalfPlane

    Reflection in the oriented geodesic geodesicLine g, obtained by transporting reflection in the imaginary axis along the projective Möbius isometry g.

    Instances For
      source
      theorem TauCeti.UpperHalfPlane.geodesicReflection_apply (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) z = g • imaginaryAxisReflection (g⁻¹ • z)

      Reflection in geodesicLine g is conjugated imaginary-axis reflection.

      source
      theorem TauCeti.UpperHalfPlane.geodesicReflection_apply_eq_smul (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) z = (Matrix.ProjectiveSpecialLinearGroup.toPGL g * Matrix.ProjGenLinGroup.mk UpperHalfPlane.J * (Matrix.ProjectiveSpecialLinearGroup.toPGL g)⁻¹) • z

      Reflection in geodesicLine g is the action of the element g J g⁻¹ of PGL(2, ℝ), the conjugate of UpperHalfPlane.J by the image of g. Products of geodesic reflections are thus computed in PGL(2, ℝ).

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_one :
      geodesicReflection 1 = imaginaryAxisReflection

      Reflection in the geodesic line of the identity is reflection in the imaginary axis.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.smul_geodesicReflection (h g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      h • (geodesicReflection g) z = (geodesicReflection (h * g)) (h • z)

      Moving a geodesic reflection by h gives the reflection in the moved geodesic h * g.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_geodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) ((geodesicReflection g) z) = z

      Reflection in a geodesic is an involution.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_symm (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
      (geodesicReflection g).symm = geodesicReflection g

      A geodesic reflection is its own inverse.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_mul_pslS (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
      geodesicReflection (g * pslS) = geodesicReflection g

      Reversing the orientation of a geodesic line does not change the reflection in it.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_mul_dilation (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) :
      geodesicReflection (g * ↑(Matrix.SpecialLinearGroup.dilation s)) = geodesicReflection g

      Shifting the parametrisation of a geodesic line does not change the reflection in it.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_apply_eq_self_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) z = z ↔ z ∈ Set.range (geodesicLine g)

      The fixed-point set of reflection in geodesicLine g is exactly that geodesic.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) :
      (geodesicReflection g) (geodesicLine g t) = geodesicLine g t

      Reflection in geodesicLine g fixes every point of its standard parametrisation.

      source
      theorem TauCeti.UpperHalfPlane.geodesicReflection_eq_of_range_eq {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hgh : Set.range (geodesicLine g) = Set.range (geodesicLine h)) :
      geodesicReflection g = geodesicReflection h

      A geodesic reflection depends only on the geodesic line as a set, not on the representative g (which also records an orientation and a base point).

      source
      theorem TauCeti.UpperHalfPlane.geodesicReflection_mem_leftHalfPlane_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) z ∈ leftHalfPlane g ↔ z ∈ rightHalfPlane g

      A point reflected across geodesicLine g lies in its left half-plane exactly when the original point lies in its right half-plane.

      source
      theorem TauCeti.UpperHalfPlane.geodesicReflection_mem_rightHalfPlane_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
      (geodesicReflection g) z ∈ rightHalfPlane g ↔ z ∈ leftHalfPlane g

      A point reflected across geodesicLine g lies in its right half-plane exactly when the original point lies in its left half-plane.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_image_rightHalfPlane (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
      ⇑(geodesicReflection g) '' rightHalfPlane g = leftHalfPlane g

      Reflection in a geodesic maps its right half-plane onto its left half-plane.

      source
      @[simp]
      theorem TauCeti.UpperHalfPlane.geodesicReflection_image_leftHalfPlane (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
      ⇑(geodesicReflection g) '' leftHalfPlane g = rightHalfPlane g

      Reflection in a geodesic maps its left half-plane onto its right half-plane.

      Reflection in a geodesic on ℍ ∪ ∂ℍ #

      source
      noncomputable def TauCeti.UpperHalfPlane.extGeodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
      UpperHalfPlane ⊕ OnePoint ℝ → UpperHalfPlane ⊕ OnePoint ℝ

      Reflection in the geodesic line of g, extended to the ideal boundary: on ℍ it is geodesicReflection g, and on ∂ℍ it is the Möbius map g J g⁻¹, where J : x ↦ -x is reflection in the imaginary axis. It fixes the line and its two ideal endpoints (IsGeodesicFromTo.extGeodesicReflection_left) and exchanges the two sides of the line (extGeodesicReflection_mem_extLeftHalfPlane_mul_pslS_iff).

      Instances For
        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_inl (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
        extGeodesicReflection g (Sum.inl z) = Sum.inl ((geodesicReflection g) z)

        On ℍ, the extended reflection is geodesicReflection.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_inr (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (ξ : OnePoint ℝ) :
        extGeodesicReflection g (Sum.inr ξ) = Sum.inr (g • UpperHalfPlane.J • g⁻¹ • ξ)

        On the ideal boundary, the extended reflection is the Möbius map g J g⁻¹.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.isLeft_extGeodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        (extGeodesicReflection g p).isLeft = p.isLeft

        The extended reflection maps points of ℍ to points of ℍ.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.isRight_extGeodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        (extGeodesicReflection g p).isRight = p.isRight

        The extended reflection maps ideal points to ideal points.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_apply (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        extGeodesicReflection g p = g • extGeodesicReflection 1 (g⁻¹ • p)

        Reflection in the geodesic line of g is reflection in the imaginary axis conjugated by g.

        source
        theorem TauCeti.UpperHalfPlane.smul_extGeodesicReflection (h g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        h • extGeodesicReflection g p = extGeodesicReflection (h * g) (h • p)

        Moving a reflection by h gives the reflection in the moved geodesic.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_one_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        extGeodesicReflection 1 (h • p) = pslConjJ h • extGeodesicReflection 1 p

        Reflection in the imaginary axis intertwines h with its conjugate pslConjJ h.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_extGeodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        extGeodesicReflection g (extGeodesicReflection g p) = p

        Reflection in a geodesic is an involution of ℍ ∪ ∂ℍ.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_injective (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
        Function.Injective (extGeodesicReflection g)

        Reflection in a geodesic is injective.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mul_pslS (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
        extGeodesicReflection (g * pslS) = extGeodesicReflection g

        Reversing the orientation of a geodesic line does not change the reflection in it.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mul_dilation (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) :
        extGeodesicReflection (g * ↑(Matrix.SpecialLinearGroup.dilation s)) = extGeodesicReflection g

        Shifting the parametrisation of a geodesic line does not change the reflection in it.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_eq_of_range_eq {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hgh : Set.range (geodesicLine g) = Set.range (geodesicLine h)) :
        extGeodesicReflection g = extGeodesicReflection h

        A geodesic reflection of ℍ ∪ ∂ℍ depends only on the geodesic line as a set.

        source
        theorem TauCeti.UpperHalfPlane.IsGeodesicFromTo.extGeodesicReflection_left {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hg : IsGeodesicFromTo g p q) :
        extGeodesicReflection g p = p

        Reflection in the line of g fixes the point that g runs from.

        source
        theorem TauCeti.UpperHalfPlane.IsGeodesicFromTo.extGeodesicReflection_right {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hg : IsGeodesicFromTo g p q) :
        extGeodesicReflection g q = q

        Reflection in the line of g fixes the point that g runs to.

        source
        theorem TauCeti.UpperHalfPlane.geodesicLine_pslConjJ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) :
        geodesicLine (pslConjJ g) t = imaginaryAxisReflection (geodesicLine g t)

        The geodesic line of the conjugate pslConjJ g is the reflection in the imaginary axis of the geodesic line of g, with the same parametrisation.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mem_extLeftHalfPlane_mul_pslS_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
        extGeodesicReflection g p ∈ extLeftHalfPlane (g * pslS) ↔ p ∈ extLeftHalfPlane g

        Reflection in a geodesic carries its left side onto the left side of the reversed line, which is its right side.

        source
        theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mem_extLeftHalfPlane_geodesicFromTo_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hpq : p ≠ q) (r : UpperHalfPlane ⊕ OnePoint ℝ) :
        extGeodesicReflection g r ∈ extLeftHalfPlane (geodesicFromTo (extGeodesicReflection g q) (extGeodesicReflection g p)) ↔ r ∈ extLeftHalfPlane (geodesicFromTo p q)

        A geodesic reflection reverses orientation: r is strictly to the left of the geodesic from p to q exactly when its reflection is strictly to the left of the geodesic from the reflection of q to the reflection of p.

        source
        theorem TauCeti.UpperHalfPlane.geodesicReflection_mem_closure_leftHalfPlane_geodesicFromTo_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hpq : p ≠ q) (z : UpperHalfPlane) :
        (geodesicReflection g) z ∈ closure (leftHalfPlane (geodesicFromTo (extGeodesicReflection g q) (extGeodesicReflection g p))) ↔ z ∈ closure (leftHalfPlane (geodesicFromTo p q))

        A point of ℍ is weakly to the left of the geodesic from p to q exactly when its mirror image is weakly to the left of the geodesic from the mirror image of q to that of p.

        Angles #

        source
        theorem TauCeti.UpperHalfPlane.velocity_pslConjJ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) :
        velocity (pslConjJ g) t = -(starRingEnd ℂ) (velocity g t)

        Reflection in the imaginary axis conjugates velocities of geodesic lines: the velocity of pslConjJ g is -conj of that of g.

        source
        @[simp]
        theorem TauCeti.UpperHalfPlane.geodesicAngle_pslConjJ (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
        geodesicAngle (pslConjJ g₁) (pslConjJ g₂) = geodesicAngle g₁ g₂

        Reflection in the imaginary axis preserves angles between geodesic lines.

        source
        theorem TauCeti.UpperHalfPlane.vertexAngle_extGeodesicReflection (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {p q r : UpperHalfPlane ⊕ OnePoint ℝ} (hpq : p ≠ q) (hpr : p ≠ r) :
        vertexAngle (extGeodesicReflection g p) (extGeodesicReflection g q) (extGeodesicReflection g r) = vertexAngle p q r

        Geodesic reflections preserve angles at vertices of ℍ ∪ ∂ℍ.

        Products of two reflections #

        source
        def TauCeti.UpperHalfPlane.geodesicReflectionComp (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
        Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

        The product of the reflections in the geodesic lines of g and of h, first in that of h: the orientation-preserving isometry z ↦ geodesicReflection g (geodesicReflection h z), as an element of PSL(2, ℝ) (geodesicReflectionComp_smul), which also acts on ℍ ∪ ∂ℍ as the composite of the extended reflections.

        Instances For
          source
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_def (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          geodesicReflectionComp g h = g * pslConjJ (g⁻¹ * h) * h⁻¹

          The product of two geodesic reflections, unfolded.

          source
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_smul_eq_extGeodesicReflection (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p : UpperHalfPlane ⊕ OnePoint ℝ) :
          geodesicReflectionComp g h • p = extGeodesicReflection g (extGeodesicReflection h p)

          The product of two geodesic reflections acts on ℍ ∪ ∂ℍ as the composite of the reflections.

          source
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_smul (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
          geodesicReflectionComp g h • z = (geodesicReflection g) ((geodesicReflection h) z)

          The product of two geodesic reflections acts on ℍ as the composite of the reflections.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_inv (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          (geodesicReflectionComp g h)⁻¹ = geodesicReflectionComp h g

          Reversing the order of two reflections inverts their product.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_self (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          geodesicReflectionComp g g = 1

          The product of a reflection with itself is the identity.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_mul_geodesicReflectionComp (g h k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          geodesicReflectionComp g h * geodesicReflectionComp h k = geodesicReflectionComp g k

          Products of reflections compose: the middle reflection cancels.

          source
          theorem TauCeti.UpperHalfPlane.mul_geodesicReflectionComp_mul_inv (k g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          k * geodesicReflectionComp g h * k⁻¹ = geodesicReflectionComp (k * g) (k * h)

          Conjugating a product of reflections by k gives the product of the reflections in the moved geodesics.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_mul_pslS_left (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          geodesicReflectionComp (g * pslS) h = geodesicReflectionComp g h

          Reversing the orientation of the first line does not change the product of reflections.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_mul_pslS_right (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
          geodesicReflectionComp g (h * pslS) = geodesicReflectionComp g h

          Reversing the orientation of the second line does not change the product of reflections.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_mul_dilation_left (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) :
          geodesicReflectionComp (g * ↑(Matrix.SpecialLinearGroup.dilation s)) h = geodesicReflectionComp g h

          Shifting the parametrisation of the first line does not change the product of reflections.

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_mul_dilation_right (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) :
          geodesicReflectionComp g (h * ↑(Matrix.SpecialLinearGroup.dilation s)) = geodesicReflectionComp g h

          Shifting the parametrisation of the second line does not change the product of reflections.

          Two geodesic lines with a common ideal endpoint #

          source
          @[simp]
          theorem TauCeti.UpperHalfPlane.geodesicReflectionComp_upperRightHom (a b : ℝ) :
          geodesicReflectionComp (Matrix.ProjectiveSpecialLinearGroup.upperRightHom a) (Matrix.ProjectiveSpecialLinearGroup.upperRightHom b) = Matrix.ProjectiveSpecialLinearGroup.upperRightHom (2 * (a - b))

          The product of the reflections in the vertical lines Re z = a and Re z = b, the geodesic lines of the translations by a and by b, is the translation by 2 (a - b).

          source
          theorem TauCeti.UpperHalfPlane.isParabolic_geodesicReflectionComp_iff {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hgh : g • OnePoint.infty = h • OnePoint.infty) :
          (geodesicReflectionComp g h).IsParabolic ↔ g • ↑0 ≠ h • ↑0

          Reflections in two lines with a common ideal endpoint. If the geodesic lines of g and h have the same forward endpoint, the product of the reflections in them is parabolic exactly when their backward endpoints differ, that is, when the lines are distinct.

          Reflecting a vertex across a side with acute angles #

          source
          theorem TauCeti.UpperHalfPlane.toComplex_extGeodesicReflection_one (p : UpperHalfPlane ⊕ OnePoint ℝ) :
          toComplex (extGeodesicReflection 1 p) = -(starRingEnd ℂ) (toComplex p)

          Reflection in the imaginary axis is z ↦ -conj z on points of ℍ ∪ ∂ℍ read as complex numbers.

          source
          theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mem_extLeftHalfPlane_geodesicFromTo_left {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {a b c : UpperHalfPlane ⊕ OnePoint ℝ} (hab : IsGeodesicFromTo g a b) (hc : c ∈ extLeftHalfPlane g) (hangle : vertexAngle a c b < Real.pi / 2) :
          extGeodesicReflection g c ∈ extLeftHalfPlane (geodesicFromTo c a)

          Reflecting across a side with an acute angle. Let the geodesic line of g run from a to b, and let c lie strictly to its left. If the angle at a between the directions to c and b is acute, then the mirror image of c in the line lies strictly to the left of the geodesic from c to a.

          source
          theorem TauCeti.UpperHalfPlane.extGeodesicReflection_mem_extLeftHalfPlane_geodesicFromTo_right {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {a b c : UpperHalfPlane ⊕ OnePoint ℝ} (hab : IsGeodesicFromTo g a b) (hc : c ∈ extLeftHalfPlane g) (hangle : vertexAngle b a c < Real.pi / 2) :
          extGeodesicReflection g c ∈ extLeftHalfPlane (geodesicFromTo b c)

          Reflecting across a side with an acute angle at its end. Let the geodesic line of g run from a to b, and let c lie strictly to its left. If the angle at b between the directions to a and c is acute, then the mirror image of c in the line lies strictly to the left of the geodesic from b to c.