Category theory; homological algebra

The Lean Pool projects whose card's first MSC2020 code is in class 18, “Category theory; homological algebra”: 3 articles, one per card.

Lemmacircuitlib: a circuit verification library for Lean 4#

A categorical semantics framework for digital circuits over Belnap's four-valued logic, following Ghica-Kaye-Sprunger. Its main theorems prove that combinational circuits (monotone functions on wire vectors) and sequential circuits (causal monotone stream functions) form symmetric monoidal categories, with a verified full adder as demonstration.

Quoted from the card LeanPool/projects/circuitlib.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Circuit.SequentialCircuitCategory.instSymmetricCategory, a main declaration that the scan does not find declared in the project's files at this commit: “The category of sequential circuits, whose morphisms are causal monotone stream functions as in Ghica-Kaye-Sprunger's denotational semantics, is symmetric monoidal, with all coherence laws (pentagon, triangle, hexagons, symmetry) proven.”
  • Circuit.CombinationalCircuitCategory.instSymmetricCategory, which the scan does not find declared in the project's files at this commit: “The category of combinational circuits, with wire counts as objects and monotone wire-vector functions as morphisms, is symmetric monoidal under juxtaposition of wire bundles.”
  • Circuit.SequentialCircuitCategory.tensorHom_causal (lemma), declared in LeanPool/Circuitlib/Circuit/Category/Sequential.lean, line 205: “Causality is preserved by parallel composition, the key lemma making sequential circuits closed under the tensor product.”
  • Circuit.BelnapLevel.instSemilatticeSup, which the scan does not find declared in the project's files at this commit: “Belnap's four truth values under the information order form a join-semilattice, the wire-value semantics in which every circuit denotes a monotone function.”
  • Circuit.CombinationalCircuit.adder_def (lemma), declared in LeanPool/Circuitlib/Circuit/Combinational.lean, line 115: “Correctness of a full adder assembled categorically from two half adders, gates, braidings, and whiskerings, computing the Boolean sum and carry bits; a demonstration of the framework.”
Project
Sources

TheoremDilatations of categories and commutative rings#

Constructs categorical dilatations from sieves of permitted numerators and denominator morphisms, and proves their universal property for Sigma-regular functors satisfying the sieve containment condition. Develops restriction and union of centers, dual codilatations, and ordinary localization as a special case. The composition isomorphism retains the explicit Sigma-regularity hypothesis left open in the original paper. For commutative rings, an exponent-profile center recovers the ring dilatation; the naive single-index comparison is refuted over Z[X]. A finite category example refutes a general intermediate-category characterization. Independent ring modules provide fraction arithmetic, a universal property, reindexing, and the unique isomorphism for two-stage dilatations.

Quoted from the card LeanPool/projects/dilatations.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • CategoryTheory.Dilatations.Dila_universal_property (theorem; a main declaration), declared in LeanPool/Dilatations/Basic.lean, line 1286: “For a nonempty indexed center in a category C and a functor F from C to D, assume that localization of D at the images of the chosen denominators is faithful and that each pushed-forward numerator sieve lies in the sieve generated by its mapped denominator. There is a unique functor from the dilatation to D whose composite with the canonical functor from C is F.” Its source, as the card gives it: “Section 5; original Theorem 3.10.”
  • CategoryTheory.Dilatations.Iso315 (def), declared in LeanPool/Dilatations/Centers.lean, line 863: “The successive dilatation at Z and the pushforward of W is isomorphic to the dilatation at the combined center Z.sum W, assuming that the composite canonical functor to the successive dilatation is Sigma-regular for Z.sum W. This regularity is an explicit hypothesis, not a theorem of the development.” Its source, as the card gives it: “Section 8.2 and Appendix B; conditional original Proposition 3.15.”
  • CategoryTheory.Dilatations.Iso318 (def), declared in LeanPool/Dilatations/Centers.lean, line 1061: “For two families of numerator sieves with the same denominator morphisms, dilating at their combined two-copy center is isomorphic to dilating at the pointwise union of the sieves.” Its source, as the card gives it: “Section 8.3; original Proposition 3.18.”
  • CategoryTheory.Dilatations.Prop51.Iso51 (def), declared in LeanPool/Dilatations/RingComparison.lean, line 625: “For any multicenter in a commutative ring A, the categorical dilatation of the multiplicative one-object category of A at all finitely supported exponent profiles is isomorphic to the one-object category of the ring dilatation A[M]. At profile nu, the denominator is the product of a_i raised to nu_i and the numerator ideal is the product of (M_i + (a_i)) raised to nu_i.” Its source, as the card gives it: “Theorem 10.1; corrected original Proposition 5.1.”
  • CategoryTheory.Dilatations.NaiveCenterCounterexample.no_C_compatible_equiv (theorem), declared in LeanPool/Dilatations/NaiveCenterCounterexample.lean, line 497: “For A = Z[X], ideal (X), and denominator 2, there is no equivalence from the categorical dilatation at the naive one-index center to the one-object category of the ring dilatation that commutes strictly with the canonical functors from the base category.” Its source, as the card gives it: “Section 10.2 and Appendix B.”
  • CategoryTheory.Dilatations.Fact52.no_realizing_center (theorem), declared in LeanPool/Dilatations/CategoryCounterexample.lean, line 465: “The constructed category with three arrows from X to Y admits no equivalence to a dilatation of the base category with two such arrows that commutes strictly with the canonical base functors. This is an explicit counterexample, not a classification of intermediate categories up to arbitrary equivalence.” Its source, as the card gives it: “Theorem 11.1.”
  • CategoryTheory.Dilatations.iteratedDilatationEquiv_existsUnique (theorem), declared in LeanPool/Dilatations/IteratedRings.lean, line 276: “For a multicenter M in any commutative ring A and any subset K of its indices, first dilate along K and then along the complementary ideals and denominators mapped to the first-stage ring. There is exactly one isomorphism of algebras over the first-stage ring from this two-stage dilatation to A[M], compatible with its canonical map.” Its source, as the card gives it: “Appendix C, Proposition C.1 and Lemma C.2.”
Project
  • Authors: Arnaud Mayeux, Jujian Zhang.
  • Source: Dilatations of categories, via their Lean formalization by Arnaud Mayeux, arXiv:2608.09305.
  • Project repository: rndmx/DilCat, at commit 60455965.
  • Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs. The card's note: “Mayeux's paper discloses Claude assistance under the author's direction; it does not quantify the share of generated proofs. The development incorporates Mayeux and Zhang's earlier ring formalization. This port includes substantial AI proof repair, optimization, and documentation.”
  • License: Apache-2.0.
  • MSC2020: 18A30, 13B30.
  • In Lean Pool: LeanPool/Dilatations, from the card LeanPool/projects/dilatations.yaml.
Sources
LeanCategoryTheory.Dilatations.Dila_universal_property

DefinitionFactorization Systems#

Formalizes factorization systems, orthogonality, orthogonal complements, and the standard construction from weak factorization plus orthogonality.

Quoted from the card LeanPool/projects/factorizationsystems.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanCategoryTheory.FactorizationSystemCharacterization

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.