Coherent modules
Coherent rings and modules, finite-presentation criteria, exact-sequence closure, localization and descent, coherent-module categories, universal coherence, Hom and tensor-product closure, finite square-zero kernels and projection base change, coherence criteria for idealizations over division rings, finite-support idealizations and faithfully flat noncoherent algebras over fields, finite-type ideal/module transfer, left Noetherianity under scalar clearing, pointwise unimodular finite-generation ascent for semilinear maps, generator bounds for semilinear images, Artin–Rees for Noetherian modules, finite-submodule adic cofinality, radical colons of arbitrary subsets, and localization saturation commuting with colons by finitely generated ideals, annihilator localization for finitely generated semimodules, relative generation by nilpotent ideals, and finite-generation, finite-presentation, finite-projectivity and flatness descent under injective tensor units, internal Krull–Schmidt decompositions and finite-length cancellation in Lean.
Quoted from the project description in formalization.yaml of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.
76 articles: 4 for highlights of its formalization.yaml whose declarations the scan finds and 72 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/coherent-modules, read at commit b670b34e (2026-11-05).
- Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
- License: Apache-2.0.
- Authors: Formal Frontier Agents.
- Review status: “other: revision-specific independent AI-agent review”.
- Review notes: “Review and acceptance are recorded for exact revisions in the project's maintained release records. Changes require independent review and applicable build, proof-integrity, rights and provenance evidence before acceptance; this field does not certify any arbitrary checkout or replace that evidence. AI-agent review is not human peer review, legal certification, source-author endorsement or complete source formalization.”
- Automation: agent; tool setup “Formal Frontier AI agents using Lean, Lake and Git for development, assembly, review and maintenance.”
- Automation notes: “Original project contributions and upstream/tooling provenance are summarized in docs/CREDITS.md. Review and verification apply to exact revisions; AI-agent participation does not imply human peer review or source-author endorsement.”
Literature
The sources its formalization.yaml names, with their relationship to it.
- Coherent rings, coherent modules and finite presentation (folklore; independently-proves).
- Semilinear Noetherian ascent under scalar clearing (folklore; independently-proves).
- Foundations of Rigid Geometry I, Kazuhiro Fujiwara, Fumiharu Kato (book; background).
Builds on
- Homological algebra (a Lake dependency, pinned at 6c7f755c)
Used by
- Adic modules
- Algebraic groups
- Formal power series
- Graded rings
- Group rings
- Minimal primes
- Multivariate polynomials
- Projective modules
- Scheme properties
- Toric ideals
- Valuation integers
- Vector bundles
Coherence via kernels of maps… to Inverse images with nilpotent…
- Coherence via kernels of maps from finite free modules
- Finiteness, projectivity and flatness under injective tensor units
- Internal Krull–Schmidt decompositions and cancellation
- Coherence of square-zero extensions and finite-support idealizations
- Additive intertwining by ranges
- Fibrewise additive intertwining
- Finite coarsening of complete orthogonal idempotents
- Dual endomorphisms
- Tensor–dual Frobenius criterion
- Annihilator quotients with two scalar actions
- Noetherian semilinear Hom
- Hom and End of matrix columns
- Projective matrix-column semimodules
- Left ideals of finite matrix semirings
- Coherence of finite matrix rings
- Left-regular elements in left Artinian rings
- Closed semimodule categories
- Kernels over semirings
- Sums of nilpotent left ideals
- Inverse images with nilpotent kernel
Relative generation by… to Finite generation from the…
- Relative generation by nilpotent ideals
- Extension of products and powers of left ideals
- Annihilators after localization
- Coatomicity of two-sided ideals
- Radical colons and pointwise annihilators
- Finitely generated ideal colons and localization
- Unit-ideal scalar families
- Coprime scalar rows
- Finite coprime-kernel decompositions
- Finite generation under pointwise unimodular clearing
- Semilinear Noetherian ascent
- Artin–Rees for Noetherian modules
- Submodule adic cofinality
- Power-killed submodule criteria
- Descent of adic cofinality
- Adic cofinality on finite products
- Cofinal ideal powers
- Semilinear transport of adic cofinality
- Krull intersection from adic cofinality
- Finite generation from the first adic quotient
Finite presentation from… to Faithfully flat tensor products
- Finite presentation from cofinal ideal quotients
- Essentially finite-type scalar extension
- Coherent modules and kernels
- Coherent homology
- Coherence along semilinear retractions
- Coherent dependent direct sums
- Coherence over product coefficient rings
- Finite presentation over product coefficient rings
- Finite presentation along scalar towers
- Coherence along quotient coefficients
- Coherence under scalar restriction
- Hom, tensor, and categories
- Coherent right duals
- Finite-module tensor zero detection
- Ideal action on finite coefficients
- Semilinear invariance of flatness
- Finiteness, projectivity and flatness under pure scalar extension
- Annihilators under finite-limit-preserving scalar extension
- Annihilator contraction under faithfully flat extension
- Faithfully flat tensor products
Faithfully flat dependent… to Finite-type ideal/module…
- Faithfully flat dependent direct sums
- Finitely generated ideals and dependent products
- Faithful flatness after base change covering maximal ideals
- Faithful flatness of unital algebras
- Faithfully flat products of algebras
- Products of localizations at submonoids
- Families of principal localizations
- Faithfully flat coherence descent
- Universal coherence
- Associative square-zero multiplication
- Commutativity of square-zero extensions
- Square-zero kernels and projection base change
- Full left-ideal lattice of square-zero extensions
- Module length and square-zero extensions
- Coherent square-zero extensions
- Opposites of square-zero extensions
- Left Noetherian square-zero extensions
- Finite-type ideal/module transfer
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.