Lane Biocini
21 January 2026

Induction principles for PSL2Z forming a hierarchy:

  1. Structural (PSL2Z-ind): Direct pattern matching on S-edge/R-edge
  2. Generator-based (PSL2Z-gen-ind): Induction by "start at E, apply s or r"
  3. Extensionality (PSL2Z-η): Functions agreeing on generators are equal

The generator-based induction captures that PSL(2,ℤ) is generated by
{s, r}, while extensionality captures freeness: the generators determine
all behavior. Together these express the universal property internally.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Groups.ModularGroup.Induction where

open import MLTT.Spartan
open import Groups.ModularGroup.Type
open import Groups.ModularGroup.Base
open import Groups.ModularGroup.Properties

S-edge-ind : {P : S-edge → 𝓤 ̇ }
           → {Q : R-edge → 𝓤 ̇ }
           → P e₀
           → P e₁
           → ((re : R-edge) → Q re → P (cross re))
           → ((d : R-sgn) (se : S-edge) → P se → Q (step d se))
           → (se : S-edge) → P se

R-edge-ind : {P : S-edge → 𝓤 ̇ }
           → {Q : R-edge → 𝓤 ̇ }
           → P e₀
           → P e₁
           → ((re : R-edge) → Q re → P (cross re))
           → ((d : R-sgn) (se : S-edge) → P se → Q (step d se))
           → (re : R-edge) → Q re

S-edge-ind p₀ p₁ c t e₀         = p₀
S-edge-ind p₀ p₁ c t e₁         = p₁
S-edge-ind p₀ p₁ c t (cross re) = c re (R-edge-ind p₀ p₁ c t re)
R-edge-ind p₀ p₁ c t (step d se) = t d se (S-edge-ind p₀ p₁ c t se)

PSL2Z-ind : {P : PSL2Z → 𝓤 ̇ }
          → P E
          → P S
          → ((re : R-edge) → P (θ re) → P (s∙ re))
          → (∀ d se → P (η se) → P (ρ d se))
          → (x : PSL2Z) → P x
PSL2Z-ind {𝓤} {P} p₀ p₁ c t (η se) =
  S-edge-ind {𝓤} {λ se → P (η se)} {λ re → P (θ re)} p₀ p₁ c t se
PSL2Z-ind {𝓤} {P} p₀ p₁ c t (θ re) =
  R-edge-ind {𝓤} {λ se → P (η se)} {λ re → P (θ re)} p₀ p₁ c t re

PSL2Z-rec : {X : 𝓤 ̇ }
          → X
          → X
          → ((re : R-edge) → X → X)
          → ((d : R-sgn) (se : S-edge) → X → X)
          → PSL2Z → X
PSL2Z-rec {𝓤} {X} x₀ x₁ c t = PSL2Z-ind {𝓤} {λ _ → X} x₀ x₁ c t

PSL2Z-iter : {X : 𝓤 ̇ }
           → X → X → (X → X) → (X → X) → (X → X) → PSL2Z → X
PSL2Z-iter e s c f-cw f-ccw =
 PSL2Z-rec e s (λ _ → c) (λ { cw _ → f-cw ; ccw _ → f-ccw })

\end{code}

Having exhausted the primitive induction, recursion, and iteration
rules, using transport we can define an induction principle based on
the generators according to the universal property of Modular group
homomorphisms. This induction principle establishes a more explicit
rendition of that universal property with respect to other types
presenting generators with compatible path spaces to those of our
PSL2Z type.

\begin{code}

PSL2Z-gen-ind : {P : PSL2Z → 𝓤 ̇ }
              → P E
              → ((x : PSL2Z) → P x → P (s x))
              → ((x : PSL2Z) → P x → P (r x))
              → (x : PSL2Z) → P x
PSL2Z-gen-ind {𝓤} {P} p₀ ps pr = PSL2Z-ind p₀ (ps E p₀) c t
 where
  t : (d : R-sgn) (se : S-edge) → P (η se) → P (θ step d se)
  t cw  se p = transport P (r-η se) (pr (η se) p)
  t ccw se p = pr (r∙ se) (transport P (r-η se) (pr (η se) p))

  c : (re : R-edge) → P (θ re) → P (s∙ re)
  c re p = ps (θ re) p

PSL2Z-gen-iter : {X : 𝓤 ̇ } → X → (X → X) → (X → X) → PSL2Z → X
PSL2Z-gen-iter x₀ fs fr = PSL2Z-gen-ind x₀ (λ _ → fs) (λ _ → fr)

\end{code}

The extensionality principle: two functions f, g : PSL2Z → X that agree
on E and commute with the generator actions (f ∘ s = fs ∘ f, etc.) must
be pointwise equal. This is the internal statement that PSL(2,ℤ) is
freely generated by s and r.

\begin{code}

PSL2Z-η : {X : 𝓤 ̇ } (fs fr : X → X)
        → (f g : PSL2Z → X)
        → f E ＝ g E
        → ((x : PSL2Z) → f (s x) ＝ fs (f x))
        → ((x : PSL2Z) → g (s x) ＝ fs (g x))
        → ((x : PSL2Z) → f (r x) ＝ fr (f x))
        → ((x : PSL2Z) → g (r x) ＝ fr (g x))
        → (x : PSL2Z) → f x ＝ g x
PSL2Z-η fs fr f g base f-s g-s f-r g-r = PSL2Z-gen-ind base ind-s ind-r
 where
  ind-s : (x : PSL2Z) → f x ＝ g x → f (s x) ＝ g (s x)
  ind-s x p = f (s x)  ＝⟨ f-s x ⟩
              fs (f x) ＝⟨ ap fs p ⟩
              fs (g x) ＝⟨ g-s x ⁻¹ ⟩
              g (s x)  ∎

  ind-r : (x : PSL2Z) → f x ＝ g x → f (r x) ＝ g (r x)
  ind-r x p = f (r x)  ＝⟨ f-r x ⟩
              fr (f x) ＝⟨ ap fr p ⟩
              fr (g x) ＝⟨ g-r x ⁻¹ ⟩
              g (r x)  ∎

PSL2Z-gen-iter-E : {X : 𝓤 ̇ } (x₀ : X) (fs fr : X → X)
                 → PSL2Z-gen-iter x₀ fs fr E ＝ x₀
PSL2Z-gen-iter-E x₀ fs fr = refl

private
  iter : PSL2Z → PSL2Z
  iter = PSL2Z-gen-iter E s r²

PSL2Z-gen-iter-s : (x : PSL2Z) → iter (s x) ＝ s (iter x)
PSL2Z-gen-iter-s = PSL2Z-ind base-E base-S ind-s ind-r
 where
  base-E : iter (s E) ＝ s (iter E)
  base-E = refl

  base-S : iter (s S) ＝ s (iter S)
  base-S = refl

  ind-s : (re : R-edge) → iter (s (θ re)) ＝ s (iter (θ re))
        → iter (s (s∙ re)) ＝ s (iter (s∙ re))
  ind-s re p = iter (s (s∙ re))   ＝⟨ refl ⟩
               iter (θ re)        ＝⟨ s² (iter (θ re)) ⁻¹ ⟩
               s (s (iter (θ re))) ＝⟨ refl ⟩
               s (iter (s∙ re))   ∎

  ind-r : (d : R-sgn) (se : S-edge) → iter (s (η se)) ＝ s (iter (η se))
        → iter (s (θ step d se)) ＝ s (iter (θ step d se))
  ind-r d se p = refl

PSL2Z-gen-iter-r : (x : PSL2Z) → iter (r x) ＝ r² (iter x)
PSL2Z-gen-iter-r = PSL2Z-ind base-E base-S ind-s ind-r
 where
  base-E : iter (r E) ＝ r² (iter E)
  base-E = refl

  base-S : iter (r S) ＝ r² (iter S)
  base-S = refl

  ind-s : (re : R-edge) → iter (r (θ re)) ＝ r² (iter (θ re))
        → iter (r (s∙ re)) ＝ r² (iter (s∙ re))
  ind-s re p = refl

  ind-r : (d : R-sgn) (se : S-edge) → iter (r (η se)) ＝ r² (iter (η se))
        → iter (r (θ step d se)) ＝ r² (iter (θ step d se))
  ind-r cw  e₀         p = refl
  ind-r cw  e₁         p = refl
  ind-r cw  (cross re) p = refl
  ind-r ccw e₀         p = refl
  ind-r ccw e₁         p = refl
  ind-r ccw (cross re) p =
    let y = s (iter (θ re))
    in (r³ (r (r (r y))) ∙ r³ y) ⁻¹

\end{code}

Initiality for the twist algebra: any endomorphism f : PSL2Z → PSL2Z
satisfying f(E) = E, f ∘ s = s ∘ f, and f ∘ r = r² ∘ f equals the
canonical twist iteration. This prefigures the universal property.

\begin{code}

PSL2Z-initiality : (f : PSL2Z → PSL2Z)
                 → f E ＝ E
                 → ((x : PSL2Z) → f (s x) ＝ s (f x))
                 → ((x : PSL2Z) → f (r x) ＝ r² (f x))
                 → (x : PSL2Z) → f x ＝ iter x
PSL2Z-initiality f f-E f-s f-r =
 PSL2Z-η s r² f iter f-E f-s PSL2Z-gen-iter-s f-r PSL2Z-gen-iter-r

\end{code}