Skip to content

Coherence via kernels of maps… to Inverse images with nilpotent…

Highlights

TheoremCoherence via kernels of maps from finite free modules#

For any unital, possibly noncommutative ring R and any left R-module M, M is coherent (finitely generated with every finitely generated submodule finitely presented) if and only if M is finitely generated and the kernel of every R-linear map Rⁿ → M is finitely generated for every natural number n, including zero.

Quoted from the highlights in formalization.yaml of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanModule.IsCoherent.iff_finite_and_fg_ker

TheoremFiniteness, projectivity and flatness under injective tensor units#

Let R be a commutative ring, S an R-algebra and M an additive commutative monoid with its given R-module structure. Assume the canonical unit N → S ⊗[R] N is injective for every additive commutative R-semimodule N in Type (max uR uM). For a possibly noncommutative semiring S, S ⊗[R] M is finitely generated over S if and only if M is finitely generated over R. For a possibly noncommutative ring S, the corresponding finite-presentation equivalence holds. If S ⊗[R] M is finite and projective over any possibly noncommutative semiring S, M is finite and projective over R; finite presentation of M is derived internally. For a commutative ring S, flatness is likewise equivalent. All three carrier universes are independent; S need not be flat over R, and M needs neither an S-action nor a supplied additive group structure.

Quoted from the highlights in formalization.yaml of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanModule.Finite.iff_finite_tensorProduct_of_injective · Module.FinitePresentation.iff_finitePresentation_tensorProduct_of_injective · Module.finite_projective_of_tensorProduct_of_injective · Module.Flat.of_flat_tensorProduct_of_injective · Module.Flat.iff_flat_tensorProduct_of_injective

TheoremInternal Krull–Schmidt decompositions and cancellation#

Over any possibly noncommutative ring, a Noetherian module or an Artinian module is a finite internal direct sum of nonzero indecomposable submodules, with an explicit A i ≠ ⊥ fact paired with each summand's categorical indecomposability. Two supplied finite internal decompositions of linearly equivalent modules have matching summands up to linear equivalence when all summands have local endomorphism rings. Indecomposable summands and finite length of one total suffice instead. Both matching conclusions include explicit nonzero facts for each supplied family. Arbitrary finite index types use the caller's decidable equality instances and may be empty; existence uses stock equality on Fin n. Matching is existential; no preservation of the given coordinates or canonical choice is asserted. A common finite-length module P, possibly zero, cancels from P × M ≃ₗ[R] P × N with no chain condition on M or N. Zero modules, including those over a zero ring, have the empty decomposition.

Quoted from the highlights in formalization.yaml of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanSubmodule.exists_fin_isInternal_indecomposable_of_isNoetherian · Submodule.exists_fin_isInternal_indecomposable_of_isArtinian · DirectSum.IsInternal.exists_equiv_of_linearEquiv_of_isLocalRing_end · DirectSum.IsInternal.exists_equiv_of_linearEquiv_of_indecomposable_of_isFiniteLength · LinearEquiv.nonempty_of_prod_of_isFiniteLength

TheoremCoherence of square-zero extensions and finite-support idealizations#

For a division ring D and a bimodule M in independent universes, the trivial square-zero extension D ⋉ M is left coherent if and only if M is finitely generated on the left. Both compatible module actions are retained, without centrality. For the stock pointwise left module ι →₀ D and any compatible right action, this is equivalent to finiteness of ι, including the empty index type. For a field k and infinite ι, the canonical inclusion algebra k → TrivSqZeroExt k (ι →₀ k), a ↦ (a, 0), is faithfully flat but not coherent. The canonical field criterion allows the zero coefficient space; finite generation means finite dimension, not a finite underlying set. More generally, for a possibly noncommutative ring R and a bimodule M with its given commuting left and right actions, left coherence of R ⋉ M implies finite generation of M on the left whenever r ↦ r • v is injective for one vector v. Sufficiency holds for a left coherent base and a coefficient bimodule finitely presented on the left.

Quoted from the highlights in formalization.yaml of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanTrivSqZeroExt.isCoherentRing_iff_finite_of_divisionRing · TrivSqZeroExt.isCoherentRing_finsupp_iff_finite · TrivSqZeroExt.finsupp_faithfullyFlat_and_not_isCoherentRing · TrivSqZeroExt.finite_of_isCoherentRing_of_injective_smul · TrivSqZeroExt.isCoherentRing_iff_finite · TrivSqZeroExt.isCoherentRing

Headline results

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Spans, kernels and coordinate faces. For a linear map of semimodules over any possibly noncommutative semiring, if its target has no nonzero additive summands of zero and has no zero scalar divisors, then span R S ⊓ ker f = span R (S ∩ ↑(ker f)) for every set S. Intersecting a finitely generated submodule with this kernel remains finitely generated. The image-only corollaries require these two properties only on range f, without changing the kernel. For an arbitrary coefficient module A with those properties and arbitrary index and support sets, the coordinate-face formulas give the same conclusions for Finsupp.supported A R J, using the given R-action. The polynomial example exhibits a nonzero proper face of a two-generated semimodule over ℕ[X]. If R is zero-sum-free and has no zero divisors, every uniformly degree-bounded coefficient face of a finitely generated submodule of I →₀ R[X] is finitely generated over R. The allowed coefficient positions may correlate the index and degree; neither I nor the allowed set needs to be finite. The whole polynomial submodule need not be finitely generated over R, and R need not be commutative.

Polynomial intertwining. For an arbitrary semiring S, additive commutative monoids M, N, and coefficient representations σ : S →+* AddMonoid.End M, τ : S →+* AddMonoid.End N, an additive map h : M →+ N that intertwines every σ s with τ s and the selected endomorphisms f with g also intertwines their plain polynomial evaluations. The semilinear version uses the given module structures over independent semirings R, R₂, any scalar homomorphism η : R →+* R₂, an η-semilinear map h, and representations into the respective linear endomorphism semirings. The hypotheses (τ s).comp h = h.comp (σ s) for every s and g.comp h = h.comp f imply (p.eval₂ τ g).comp h = h.comp (p.eval₂ σ f). All five carrier universes are independent. No coefficient/end commutation, finiteness, or module structure on the semilinear Hom is required.

Stable kernels and ranges. For an additive commutative group with its given module structure over a possibly zero, noncommutative semiring, simultaneous one-step stability at a natural bound, including zero, gives the specified sum equivalence from the power kernel and range. The kernel restriction is nilpotent and the range restriction is an automorphism. Canonical projections are independent of the stable bound and natural for arbitrary linear intertwiners. Noetherianity and Artinianity of the module give a common bound; the separate Noetherian-surjective and Artinian-injective automorphism criteria retain their asymmetric hypotheses. See StableKernelRange. Over arbitrary ring scalars, a finite-length module that is categorically indecomposable has a local endomorphism ring, and each endomorphism is nilpotent or a unit. The indecomposable predicate already excludes the zero module; see Local. The classical ring-module antecedents are Fitting's lemma and its indecomposable finite-length local-endomorphism consequence, as presented in Wisbauer, Foundations of Module and Ring Theory, §§31.13 and 32.4(3)(iii). The explicit-one-step semiring/additive-group decomposition above generalizes the cited ring-module setting; the local-endomorphism theorem retains ring scalars. See references and credit.

Internal Krull–Schmidt decompositions and cancellation. Over any ring, a Noetherian module or an Artinian module is a finite internal direct sum of nonzero indecomposable submodules; the two chain conditions are separate existence hypotheses. Each existence witness includes A i ≠ ⊥ alongside categorical indecomposability. Two supplied finite internal decompositions of linearly equivalent modules match up to an equivalence of index types and linear equivalences of summands when all summands have local endomorphism rings. Indecomposable summands and finite length of one total give the same matching. Both matching conclusions include ∀ i, A i ≠ ⊥ and ∀ j, B j ≠ ⊥, derived from the given hypotheses. Arbitrary finite index types use the caller's decidable equality instances and may be empty; existence uses the stock equality instance on Fin n. The matching is existential, not required to preserve the given coordinates. A common finite-length module P cancels from P × M ≃ₗ[R] P × N, with no chain condition on M or N; P may be zero. Zero modules, including those over a zero ring, have the empty decomposition. See KrullSchmidt, which realizes the categorical theorems of Homological Algebra through ModuleCat.

TheoremAdditive intertwining by ranges#

An additive map between commutative monoids intertwines a finite family of source endomorphisms summing to the identity with an orthogonal idempotent target family if and only if it maps each source range into its corresponding target range. No source orthogonality, target completeness, subtraction or cancellation is required, and the monoid and index universes are independent. The arbitrary-index range-action lemma also supplies the coordinate calculation for the existing linear product-of-ranges equivalence through Mathlib's canonical endomorphism action. See OrthogonalIdempotents.semiconj_iff_mapsTo_range and linearEquivPiRange.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanOrthogonalIdempotents.semiconj_iff_mapsTo_range

TheoremFibrewise additive intertwining#

For additive commutative monoids M, N, let P : I → AddMonoid.End M have finite index set and sum to the identity, and let Q : J → AddMonoid.End N be an orthogonal idempotent family, with decidable equality on J. For any q : I → J and additive h : M →+ N, sending range (P i) into range (Q (q i)) for every i implies h ∘ (∑ i with q i = j, P i) = Q j ∘ h for every j. This implication uses no source orthogonality; it is an equivalence when P is a complete orthogonal idempotent family. The target label set may be infinite, and Q need not be complete; labels may be merged or omitted. An unused Q j need only kill h(M), not vanish on all of N. No subtraction, cancellation or scalar compatibility is required, and the two monoid and two index universes are independent. See OrthogonalIdempotents.semiconj_sum_fiberwise_of_mapsTo_range and CompleteOrthogonalIdempotents.semiconj_sum_fiberwise_iff_mapsTo_range.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanOrthogonalIdempotents.semiconj_sum_fiberwise_of_mapsTo_range

TheoremFinite coarsening of complete orthogonal idempotents#

Over any possibly noncommutative Semiring A, summing a finite complete orthogonal family over the fibres of an arbitrary map q : I → J gives a complete orthogonal family indexed by J. Both index types have Fintype instances, with decidable equality needed only on J; the three universes are independent. The map need not be surjective: unused labels have value zero. Empty index types and zero semirings are allowed; no additive inverses, cancellation or centrality is required. See CompleteOrthogonalIdempotents.sum_fiberwise.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanCompleteOrthogonalIdempotents.sum_fiberwise

DefinitionDual endomorphisms#

Over a commutative semiring R, Module.End.dualMapAlgHom bundles dualization as an algebra homomorphism from the opposite endomorphism algebra of any R-semimodule. For a possibly noncommutative R-algebra A, Module.Dual.rightRegularAlgHom gives named operators F_a(φ)(x) = φ(a * x), with F_a.comp F_b = F_(b * a) and the original pointwise R-scalar structure on the dual. No finiteness or freeness is required. Over a commutative ring R and a possibly noncommutative ring algebra A, Module.Dual.coextensionEquiv identifies opposite-algebra coextension of R, restricted to R, with the original dual, intertwining coextension translation with these named operators. Its generic pointwise Hom comparison retains the given algebra action and allows independent scalar and module universes. For self-pairings, LinearMap.nondegenerate_of_surjective_of_separatingLeft proves both separating directions from surjectivity and left separation; a bijective map to the dual is consequently nondegenerate, even for semimodules.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanModule.End.dualMapAlgHom

TheoremTensor–dual Frobenius criterion#

For a finite-dimensional, possibly noncommutative or zero algebra A over a field K, Module.Dual.exists_nondegenerate_mul_of_tensorProduct_equiv produces a functional λ with both-sided nondegenerate pairing λ(a * x) from a subspace C of the original dual and an equivalence e : C ⊗[K] A ≃ₗ[K] Module.Dual K A satisfying e (c ⊗ₜ a) x = c (a * x). The algebra needs only Semiring A; finiteness of C is derived, and the scalar and algebra universes are independent.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanModule.Dual.exists_nondegenerate_mul_of_tensorProduct_equiv

TheoremAnnihilator quotients with two scalar actions#

Suppose a ring A and a semiring C act on the same additive commutative monoid M, with commuting given actions. If M is finitely generated over C and Noetherian over A, then A modulo the annihilator of its original action is left Noetherian; see isNoetherianRing_quotient_annihilator_of_finite. If M is an additive commutative group, finite generation over C and coherence over A instead give a coherent annihilator quotient, as a regular left module over the quotient ring; see isCoherentRing_quotient_annihilator_of_finite. The three universes are independent. Neither scalar type needs to be Noetherian, and the A-action need not commute with itself. Taking C = A in the Noetherian result recovers the self-commuting criterion: for an additive commutative group with a self-commuting A-action, Noetherianity over A is equivalent to finite generation over A and left Noetherianity of the annihilator quotient. In particular, this applies over every commutative ring. The sufficient direction holds over any ring for an additive commutative monoid with its given module structure, without a commutation hypothesis.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanisNoetherianRing_quotient_annihilator_of_finite

TheoremNoetherian semilinear Hom#

For semirings R, R₂, a ring S, a finitely generated R-semimodule M, and a Noetherian S-module N with a commuting R₂-action, isNoetherian_semilinearMap makes M →ₛₗ[σ] N Noetherian for the canonical pointwise S-action, for every σ : R →+* R₂. The five universes are independent; no surjectivity of σ, scalar commutativity or ambient Noetherianity is required. isNoetherian_linearMap_of_finite gives the plain-linear specialization and recovers Mathlib's isNoetherian_linearMap proposition in its commutative-ring case, with the same pointwise action.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanisNoetherian_semilinearMap

DefinitionHom and End of matrix columns#

Over an arbitrary possibly noncommutative semiring R, finite-sum matrix actions retain the given coefficient-module structures. For a finite nonempty index I, LinearMap.matrixModuleHomAddEquiv identifies coefficient-linear maps additively with matrix-linear maps of columns; its inverse is characterized at every coordinate. Module.matrixModuleEndRingEquiv preserves the usual order of composition. For the regular coefficient module this gives Rᵐᵒᵖ, not the full matrix semiring. With empty I, coordinate extension is still surjective, but need not be injective. Zero semirings are allowed, and no scalar-module structure on a general Hom is used.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanLinearMap.matrixModuleHomAddEquiv

TheoremProjective matrix-column semimodules#

For a semiring R, an additive commutative monoid M with its given R-module structure, and a finite type I with decidable equality, Matrix.Module.projective_iff characterizes projectivity of the canonical Matrix I I R-module on I → M by IsEmpty I ∨ Module.Projective R M. In particular, for inhabited I, projectivity is equivalent to that of M over R. No coefficient commutativity or additive inverses are required, and the carrier universes are independent.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanMatrix.Module.projective_iff

DefinitionLeft ideals of finite matrix semirings#

For [Semiring R], [Fintype I] and [DecidableEq I], including empty I, Submodule.matrixRowsOrderIso identifies left ideals of Matrix I I R with R-submodules of the row module I → R. Left Artinianity and left Noetherianity of the matrix semiring are equivalent to the corresponding conditions on this row module, not to unrestricted conditions on the coefficient semiring.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanSubmodule.matrixRowsOrderIso

InstanceCoherence of finite matrix rings#

For an arbitrary, possibly noncommutative or zero Ring R, a finite type I with its given decidable equality, and the canonical regular left modules, Matrix.instIsCoherentRing gives coherence of Matrix I I R from coherence of R, including empty I. For nonempty I, IsCoherentRing.of_matrix reflects coherence and Matrix.isCoherentRing_iff gives the equivalence. The ring and index universes are independent. The supporting Matrix.entrywiseLinearMap applies a coefficient-linear map (κ → R) →ₗ[R] R entrywise to a family of matrices, linearly for regular left matrix multiplication, over any semiring and arbitrary family index κ. Its scalar-restricted kernel has a split entry projection onto the coefficient kernel. Reflection needs nonempty I: the empty matrix ring has one element and is coherent for every R. More generally, for any additive commutative monoid M with its given R-module structure, Matrix.Module.instIsCoherent preserves coherence under the canonical finite-sum action of Matrix I I R on I → M, including empty I. For nonempty I, Module.IsCoherent.of_matrixModule reflects coherence and Matrix.Module.isCoherent_iff gives the equivalence with Module.IsCoherent R M. No coherence of R, Noetherianity, or extra finite-generation premise is required. The index, coefficient and module universes are independent, and R may be zero. With empty I, every column module is a subsingleton and hence coherent, so nonemptiness is essential for reflection.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanMatrix.instIsCoherentRing

TheoremLeft-regular elements in left Artinian rings#

For an arbitrary unital Ring A with [IsArtinianRing A], IsLeftRegular.isUnit_of_isArtinianRing makes every left-regular element a unit. Artinianity concerns the original left regular module; no opposite-Artinian, commutativity or nontriviality hypothesis is required, and the carrier universe is arbitrary. The reverse implication is already available through Mathlib's IsUnit.isRegular.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanIsLeftRegular.isUnit_of_isArtinianRing

DefinitionClosed semimodule categories#

For a CommSemiring R, SemimoduleCat.tensorLeftHomAdjunction makes tensoring with M left adjoint to its wrapped-morphism Hom functor. The Hom functor allows an independent carrier universe; the monoidal closed structure uses the common scalar and carrier universe of the tensor category. Currying, uncurrying, evaluation and coevaluation have pure-tensor formulas. Over a commutative ring, ModuleCat.ihomSemimoduleIso compares the chosen internal Homs and their unit, counit and precomposition maps. The finite-basis client uses a specified basis with finite index type to show that tensoring preserves existing limits at two independent diagram sizes; the index universe is independent as well.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanSemimoduleCat.tensorLeftHomAdjunction

DefinitionKernels over semirings#

For an arbitrary Semiring R, SemimoduleCat.kernelIsLimit makes the existing kernel submodule, with its subtype inclusion, a categorical kernel. SemimoduleCat.hasKernels_semimoduleCat gives kernels in SemimoduleCat.{v} R, with independent coefficient and carrier universes. Over a ring, ModuleCat.kernelCone_semimodule_hom_apply shows that the comparison with Mathlib's module kernel preserves underlying elements.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanSemimoduleCat.kernelIsLimit

TheoremSums of nilpotent left ideals#

For arbitrary left ideals I, J of a possibly noncommutative Semiring R, Ideal.sup_pow_add_sub_one_le gives (I ⊔ J) ^ (m + n - 1) ≤ I ^ m * ⊤ ⊔ J ^ n * ⊤ for all natural m, n. Global witnesses I ^ m = 0 and J ^ n = 0 therefore give (I ⊔ J) ^ (m + n - 1) = 0; Ideal.isNilpotent_sup makes the sum of two globally nilpotent left ideals nilpotent. No commutativity, two-sidedness or positivity of the exponents is required. The relative-generation client combines this with nilpotent-ideal elimination to deduce P ≤ N from P ≤ N ⊔ (I ⊔ J) • P in any additive commutative R-semimodule, with an independent carrier universe.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanIdeal.sup_pow_add_sub_one_le

TheoremInverse images with nilpotent kernel#

For a unital semiring homomorphism f and a target left ideal J, Ideal.pow_comap_eq_zero_of_ker_pow_eq_zero gives J.comap f ^ (m * n) = 0 from the global witnesses J ^ m = 0 and (RingHom.ker f) ^ n = 0. The companion Ideal.isNilpotent_comap gives global nilpotence of the inverse image. Both semirings may be noncommutative, all natural exponents including zero are allowed, and the source, target and generic RingHomClass homomorphism family have independent universes. The same module gives product and power inclusions for inverse images without nilpotence hypotheses.

Quoted from the headline results in README.md of FormalFrontier/coherent-modules at commit b670b34e, Apache-2.0.

Lean

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

Sources
LeanIdeal.pow_comap_eq_zero_of_ker_pow_eq_zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.