Projective line over a commutative ring; Borel subgroup of SL₂ #

Definition: ModularCurve_ProjectiveLine (645d7c19-655a-5a1f-81d2-89ea49d002be), by Claude, 2026-09-05.

Over a commutative ring $R$, a pair $(a,c)\in R^2$ is called a unimodular row, IsUnimodularRow a c, when it admits a Bézout relation: there exist $x,y\in R$ with $xa+yc=1$. Two trivial instances are recorded, $(1,t)$ and $(m,1)$, together with the fact that unimodularity is preserved by any ring homomorphism $f:R\to S$, applied entrywise. The subtype UnimodularRow R consists of the pairs $v\in R\times R$ satisfying this predicate, and unimodularRowSetoid R equips it with the equivalence relation $v\sim w$ iff there is a unit $u\in R^\times$ with $u\,v_1=w_1$ and $u\,v_2=w_2$; reflexivity, symmetry and transitivity come from $1$, $u^{-1}$ and products of units. The projective line ProjectiveLine R is defined to be the quotient of UnimodularRow R by this relation, so $\mathbb{P}^1(R)$ is here the set of unimodular rows up to scaling by $R^\times$, a quotient of a chosen model by a congruence rather than an abstractly characterised object. It is finite whenever $R$ is. Functoriality is provided by ProjectiveLine.map f, induced by entrywise application of a ring homomorphism $f:R\to S$ (well defined because $f$ carries units to units), with the expected description of its value on the class of a unimodular row.

The second section defines borel R, the subgroup of $\mathrm{SL}_2(R)$ whose carrier is the set of matrices $M$ with $M_{1,0}=0$ (indices in Fin 2), i.e. the upper-triangular matrices of determinant $1$; closure under multiplication and inversion is checked from the explicit formulae for $2\times 2$ products and for the inverse of an element of $\mathrm{SL}_2$. The membership criterion mem_borel_iff states that $A\in$ borel R is exactly the condition $A_{1,0}=0$.

Relation to Mathlib. Mathlib's Projectivization is built for vector spaces over a division ring; the projective line of a commutative ring defined here is the project's own construction, as is the Borel subgroup of Matrix.SpecialLinearGroup (Fin 2) R.

Where it is used. These definitions serve the computation of the index of $\Gamma_0(N)$: left cosets of borel in $\mathrm{SL}_2(R)$ correspond to points of $\mathbb{P}^1(R)$ through the class of the first column, and for $R=\mathbb{Z}/N$ one has $\#\mathbb{P}^1(\mathbb{Z}/N)=\psi(N)$, with $\Gamma_0(N)$ the preimage of borel (ZMod N) under reduction.

source

def ModularCurve.IsUnimodularRow {R : Type u_1} [CommRing R] (a c : R) :

Prop

The two entries generate the unit ideal, equivalently a * x + c * y = 1 is solvable.

Equations

ModularCurve.IsUnimodularRow a c = ∃ (x : R) (y : R), x * a + y * c = 1

Instances For

source

theorem ModularCurve.isUnimodularRow_one_left {R : Type u_1} [CommRing R] (t : R) :

IsUnimodularRow 1 t

source

theorem ModularCurve.isUnimodularRow_one_right {R : Type u_1} [CommRing R] (m : R) :

IsUnimodularRow m 1

source

theorem ModularCurve.IsUnimodularRow.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {a c : R} (h : IsUnimodularRow a c) :

IsUnimodularRow (f a) (f c)

source

@[reducible, inline]

abbrev ModularCurve.UnimodularRow (R : Type u_3) [CommRing R] :

Type u_3

A pair of ring elements generating the unit ideal.

Equations

ModularCurve.UnimodularRow R = { v : R × R // ModularCurve.IsUnimodularRow v.1 v.2 }

Instances For

source

@[instance_reducible]

instance ModularCurve.unimodularRowSetoid (R : Type u_3) [CommRing R] :

Setoid (UnimodularRow R)

Equations

ModularCurve.unimodularRowSetoid R = { r := fun (v w : ModularCurve.UnimodularRow R) => ∃ (u : Rˣ), ↑u * (↑v).1 = (↑w).1 ∧ ↑u * (↑v).2 = (↑w).2, iseqv := ⋯ }