Special linear groups: reduction, centers, and coordinate descriptions

The natural reduction map SL₂(ℤ) → SL₂(ℤ/dℤ) is surjective (strong approximation for SL₂; Shimura §1.6, Serre Ch. VII) — jointly so at two coprime moduli, by the Chinese remainder theorem — and the base-change map SL(n, R) → GL(n, S) sends -I to -I. Base change is functorial: SL(n, -) carries a composite of ring homs to the composite of the induced group homs, and the identity to the identity, which is what lets a congruence on a whole matrix be reduced along a further ring map in one step rather than entry by entry. Basic coordinate descriptions for SL₂ and its image under mapGL are also recorded here for downstream matrix computations, together with what the determinant says about a matrix with a prescribed bottom row (N, p): it is the Bézout relation m p - n N = 1.

mem_center_iff_eq_one_or_eq_neg_one pins down ±I itself, which is what the base-change statement moves around: over a commutative ring without zero divisors the centre of SL₂ is exactly {±I}, the scalar form Mathlib gives having no other square roots of 1 to offer.

The general positive-size center is identified with the corresponding roots-of-unity group by specializing Mathlib's finite-index-type equivalence to Fin n.

The surjectivity is ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/SL2Surjection.lean, Chris Birkbeck). Prerequisite for the diamond operators of the ModularForms roadmap (Layer 0), where it realizes every unit of ZMod N as the lower-right entry of a matrix in Γ₀(N).

The two-modulus form generalizes an ad-hoc instance from the same project at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08 (Apache-2.0): LeanModularForms/StrongMultiplicityOne/DescentCosets.lean proves descendExtraGamma_exists for the single coprime pair (p, N / p). The statement here is the general coprime pair, and the proof is independent of the source's.

Main results

• Matrix.SpecialLinearGroup.map_intCast_zmod_surjective: strong approximation for SL₂, with Matrix.SpecialLinearGroup.map_intCast_zmod_prod_surjective its two-modulus form: reductions prescribed at coprime d and d' are realized by one integral matrix.
• Matrix.SpecialLinearGroup.map_comp and Matrix.SpecialLinearGroup.map_id: the two functor laws for base change, which support whole-matrix reduction arguments such as the level antitonicity of the principal congruence subgroups.
• Matrix.SpecialLinearGroup.mapGL_neg_one: mapGL S (-1) = -1.
• Matrix.SpecialLinearGroup.vecMul_eq_iff_eq_vecMul_inv: right multiplication of row vectors by g is inverted by g⁻¹.
• Matrix.SpecialLinearGroup is countable when its coefficient ring is.
• Matrix.SpecialLinearGroup.fin_two_mul_sub_mul_eq_one: the determinant-one identity in coordinates.
• Matrix.SpecialLinearGroup.coe_mapGL_fin_two: the entrywise matrix of mapGL S on SL₂(R), with coe_mapGL_int_rat_fin_two its ℤ-to-ℚ specialization.
• Matrix.SpecialLinearGroup.mul_sub_mul_eq_one_of_lowerRow: a bottom row (N, p) gives the Bézout relation m p - n N = 1.
• Matrix.SpecialLinearGroup.centerMulEquivRootsOfUnityFin: the center of SL(Fin n, A) is rootsOfUnity n A when 0 < n.
• Matrix.SpecialLinearGroup.mem_center_iff_eq_one_or_eq_neg_one: the centre of SL₂ is {±I} when R has no zero divisors.
• Matrix.SpecialLinearGroup.finite_center and Matrix.SpecialLinearGroup.card_center_le_two: that centre is finite, of order at most two.
• Matrix.SpecialLinearGroup.disjoint_center_iff_neg_one_notMem: the simp-normal form of the = 1 case, Disjoint (center _) Γ ↔ -I ∉ Γ.
• Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_two_iff and Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_one_iff: for a subgroup Γ ≤ SL₂, the part of the centre that Γ contains has order 2 exactly when -I ∈ Γ and 1 exactly when it does not — both under -1 ≠ 1, which fails exactly when (2 : R) = 0.
• Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_one_or_two: that order is 1 or 2, needing no hypothesis beyond NoZeroDivisors R.

References

• Shimura, Introduction to the arithmetic theory of automorphic functions, §1.6
• Serre, A course in arithmetic, Ch. VII

instance Matrix.SpecialLinearGroup.instCountable_tauCeti {R : Type u_1} [CommRing R] [Countable R] {n : Type u_2} [Fintype n] [DecidableEq n] : Countable (SpecialLinearGroup n R)

SL(n, R) is countable when the coefficient ring is, the index type being finite.

@[simp]

theorem Matrix.SpecialLinearGroup.map_id {R : Type u_1} [CommRing R] {n : Type u_2} [Fintype n] [DecidableEq n] : map (RingHom.id R) = MonoidHom.id (SpecialLinearGroup n R)

Functoriality of the induced map on special linear groups, identity law. Base change along the identity ring hom is the identity.

@[simp]

theorem Matrix.SpecialLinearGroup.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {n : Type u_4} [Fintype n] [DecidableEq n] (f : R →+* S) (g : S →+* T) : (map g).comp (map f) = map (g.comp f)

Functoriality of the induced map on special linear groups, composition law. Base change along f and then along g is base change along g ∘ f, so a composite of induced maps is again a single induced map.

theorem Matrix.SpecialLinearGroup.toGL_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (f : R →+* S) (g : SpecialLinearGroup n R) : toGL ((map f) g) = (GeneralLinearGroup.map f) (toGL g)

The inclusion into the general linear group commutes with entrywise ring maps.

theorem Matrix.SpecialLinearGroup.vecMul_eq_iff_eq_vecMul_inv {R : Type u_1} [CommRing R] {n : Type u_2} [Fintype n] [DecidableEq n] (g : SpecialLinearGroup n R) (a y : n → R) : vecMul a ↑g = y ↔ a = vecMul y ↑g⁻¹

Right multiplication of row vectors by g ∈ SL(n, R) is inverted by g⁻¹.

theorem Matrix.SpecialLinearGroup.fin_two_mul_sub_mul_eq_one {R : Type u_1} [CommRing R] (g : SpecialLinearGroup (Fin 2) R) : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0 = 1

The determinant-one identity for an element of SL₂(R), written in coordinates.

theorem Matrix.SpecialLinearGroup.coe_mapGL_fin_two {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (σ : SpecialLinearGroup (Fin 2) R) : ↑((mapGL S) σ) = !![(algebraMap R S) (↑σ 0 0), (algebraMap R S) (↑σ 0 1); (algebraMap R S) (↑σ 1 0), (algebraMap R S) (↑σ 1 1)]

The matrix of mapGL S σ, written entrywise for σ ∈ SL₂(R).

theorem Matrix.SpecialLinearGroup.coe_mapGL_int_rat_fin_two (σ : SpecialLinearGroup (Fin 2) ℤ) : ↑((mapGL ℚ) σ) = !![↑(↑σ 0 0), ↑(↑σ 0 1); ↑(↑σ 1 0), ↑(↑σ 1 1)]

The rational matrix of mapGL ℚ σ, written entrywise for σ ∈ SL₂(ℤ).

theorem Matrix.SpecialLinearGroup.mul_sub_mul_eq_one_of_lowerRow {N p : ℕ} {σ : SpecialLinearGroup (Fin 2) ℤ} (hσ10 : ↑σ 1 0 = ↑N) (hσ11 : ↑σ 1 1 = ↑p) : ↑σ 0 0 * ↑p - ↑σ 0 1 * ↑N = 1

The bottom row of an SL₂(ℤ) matrix is a Bézout relation. If it is (N, p), then the top row (m, n) satisfies m p - n N = 1.

noncomputable def Matrix.SpecialLinearGroup.centerMulEquivRootsOfUnityFin (n : ℕ) (hn : 0 < n) (A : Type u_1) [CommRing A] : ↥(Subgroup.center (SpecialLinearGroup (Fin n) A)) ≃* ↥(rootsOfUnity n A)

For 0 < n, the center of SL(Fin n, A) is the group of nth roots of unity.

Equations

• Matrix.SpecialLinearGroup.centerMulEquivRootsOfUnityFin n hn A = (Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' ⟨0, hn⟩).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem Matrix.SpecialLinearGroup.coe_centerMulEquivRootsOfUnityFin_apply (n : ℕ) (hn : 0 < n) (A : Type u_1) [CommRing A] (c : ↥(Subgroup.center (SpecialLinearGroup (Fin n) A))) : ↑↑((centerMulEquivRootsOfUnityFin n hn A) c) = ↑↑c ⟨0, hn⟩ ⟨0, hn⟩

The center equivalence reads off the upper-left entry of a central matrix.

@[simp]

theorem Matrix.SpecialLinearGroup.coe_centerMulEquivRootsOfUnityFin_symm_apply (n : ℕ) (hn : 0 < n) (A : Type u_1) [CommRing A] (ζ : ↥(rootsOfUnity n A)) : ↑↑((centerMulEquivRootsOfUnityFin n hn A).symm ζ) = (scalar (Fin n)) ↑↑ζ

The inverse center equivalence sends a root of unity to its scalar matrix.

@[simp]

theorem Matrix.SpecialLinearGroup.mapGL_neg_one {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [CommRing S] [Algebra R S] [Fact (Even (Fintype.card n))] : (mapGL S) (-1) = -1

-I maps to -I under SL(n, R) → GL(n, S).

@[simp]

theorem Matrix.SpecialLinearGroup.mem_center_iff_eq_one_or_eq_neg_one {R : Type u_1} [CommRing R] [NoZeroDivisors R] {γ : SpecialLinearGroup (Fin 2) R} : γ ∈ Subgroup.center (SpecialLinearGroup (Fin 2) R) ↔ γ = 1 ∨ γ = -1

The centre of SL₂ is {±I} over any commutative ring without zero divisors.

Matrix.SpecialLinearGroup.mem_center_iff puts a central element in scalar form r • I with r ^ 2 = 1; without zero divisors the only such scalars are ±1, which turns that existential into an alternative. The hypothesis is needed, not incidental — over ZMod 8 the scalar 3 also squares to 1, so the centre is strictly larger than {±I} there.

@[simp] because the rewrite terminates: it takes a structured membership to a disjunction of equalities, and nothing rewrites γ ∈ Subgroup.center _ first — Mathlib's general Subgroup.mem_center_iff is @[to_additive] but carries no simp attribute.

theorem Matrix.SpecialLinearGroup.finite_center {R : Type u_1} [CommRing R] [NoZeroDivisors R] : Finite ↥(Subgroup.center (SpecialLinearGroup (Fin 2) R))

The centre of SL₂ is finite: by mem_center_iff_eq_one_or_eq_neg_one it is the set {±I}, which has at most two elements — exactly two unless 1 = -1 in R, where it is a singleton.

theorem Matrix.SpecialLinearGroup.card_center_le_two {R : Type u_1} [CommRing R] [NoZeroDivisors R] : Nat.card ↥(Subgroup.center (SpecialLinearGroup (Fin 2) R)) ≤ 2

The centre of SL₂ has at most two elements. Stated as a bound rather than an equality because 1 = -1 when R has characteristic 2, where the centre is trivial.

This is a strictly weaker statement than finiteness: Nat.card is 0 on an infinite type, so ≤ 2 alone would also hold for an infinite centre. Callers that need both take finite_center as well.

theorem Matrix.SpecialLinearGroup.card_center_eq_two {R : Type u_1} [CommRing R] [NoZeroDivisors R] (hne : -1 ≠ 1) : Nat.card ↥(Subgroup.center (SpecialLinearGroup (Fin 2) R)) = 2

The centre of SL₂ has exactly two elements once -I ≠ I. card_center_le_two is the unconditional bound; this is the value, and it is what a consumer evaluating the centre factor of a stabiliser splitting needs. In characteristic 2 the hypothesis fails and the centre is the singleton {I}.

theorem Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_one_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] (Γ : Subgroup (SpecialLinearGroup (Fin 2) R)) : Nat.card ↥((Subgroup.center (SpecialLinearGroup (Fin 2) R)).subgroupOf Γ) = 1 ↔ -1 ∉ Γ

The complementary case: the factor is 1 exactly when -I ∉ Γ, i.e. when the matrix and projective stabiliser orders agree.

@[simp]

theorem Matrix.SpecialLinearGroup.disjoint_center_iff_neg_one_notMem {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] (Γ : Subgroup (SpecialLinearGroup (Fin 2) R)) : Disjoint (Subgroup.center (SpecialLinearGroup (Fin 2) R)) Γ ↔ -1 ∉ Γ

Γ meets the centre only in the identity exactly when it does not contain -I. Disjoint of subgroups is triviality of the intersection, not emptiness — 1 lies in both however Γ is chosen — so the content is that -I is the only other candidate. This is card_center_subgroupOf_eq_one_iff restated at its simp-normal form: simp rewrites Nat.card (center.subgroupOf Γ) = 1 through Subgroup.card_eq_one and Subgroup.subgroupOf_eq_bot into Disjoint (center _) Γ, and this is the rule that then finishes the job. Stating it separately is what makes the = 1 case simp-reachable at all, since the cardinality form cannot itself carry @[simp].

Needs (2 : R) ≠ 0 for the same reason as the = 2 companion: in characteristic 2 the centre is the singleton {I}, so it is disjoint from every Γ — while -I = I ∈ Γ for every Γ, including ⊥, since I always lies in a subgroup. Without the hypothesis the equivalence fails for all Γ, not merely for nontrivial ones.

@[simp]

theorem Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_two_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] (Γ : Subgroup (SpecialLinearGroup (Fin 2) R)) : Nat.card ↥((Subgroup.center (SpecialLinearGroup (Fin 2) R)).subgroupOf Γ) = 2 ↔ -1 ∈ Γ

The ±I factor is 2 exactly when -I ∈ Γ. The part of the centre that Γ contains is {I} or {±I} according to whether Γ contains -I, so the centre factor in the stabiliser splitting for a subgroup of SL₂ is decided by that single membership.

Needs -1 ≠ 1: in characteristic 2 the centre is the singleton {I} and the count is always 1. The unindexed card_center_subgroupOf_eq_one_or_two needs no such hypothesis.

theorem Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_one_or_two {R : Type u_1} [CommRing R] [NoZeroDivisors R] (Γ : Subgroup (SpecialLinearGroup (Fin 2) R)) : Nat.card ↥((Subgroup.center (SpecialLinearGroup (Fin 2) R)).subgroupOf Γ) = 1 ∨ Nat.card ↥((Subgroup.center (SpecialLinearGroup (Fin 2) R)).subgroupOf Γ) = 2

The ±I factor is always 1 or 2, with no hypothesis on R beyond NoZeroDivisors: the = 1 case is what characteristic 2 gives, where -I = I and the centre is the singleton {I}. This is the form for a consumer that needs only the two-way split and not the -I ∈ Γ membership that decides between them.

@[simp]

theorem Matrix.SpecialLinearGroup.inv_apply_one_zero {R : Type u_1} [CommRing R] (M : SpecialLinearGroup (Fin 2) R) : ↑M⁻¹ 1 0 = -↑M 1 0

The (1,0) coordinate of the inverse of an SL₂ element, from SL2_inv_expl.

@[simp]

theorem Matrix.SpecialLinearGroup.inv_apply_one_one {R : Type u_1} [CommRing R] (M : SpecialLinearGroup (Fin 2) R) : ↑M⁻¹ 1 1 = ↑M 0 0

The (1,1) coordinate of the inverse of an SL₂ element, from SL2_inv_expl.

@[simp]

theorem Matrix.SpecialLinearGroup.inv_apply_zero_zero {R : Type u_1} [CommRing R] (M : SpecialLinearGroup (Fin 2) R) : ↑M⁻¹ 0 0 = ↑M 1 1

The (0,0) coordinate of the inverse of an SL₂ element, from SL2_inv_expl.

@[simp]

theorem Matrix.SpecialLinearGroup.inv_apply_zero_one {R : Type u_1} [CommRing R] (M : SpecialLinearGroup (Fin 2) R) : ↑M⁻¹ 0 1 = -↑M 0 1

The (0,1) coordinate of the inverse of an SL₂ element, from SL2_inv_expl.

theorem Matrix.SpecialLinearGroup.map_intCast_zmod_surjective {d : ℕ} : Function.Surjective ⇑(map (Int.castRingHom (ZMod d)))

Strong approximation for SL₂ over ℤ: the reduction map SL₂(ℤ) → SL₂(ℤ/dℤ) is surjective.

theorem Matrix.SpecialLinearGroup.map_intCast_zmod_prod_surjective {d d' : ℕ} (hcop : d.Coprime d') : Function.Surjective ⇑((map (Int.castRingHom (ZMod d))).prod (map (Int.castRingHom (ZMod d'))))

Strong approximation for SL₂ at two coprime moduli: for coprime d and d', the joint reduction SL₂(ℤ) → SL₂(ℤ/dℤ) × SL₂(ℤ/d'ℤ) is surjective. So a prescribed reduction modulo d and a prescribed reduction modulo d' are realized simultaneously by a single integral matrix.