Skip to content

General linear groups

Finite general linear groups over possibly noncommutative semirings and rings: Kronecker products of matrix units with reversed identity-factor inverse witnesses, elementary units, ordered commutators, relative normal closures inside elementary groups, finite stabilization, Whitehead block factorization and doubled relative membership and lifting; rectangular block units for independent finite indices with explicit diagonal units; reindexing, nil and quasiregular ideals, congruence subgroups and quotient lifting, nonunital unitization, and matrix trace modulo additive commutators. Scalar unit reflection for Ring-to-Semiring homomorphisms forces quasi-regularity of the canonical two-sided kernel without surjectivity; for surjective maps it is equivalent to this kernel condition. Source and target universes are independent, with no commutativity or local-ring hypothesis. A square-zero kernel of any Ring-to-Semiring homomorphism identifies units mapping to 1 with the additive kernel via u - 1 and 1 + x; the inverse unit has value 1 - x. All mixed kernel products must vanish, with no surjectivity assumption. For left ideals I, J with I^2 contained in J, original-ring principal units map to the additive layer I/(I intersect J); Jacobson containment of I makes the map surjective and identifies its kernel quotient with that layer. Neither two-sidedness nor J contained in I is required. Dual-number GL, SL and scalar-unit reduction kernels, determinant/trace, coefficient maps and the left-conjugation adjoint action use commutative rings. The trace quotient is an additive group, not a quotient ring; its corner inverse requires a chosen matrix index. A Steinberg presentation adds elementary-symbol relations, universal lifts and a finite map onto the elementary subgroup, without opposite-root or central-extension assertions. Over iterated dual numbers, Mathlib's GL units have an ordered commutator equal to the mixed lift of the associative matrix bracket; its outer reduction-kernel element has complete pure-inner readback. For trace-zero inputs, the refinement in Mathlib's SL group uses special-linear factors, identifies the ordered mixed commutator and reads back its pure-inner trace-zero coefficient in the outer SL kernel. Elementary unit-pivot diagonalization, product-one diagonal membership, continuous elementary paths and finite special-linear elementary neighborhoods add algebraic and topological interfaces with their respective unit-minor, path-connectedness and open-scalar-unit hypotheses. Zero-product rectangular blocks over any ring yield a unit 1 + AB whose stabilization is an elementary ordered commutator of block shears. Stable general linear groups form a direct limit over semirings; over rings their stable elementary subgroup is perfect and equals the commutator subgroup, with quotient canonically the abelianization. Over commutative rings the stable determinant and its quotient and abelianization factorizations admit rank-one sections; the elementary subgroup lies in the determinant kernel. Ordered products of matrices with entries in a left ideal I over a semiring have entries in I raised to the list length, for independent finite decidable indices, including empty lists and indices. Repeated factors recover the matrix-power bound. Any exponent annihilating the whole ideal also annihilates a matrix whose entries lie in it.

Quoted from the project description in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

6 articles: 5 for highlights of its formalization.yaml whose declarations the scan finds and 1 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/general-linear-groups, read at commit a2199cf0 (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “independent agent review; no human mathematical review claimed”.
  • Review notes: “Reviews and build evidence concern specific revisions. No complete Weibel source correspondence or source formalization is asserted.”
  • Automation: agent; framework “AI agents using Lean and Lake”; tool setup “Formal Frontier Agents developed Lean proofs and ordinary-import clients using mathlib APIs, compiler feedback and Lake. The clients exercise the public interfaces and degenerate examples; the historical API reference does not enumerate all present results.”; prompting notes “AI-assisted formalization states hypotheses explicitly and uses kernel-checked Lean proofs.”
  • Automation notes: “AI agents produced code, proofs and documentation with compiler feedback; no human mathematical review or source-author endorsement is asserted. AI generation alone does not establish originality, copyright ownership or third-party redistribution rights.”

Literature

The sources its formalization.yaml names, with their relationship to it.

Builds on

Used by

Highlights

DefinitionPrincipal-unit quotients and Jacobson lifting#

For left ideals I, J in any ring R with I^2 ≤ J and I ≤ Ring.jacobson R, the subgroup U(I) = {u : Rˣ | u - 1 ∈ I} modulo the kernel of u ↦ [u - 1] is canonically isomorphic to the additive quotient I / (I ∩ J), with inverse [x] ↦ [1 + x], without two-sidedness or J ≤ I.

Quoted from the highlights in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanIdeal.principalUnitsQuotientEquiv · Ideal.principalUnitsToQuotient_ker · Ideal.principalUnitsQuotientEquiv_symm_mk

DefinitionSquare-zero unit kernels and conjugation#

For any ring homomorphism f : R →+* S from a possibly noncommutative ring to a semiring with (ker f)^2 = 0, the units mapping to 1 are isomorphic to the additive group ker f by u ↦ u - 1 and x ↦ 1 + x, and conjugation by any g : Rˣ corresponds to x ↦ g * x * g⁻¹, without a surjectivity hypothesis.

Quoted from the highlights in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanRingHom.unitsKerEquivOfSquareZero · RingHom.unitsKerEquivOfSquareZero_conj_apply_coe

TheoremNilpotent principal-unit groups#

For any left ideal I of a possibly noncommutative ring R and any natural N with I^N = 0, the principal-unit subgroup {u : Rˣ | u - 1 ∈ I} is nilpotent of class at most N - 1, using natural subtraction and including the trivial-subgroup cases N = 0 and N = 1.

Quoted from the highlights in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanIdeal.isNilpotent_stabilizer_quotient_one_of_pow_eq_bot · Ideal.nilpotencyClass_stabilizer_quotient_one_le_of_pow_eq_bot

DefinitionPositive principal-unit layer commutator pairings#

For a left ideal I in any ring R and positive degrees a, b, the bracket xy - yx descends to an integer-bilinear pairing of successive ideal layers in degree a+b, and its restriction along the injective principal-unit symbols is the pairing represented by the ordered commutator of original-ring units, without two-sidedness, Jacobson containment or symbol surjectivity.

Quoted from the highlights in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanIdeal.powLayerCommutator · Ideal.principalUnitsPowLayerCommutator · Ideal.principalUnitsPowLayerCommutator_mk_mk · Ideal.principalUnitsPowLayerSymbol_commutator

TheoremFunctorial symbols and Jacobson equivalences#

On positive layers, unital ring maps carrying left ideals into left ideals induce integer-linear maps preserving symbols and commutator pairings, while Jacobson-contained ideals have symbol equivalences with natural inverses when both ideals satisfy the radical condition, and pointwise-nil or power-nilpotent left ideals have surjective symbols.

Quoted from the highlights in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanIdeal.principalUnitsPowLayerSymbol_map · Ideal.powLayerMap_commutator · Ideal.principalUnitsPowLayerMap_commutator · Ideal.principalUnitsPowLayerEquiv · Ideal.principalUnitsPowLayerEquiv_symm_map · Ideal.principalUnitsPowLayerSymbol_surjective_of_forall_isNilpotent · Ideal.principalUnitsPowLayerSymbol_surjective_of_pow_eq_bot

Headline results

Quoted from the headline results in README.md of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Elementary generation over Euclidean domains. For any EuclideanDomain R, an invertible finite matrix belongs to the elementary subgroup exactly when its determinant is one, including empty and singleton index types. The stable elementary quotient is multiplicatively equivalent to Rˣ, with the existing quotient determinant as forward map and the existing rank-one section as inverse. Both directions commute with arbitrary ring homomorphisms between Euclidean domains. Euclidean elementary generation.

Signed swaps and even permutation matrices. Over any possibly noncommutative Ring R, the word e_ij(1) e_ji(-1) e_ij(1) gives the signed coordinate swap with block [0,1;-1,0]. Every even permutation of a finite decidable basis gives an element of the original finite elementary subgroup, including ranks zero, one and two and zero rings. The permutation unit sends e_i to e_(σ i); no parity converse is asserted in characteristic two. The argument follows Weibel, The K-book, III.1.2.1, using Mathlib's permutation units and generation of the alternating group by three-cycles. Signed coordinate swaps and even permutations.

Upper-triangular semiring nilpotence. For an arbitrary, possibly noncommutative Semiring R and an independently-universed finite linearly ordered index type, an upper triangular matrix is nilpotent if and only if every diagonal entry is nilpotent. Given e : ι → ℕ killing the corresponding diagonal entries, the bound is A ^ (∑ i, e i) = 0, including empty indices and zero exponents. The strict Fin n predicate uses only Zero; its support bound holds over NonUnitalNonAssocSemiring and its nilpotence over NonUnitalSemiring. Positive-power index n means n + 1 factors, not an exact nth-power bound. The unitization and relative general linear constructions require NonUnitalRing. Upper-triangular nilpotence, nonunital powers and strict triangularity.

Finite block-triangular units. Over any possibly noncommutative Ring, a block-triangular matrix on a finite decidable index type is a unit if each equality-fiber diagonal block is a unit and its represented labels form a strict chain in a Preorder. For a PartialOrder, a chain for ≤ suffices. The index, label and coefficient universes are independent. Labels have decidable equality but need not be finite or globally linearly ordered, and block sizes may differ. Empty indices, empty fibers and zero rings are included. Over a Semiring, the converse holds if each original diagonal-block matrix monoid is Dedekind-finite: an ambient matrix unit then has unit diagonal blocks. Separately, given [Invertible M] and unit diagonal blocks, the given inverse ⅟M is block triangular over a semiring, with no direct-finiteness assumption. Both directions retain the same represented-chain hypotheses; neither asserts semiring sufficiency from diagonal units or derives matrix direct finiteness from scalar direct finiteness. Block-unit criterion.

Matrix ideal-power bounds and nilpotence. For a Semiring R and a left ideal I : Ideal R, an ordered list As of square matrices with entries in I has (As.prod) i j ∈ I ^ As.length. The finite decidable index type has a universe independent of the coefficients. Repeated factors recover (A ^ k) i j ∈ I ^ k. Any exponent annihilating the whole ideal also annihilates the matrix, so IsNilpotent I implies IsNilpotent A. Empty lists, empty indices and zero semirings are included, without two-sidedness or commutativity. Right-append induction matches I ^ (k + 1) = I ^ k * I, without a multiplicative monoid on arbitrary left ideals; pointwise nilness of an arbitrary ideal does not give a uniform exponent. For a CommSemiring R, however, a finite square matrix with nilpotent entries is nilpotent: its finitely generated entry ideal is contained in the nilradical and is therefore nilpotent. This needs no Noetherian hypothesis and includes empty indices and zero semirings. Ordered-product bound and nilpotence, nilpotent entries, nonzero dual-number diagonal, nonzero matrix over ZMod 4.

Kronecker products of matrix units. Over any Semiring, the Kronecker product of two unit matrices is a unit, for independently-universed finite decidable square indices, including empty indices and zero semirings. The ordered factorization (A ⊗ₖ 1) * (1 ⊗ₖ B), for chosen input units with stored inverse values A' and B', supplies the reversed inverse witness (1 ⊗ₖ B') * (A' ⊗ₖ 1); tensoring input inverses is not valid in general over noncommutative coefficients. The rectangular mixed identity needs only a NonAssocSemiring and finite, decidable middle indices. Over commutative coefficients, the extracted unit agrees with mathlib's general linear Kronecker construction. Unit preservation, operational examples.

Single-entry matrix corners. For a Semiring R, finite decidable indices and a chosen index i, the corner of Matrix ι ι R at the diagonal matrix unit single i i 1 is ring-equivalent to R by extracting the (i,i) entry; its inverse inserts a coefficient there. The corner identity is the matrix unit, which need not be the ambient matrix identity. The equivalence also covers noncommutative and zero semirings. Corner equivalence, concrete clients.

Whitehead factorization and doubled lifting. Over any Ring, the block diagonal diag(g, g⁻¹) of a unit is elementary. A surjective ring homomorphism lifts this doubled block as a unit; it need not lift the original same-rank unit. For separately finite block indices, explicitly supplied diagonal units also give rectangular upper-triangular units with ordered inverse block -(A⁻¹ * B * D⁻¹). Factorization, doubled lift, elementary membership, rectangular guide.

Stable general linear and elementary groups. Initial-segment stabilization defines a coherent system of finite general linear groups over any Semiring, whose noncommutative direct limit has finite representatives, an eventual equality criterion, compatible lifts and coefficient maps. Over any Ring, the directed union of finite elementary images is the stable commutator subgroup; it is perfect in its own right and normal in stable general linear groups. Its quotient is canonically the abelianization, naturally under coefficient maps. No finite ambient elementary normality or commutativity hypothesis is needed. Stable general linear group, stable elementary group, boundary and quotient clients.

Opposite coefficients. Over any Semiring R, inverse-transpose gives GL ι R ≃* GL ι Rᵐᵒᵖ for finite decidable indices and an equivalence of the original stable groups. Its entries are op ((g⁻¹) j i), using the unit inverse. Both directions commute with stabilization and arbitrary unital coefficient maps; double application is canonical double-opposite coefficient transport. Over a Ring R, it identifies the original stable elementary subgroups and induces an equivalence of their quotients, with representative and coefficient-naturality formulas. Empty ranks and zero semirings are allowed. Finite inverse-transpose, stable inverse-transpose, elementary quotients.

Finite coefficient products of stable groups and elementary quotients. For arbitrary Semiring R and Semiring S in independent universes, coefficient projections give StableGL (R × S) ≃* (StableGL R × StableGL S). For [Finite ι] and a family of semirings R i, evaluation gives StableGL (∀ i, R i) ≃* (∀ i, StableGL (R i)), including the empty family. Over arbitrary rings these comparisons carry the stable elementary subgroup onto the product of the elementary subgroups and induce equivalences of the existing elementary quotients. All comparisons commute with arbitrary coefficient maps; inverse-stage computations allow unequal representative ranks after passage to any common upper bound. Zero rings and rank zero are included; no unrestricted infinite-product stable-group equivalence is asserted. These extend the binary ring example in Weibel, The K-book, Example III.1.1.3. Finite coefficient products.

Matrix invariance of stable groups and elementary quotients. For 0 < n, fixed row-major flattening gives StableGL (Matrix (Fin n) (Fin n) R) ≃* StableGL R over any Semiring R. Over a Ring R, it induces an equivalence of the existing stable elementary quotients. Over a CommRing R, the transported quotient determinant on a matrix-ring unit is its ordinary finite determinant. Matrix invariance.

Stable determinant. Over a commutative ring, finite determinants induce homomorphisms on stable general linear groups, their elementary quotient and their abelianization. Rank-one units provide determinant sections; the elementary subgroup lies in the determinant kernel. The abelian elementary quotient splits as the product of its determinant kernel and the units, naturally under coefficient maps; this does not assert a product splitting of stable general linear groups. For commutative local rings, elementary matrices equal the determinant kernel, and the existing quotient determinant is an equivalence with the units. The rank-one map itself is defined over any semiring. Determinant and rank-one maps, integer and boundary examples.

Zero-product elementary stabilization. For rectangular A, B over any Ring with B * A = 0, the unit 1 + A * B has inverse 1 - A * B. Stabilizing by the identity on the other block gives exactly the ordered commutator of the upper shear of A and lower shear of B, hence an elementary unit. Both index types may be empty. Construction and factorization, integer and boundary examples.

Rectangular complement isomorphisms. In any preadditive category C : Type u with Category.{v} C, for arbitrary objects X, Y and morphisms a : X ⟶ Y, b : Y ⟶ X, the complements are simultaneously isomorphisms: IsIso (𝟙 X - a ≫ b) ↔ IsIso (𝟙 Y - b ≫ a). Their canonical inverse is inv (𝟙 X - a ≫ b) = 𝟙 X + a ≫ inv (𝟙 Y - b ≫ a) ≫ b under only IsIso (𝟙 Y - b ≫ a). The universes u, v are independent; no finiteness, biproduct or nonzero-object hypothesis is imposed. The rectangular unit-switch inverse below is a finite-matrix specialization. Criterion and inverse.

Rectangular unit switch. Over any Ring, for independently finite, decidable index types, a unit g = 1 + A * B determines a unit h = 1 + B * A with inverse 1 - B * g⁻¹ * A. Its diagonal pair diag(g, h⁻¹) is the ordered product U(A) L(B) U(-(g⁻¹ * A)) L(-(B * g)), hence elementary. Empty blocks and the zero ring are allowed; B * A = 0 recovers the zero-product stabilization commutator above. Construction and factorization, integer and boundary examples.

Ring Schur reduction. For independently finite, decidable block indices over any Ring, an invertible northwest block A makes [[A, B], [C, D]] a unit exactly when the ordered residual D - C * ⅟A * B is a unit. Given a unit residual, the corresponding block unit has an explicit ordered inverse; homomorphisms killing the elementary subgroup see only the diagonal pivot and residual, with no condition on the target group. Empty blocks and the zero ring are included. Construction and criterion, noncommutative and boundary clients.

Unit-pivot reduction and elementary diagonals. Over any CommRing, unit ordered leading minors permit two-sided elementary diagonalization; a product-one diagonal is elementary, and the unit-pivot, determinant-one criterion puts a finite GL unit in E. This is not a general SL = E theorem; the minor hypothesis is stronger than nonvanishing. More generally, if an elementary left factor can produce a unit leading entry for every invertible matrix at every successor rank, the same two-sided reduction exists at every finite rank. The latter theorem is conditional on that all-rank pivot property; it does not assert an unconditional elementary generation theorem. Unit-pivot guide, conditional pivot induction, diagonal guide.

Elementary generation over local rings. Every invertible finite matrix over a commutative local ring has elementary left and right factors reducing it to a diagonal of units, without a leading-minor hypothesis. At every finite rank, determinant one characterizes the elementary subgroup. The stable elementary subgroup is the determinant kernel, and the elementary quotient is canonically the coefficient units via the existing determinant and rank-one section. Over a field, Mathlib transvection lists give an invertible diagonal factorization. Local generation, nonfield and rank-boundary clients.

Elementary paths and SL neighborhoods. Over a topological ring, elementary GL units vary continuously with coefficients, even when the coefficient ring is noncommutative. Path-connected coefficients make the elementary subgroup path connected. For commutative coefficients, an open scalar-unit locus makes its comap in Mathlib's special linear group open and closed; additionally path-connected coefficients identify it with the identity path component. Paths guide, neighborhood guide.

TheoremScalar unit reflection and canonical quasi-regular kernels#

For f : R →+* S from a possibly noncommutative ring to a semiring, IsLocalHom f (reflection of units) makes the canonical two-sided kernel TwoSidedIdeal.ker f quasi-regular, without surjectivity, by RingHom.isQuasiregular_ker. For a surjective such map, unit reflection is equivalent to kernel quasi-regularity by RingHom.isLocalHom_iff_isQuasiregular_ker; its reverse direction is also available through RingHom.isLocalHom_of_surjective_of_isQuasiregular_ker. Mathlib supplies IsUnit (f a) ↔ IsUnit a via isUnit_map_iff; under surjectivity it also gives a surjective induced map on units. Source and target universes are independent; neither commutativity, local-ring structure, nontriviality nor nilness of the kernel is assumed. Nil kernels specialize through TwoSidedIdeal.IsNil.isQuasiregular.

Quoted from the headline results in README.md of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

Lean

Read from the source at commit a2199cf0, without running Lean.

Sources
LeanRingHom.isQuasiregular_ker

Lifting modulo quasi-regular ideals. For a two-sided ideal, its unitization general linear group identifies with the congruence kernel; quasi-regularity of every ideal element additionally makes the quotient GL map surjective. The Jacobson radical is the greatest quasi-regular ideal, and pointwise nil ideals provide examples without a shared nilpotence exponent. Kernel equivalence, quotient lifting, ideal characterization.

Trace modulo additive commutators. For a chosen index p : n, trace gives an additive equivalence from square matrices modulo additive commutators to the coefficient ring modulo additive commutators; its inverse inserts a scalar in the p,p corner. The forward map also works at empty rank. These are additive groups, not quotient rings or a K₀ descent. Equivalence and forward map. The following characteristic laws use weaker hypotheses: cyclic representatives and unit conjugation require AddCommGroup with Mul, respectively Monoid, without distributivity; raw block trace requires only AddCommMonoid and two independently-universed finite index types, without decidable equality or nonemptiness. The raw Sum-indexed block shape complements mathlib's dependent trace_blockDiagonal' formula.

Finite elementary and relative structure. Off-diagonal elementary units generate E; ordered commutator laws prove that E is perfect at rank at least three. A two-sided ideal defines the relative normal closure inside E, not a claimed same-rank normal subgroup of ambient GL. Congruence units become relatively elementary after Whitehead doubling; stabilization preserves elementary, relative and congruence inclusions. Perfectness, relative subgroup, relative Whitehead, guides.

A Steinberg presentation and universal maps. Over any Ring, for an arbitrary index type, symbols satisfy precisely the additive, disjoint-root and ordered-composable-root relations, and compatible maps extend uniquely. Finite decidable indices additionally give a surjection onto E, not onto all of GL. The reverse relation has coefficient -(b * a); no opposite-root, central-kernel or K₂ theorem is claimed. Universal lift, onto-E map, presentation guide.

Units over square-zero kernels. For a homomorphism from any Ring to any Semiring, a square-zero kernel identifies the units mapping to 1 with the additive kernel, written multiplicatively. The coordinates are u ↦ u - 1 and x ↦ 1 + x, with inverse unit 1 - x. The hypothesis kills every mixed product of kernel elements; no commutativity or surjectivity is needed. The scalar dual-number equivalence is a specialization with its explicit lift and readback preserved. This is the algebraic ingredient of Fesenko–Vostokov, Chapter I (5.4)(3), not a unit-lifting or valuation-layer quotient theorem. Equivalence and coordinate API, dual-number comparison.

Principal-unit ideal layers on original-ring units. For left ideals I, J in any Ring, with I ^ 2 ≤ J, the stock stabilizer of [1] in the quotient left module R / I maps by u ↦ [u - 1] to the additive layer I / (I ∩ J), written multiplicatively. Its kernel is exactly the relative stabilizer modulo J, which is therefore normal. If additionally I ≤ Ring.jacobson R, the map is surjective and its kernel quotient is isomorphic to that additive layer, with inverse [x] ↦ [1 + x] in the original ring. Neither ideal needs to be two-sided, and J ≤ I is not assumed. For two-sided I, the carrier agrees with the kernel of reduction on units. The nonzero-denominator model uses (3)/(9) in ZMod 27; the integer boundary explains the original-unit lifting hypothesis. Equivalence and characteristic laws, models and boundary. For a commutative domain R, a nonzero principal ideal I = Ideal.span {π} contained in Ideal.jacobson ⊥, and n ≥ 1, the original-ring unit stabilizer at I ^ n, modulo its exact coordinate kernel (the relative deeper stabilizer at I ^ (n + 1)), is equivalent to Multiplicative (R ⧸ I). It sends [1 + a * π ^ n] to [a]; the inverse returns that original-ring unit class. The target is the additive coefficient ring, not necessarily a field. Replacing π by u * π for u : Rˣ with residue unit ū multiplies a fixed class's forward coefficient by (ū⁻¹) ^ n; the inverse at a fixed coefficient uses the old inverse with parameter multiplied by ū ^ n. Normality and surjectivity are conclusions, not assumptions; exponent zero instead gives multiplicative reduction. Coefficients and generator-change laws, coefficient clients.

Principal-unit commutators and nilpotence. Over any Ring R, including noncommutative and zero rings, write U(I) for the stock Rˣ-stabilizer of 1 in the quotient left module R ⧸ I. For two-sided I, this is the kernel of reduction on units to the quotient ring. Arbitrary left ideals A, B satisfy [U(A), U(B)] ≤ U(A * B + B * A). For two-sided I, [U(I ^ a), U(I ^ b)] ≤ U(I ^ (a + b)) for all a, b : ℕ, including zero, without a nilpotence assumption. For any left ideal I, the lower central series has LCS(k) ≤ U(I ^ (k + 1)), with zeroth term U(I). If I ^ N = ⊥, then U(I) is nilpotent of class at most N - 1 (natural subtraction); N = 0 and N = 1 give the trivial subgroup. This is not a nilpotence claim about the full unit group. Positive additive layers use the preceding ideal-layer and power-coordinate API, not an additive equivalence at exponent zero. Commutator bounds and nilpotence.

Leading coordinates of principal-unit commutators. For any left ideal I in any Ring R and positive a, b, let x = u - 1 ∈ I ^ a and y = v - 1 ∈ I ^ b for original-ring units u, v. Then [u, v] - 1 - (x * y - y * x) ∈ I ^ (a + b + min a b). In particular, [u, v] - 1 and x * y - y * x have the same class in the quotient left module R ⧸ I ^ (a + b + 1). No two-sidedness, commutativity or nilpotence is needed; the commutator is u * v * u⁻¹ * v⁻¹, with no degree-dependent sign. Coordinate estimate and quotient equality, API guide.

Positive principal-unit layer pairings. For any left ideal I in any Ring R and a, b : ℕ+, the bracket xy - yx descends to an integer-bilinear pairing of successive ideal layers in degrees a, b and a + b. The additive positive unit layers embed in these ideal layers by the injective symbol [u] ↦ [u - 1]; their pairing is represented by the ordered commutator of original-ring units. Both pairings are alternating, with ordinary negation under swapping and the canonical degree cast. No two-sidedness, Jacobson condition or symbol surjectivity is assumed, and no degree-zero additive layer is asserted. Pairings and characteristic laws, API guide.

Functorial symbols and Jacobson equivalences. A unital ring map carrying a left ideal I into J induces integer-linear maps on their positive ideal and unit layers, preserving symbols and both commutator pairings. The maps respect identities and composition, without injectivity, surjectivity or radical assumptions on the ring map. If I ≤ Ring.jacobson R, its symbol is an integer-linear equivalence, with inverse represented by the original-ring unit 1 + x. Inverse naturality requires the Jacobson condition on both source and target ideals. Symbols are also surjective when every element of the left ideal is nilpotent, or when I ^ N = ⊥, including N = 0, 1; no two-sidedness or common exponent is assumed for the pointwise-nil result. Forward maps and naturality, Equivalences and nil lifting, API guide.

Images of principal-unit subgroups. For a ring homomorphism f : R →+* S with Ring R and Ring S in independent universes, and a left ideal I ≤ Ideal.jacobson ⊥, a unit u : Sˣ lies in the image under Units.map f.toMonoidHom of the original R-unit stabilizer of [1] in the quotient left module R ⧸ I exactly when ∃ a ∈ I, f a = (u : S) - 1. This uses the set image of ideal elements, not the extended ideal Ideal.map f I. The map need not be injective, and neither ring needs to be commutative; no domain, local-ring or valuation hypothesis is needed. Image membership criterion.

Finite exponential and logarithm coordinates. Over a possibly noncommutative or zero rational algebra, Mathlib's finite exponential, packaged as a unit, and a concrete logarithm give a plain equivalence between nilpotent elements and units u with nilpotent coordinate u - 1. This restricts to the elements of any pointwise-nil left ideal I and its principal-unit stabilizer of 1 in the quotient left module R ⧸ I; neither two-sidedness nor a uniform nilpotence exponent is required. Addition and product laws require commuting inputs; integer multiples correspond to integer powers in the unit group. These are equivalences of types, not group equivalences. Exponential units and logarithm, principal-unit restriction.

First-order dual-number kernels and conjugation. Over any CommRing, the multiplicative reduction identity fibers of Mathlib's GL and SL groups and of scalar units identify with additive matrices, trace-zero matrices and scalars. The determinant corresponds to trace; arbitrary ring-hom coefficient maps commute with these constructions without being implicitly R-linear. Unit left conjugation corresponds to g * X * g⁻¹, even for nonconstant dual-number units; the SL-kernel action uses SL conjugators. First-order fiber groups are abelian, so their commutator is not the generally nonzero matrix Lie bracket. Kernel equivalences, determinant/trace, adjoint guide.

Mixed dual-number GL and SL commutators. For finite matrices over a CommRing, units over iterated dual numbers satisfy the ordered identity [1 + εX, 1 + ηY] = 1 + εη(XY - YX) with full outer-kernel readback. When each input is trace zero, special-linear factors yield the analogous identity in Mathlib's SL group and trace-zero readback. The ε-factor reduces to the inner lift liftGL X (in SL, liftSL X), usually not 1: this is not a bracket of two elements of the abelian first-order outer kernel, nor a global Lie- or scheme-tangent theorem. GL identity, SL identity, GL guide, SL guide.

Main results

Its formalization.yaml lists 221 main results, and the scan finds 221 of them declared in the file the yaml gives; they are on their own page, not made articles.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.