Skip to content

Projective modules

Row-finite linear systems with target satisfying Module.Baer have full solutions whenever every finite set of rows has a solution. Over a semisimple ring this holds for every left module, including modules over division rings; scalars, targets, rows and coordinates have independent universes. Solutions are arbitrary coordinate functions, not necessarily finitely supported functions. Reusable Lean theory of projective modules: finite-projective dual and evaluation base change, invertible modules, exterior algebras and powers, determinants, bounded cancellation and countable absorption, infinite free coordinates, finite stable presentations and IBN-only integer-rank independence, balanced tensor products, right scalar extension and chosen right-free coefficient transport along arbitrary unital semiring homomorphisms, exactness, local and PID freeness, preadditive stable module categories, countably generated submodules over left-Noetherian rings, and locally constant rank and componentwise-free classification. Noncommutative and commutative results retain their distinct hypotheses; rank classification is not asserted for all finite projectives over arbitrary rings. Given an equivalence of module categories over arbitrary rings, finite generation is preserved and reflected with independent scalar and carrier universes. Finite projectivity is preserved with an unrestricted source carrier and target carrier at its scalar/carrier maximum, and is reflected when both carriers are at their corresponding maxima. No linearity, commutativity or freeness premise is imposed on this equivalence interface. Ordinary-coefficient evaluation gives an R-linear equivalence M ≃ₗ[R] ((M →ₗ[R] R) →ₗ[Rᵐᵒᵖ] R) for any semiring R and finitely generated projective left R-module M with additive commutative monoid structure. The first Hom uses the canonical right-regular Rᵐᵒᵖ-action on coefficient R and the second its left-regular R-action. Scalar and source universes are independent; no right action on M, additive inverses or freeness is assumed. Evaluation, inverse and naturality laws accompany the equivalence. Over commutative semirings, two inverse inner-scalar restrictions compare it with Mathlib's Module.evalEquiv, preserving coefficient R and outer scalars R. For commutative semirings and finitely generated projective modules with additive commutative monoid structure, contraction gives a linear endomorphism trace without choosing a basis. Its rank-one evaluation, conjugation and dual-map invariance, cyclicity for maps between two finite projective modules and finite-free comparison with the finite-basis trace retain independent scalar and carrier universes. If the module is an additive commutative group, additivity and cyclicity give trace zero on additive commutators; no ring structure on the scalar semiring is required. For two finite projective additive-commutative-monoid modules, tensoring endomorphisms multiplies their traces, with independent scalar and factor universes. Both bilinear and pointwise forms are provided. Partial trace over a finite projective factor M contracts arbitrary linear maps M tensor N → M tensor P to maps N → P, linearly in the whole input. The untraced factors are arbitrary, with four independent universes. On a tensor product of maps a and b it is trace(a) times b, without normalization. On nonfree projectives the scalar trace need not be a natural multiple of the scalar unit. Product endomorphisms have the sum of their factor traces; diagonal inclusion-projection blocks have the factor traces and off-diagonal blocks have trace zero. An arbitrary block endomorphism of a product of finite projective factors has the sum of its diagonal traces. The off-diagonal formulas assume finite projectivity only of the product, without bases, additive inverses or coupled carrier universes. An arbitrary endomorphism of a finite dependent product of finite projective modules has the finite sum of the traces of its diagonal coordinate composites. The index need only be finite, with independent scalar, index and carrier universes. Over arbitrary rings, the library also describes stably-free kernels of surjections onto finitely generated stably-free targets, finite-coordinate kernel presentations and surjective right-linear matrix kernels. Rectangular right-coordinate maps need finite source coordinates but allow arbitrary target indices; transporting a supplied equivalence needs both indices finite. These constructions use left coefficients and right scalars, without commutativity, injectivity, IBN or equal index cardinalities. Finite projective categories over arbitrary rings are essentially small in the ring universe at independent carrier universes. Ring-universe representatives and linear equivalences give a common reference skeleton for comparing arbitrary input classes. Over a commutative semiring, an idempotent-generated ideal is free exactly for the zero and unit idempotents, without a nontriviality assumption. Right scalar-extension comparisons satisfy pointwise unit and triple-composition associativity laws over arbitrary rings and right modules, with five independent scalar and module universes. A unit semiconjugating two homomorphisms of arbitrary rings induces a fixed-right-target linear equivalence on their scalar extensions, with left multiplication by the unit and its inverse on tensor coefficients. Principal right ideals over arbitrary source and target rings have an image-one scalar-extension equivalence without idempotence, and an image-zero annihilation theorem with idempotence. An idempotent right ideal and its scalar extension are bundled as finite projectives over arbitrary rings, including noncentral matrix idempotents. The right-ideal bundle has an identity linear equivalence to its canonical principal ideal, identifying zero and scalar action. Canonical right regular modules on ordinary semiring carriers are finite and free, including zero semirings. A finite projective common stabilizer can be replaced by a common standard finite free one, without finiteness or projectivity assumptions on the ambient modules. Finite ranks are preserved by ring-universe representatives; finitely generated free categorical objects are classified by finite rank over rings satisfying the strong rank condition, not all finite projectives over arbitrary rings. Finite projective right-module classes form a ring-sized direct-sum monoid and additive Grothendieck group, with arbitrary-carrier generators, universal properties and common finite-projective or finite-free stabilization criteria over arbitrary rings. Over division rings, canonical natural-valued class and integer-valued group dimensions give additive equivalences with ℕ and ℤ, with finite-coordinate and all-integer regular-generator inverses. Scalar extension along arbitrary unital maps between division rings preserves both dimensions and induces bijective class and K₀ maps. For a division-ring source and any ring target, the whole induced maps are independent of the chosen scalar homomorphism. Subsingleton rings give trivial class monoids and groups, not division-ring dimension invariants. Every unital ring homomorphism induces additive scalar-extension maps on right-module classes and K₀, with arbitrary-carrier evaluation and entire-map identity and composition laws over noncommutative and zero rings. The free-word zero-generator augmentation returns the coefficient of the empty word, fixing constants and killing letter monomials. The full-letter linear combination has range equal to its canonical semilinear kernel, under the left regular word-semiring action. These results allow arbitrary, possibly noncommutative or trivial coefficient semirings and empty or infinite alphabets, with independent coefficient and alphabet universes. Over a commutative base ring R and an arbitrary target ring S, right scalar extension agrees with the module-first Mathlib tensor product, with the specified homomorphism-induced coefficient action and right multiplication on coefficients. For commutative S, a separate pointwise comparison lands in the right-module view of Mathlib's scalar-first extension. Pure-tensor, inverse and map-naturality laws retain independent scalar and carrier universes without finiteness or centrality hypotheses.

Quoted from the project description in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.

7 articles: 3 for highlights of its formalization.yaml whose declarations the scan finds and 4 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/projective-modules, read at commit 27f95a8b (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “agent-reviewed”.
  • Review notes: “Independent AI-agent review is reported. This metadata is not acceptance, build or axiom-check evidence and establishes neither source correspondence nor rights clearance. No human review, book-author endorsement or complete-book formalization is claimed.”
  • Automation: agent; framework “AI agents using Lean and Lake”; tool setup “Formal Frontier AI agents contributed Lean code and documentation using mathlib. Separately authored mathematics and expression adaptations are credited in docs/CREDITS.md.”; prompting notes “AI assistance focused on exact hypotheses, handedness, independent universes and reusable mathematical APIs.”
  • Automation notes: “Code and documentation include AI-agent contributions. AI generation alone establishes no originality, proof correctness or rights clearance.”

Literature

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

  • The K-book: An Introduction to Algebraic K-theory, Charles A. Weibel, Complete-book build dated 2013-08-29, Chapter I module and projective-module material, including Definition I.1.2 on finite stable coordinates, Example I.2.1.2 and the exterior-power Sum Formula on displayed pages 18-19 (physical PDF pages 26-27), and Chapter II group completion, projective-module K₀, stabilization and division-ring dimension (book; adapts).

Builds on

Used by

Highlights

TheoremSylvester's determinant identity for finite projective modules#

For finite projective modules P and Q over a commutative ring R and R-linear maps f : P → Q and g : Q → P, det(1 + g ∘ f) = det(1 + f ∘ g).

Quoted from the highlights in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.

Lean

Read from the source at commit 27f95a8b, without running Lean.

Sources
LeanModule.determinant_one_add_comp_comm

TheoremTensor-product determinants and rank powers#

For finite projective R-modules P and Q over a commutative ring R, det(f ⊗ g) = rankPower_Q(det(f)) · rankPower_P(det(g)) for all endomorphisms f of P and g of Q, and the rank-power map of P ⊗ Q is rankPower_P ∘ rankPower_Q.

Quoted from the highlights in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.

Lean

Read from the source at commit 27f95a8b, without running Lean.

Sources
LeanModule.determinant_tensorProduct_map · Module.rankPower_tensorProduct

TheoremProjective modules lift across nilpotent ideals#

For any ring R and nilpotent two-sided ideal I, every projective R/I-module is isomorphic to the canonical reduction of a projective R-module. Finitely generated inputs admit finitely generated lifts. Neither commutativity nor a finite-generation assumption on I is needed.

Quoted from the highlights in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.

Lean

Read from the source at commit 27f95a8b, without running Lean.

Sources
LeanModule.exists_projective_lift · Module.exists_finite_projective_lift

Headline results

The 51 headline results of its README are on a page of their own: 4 articles, 47 quoted as text.

Main results

Its formalization.yaml lists 210 main results, and the scan finds 210 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.