Relative generation by… to Finite generation from the…

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

TheoremRelative generation by nilpotent ideals#

For a left ideal I of a possibly noncommutative semiring R and submodules N, P of an additive commutative R-semimodule, Submodule.le_sup_pow_smul_of_le_sup_smul propagates P ≤ N ⊔ I • P to P ≤ N ⊔ (I ^ n) • P for every natural n. Under global nilpotence IsNilpotent I, the companion Submodule.le_of_le_sup_smul_of_isNilpotent gives P ≤ N. The carrier universes are independent, and no finite generation, additive inverses, cancellation or nontriviality is required.

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.le_sup_pow_smul_of_le_sup_smul

TheoremExtension of products and powers of left ideals#

For any unital homomorphism f : A →+* B between semirings in independent universes, Ideal.map_mul_of_isTwoSided gives (I * J).map f = I.map f * J.map f whenever I.map f is two-sided. The companion Ideal.map_pow_of_isTwoSided gives (I ^ n).map f = (I.map f) ^ n for every natural exponent, including zero. Neither semiring must be commutative, and f need not be surjective.

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.map_mul_of_isTwoSided

TheoremAnnihilators after localization#

For commutative semirings R, A, a submonoid T : Submonoid R, an R-algebra A realizing localization at T, and a standard localized-module map f : M →ₗ[R] N, IsLocalizedModule.map_annihilator gives 

Ideal.map (algebraMap R A) (Module.annihilator R M) =
  Module.annihilator A N
when M is finitely generated over R. The semimodules are additive commutative monoids, N has its compatible A-action, and all four carrier universes are independent. Zero semirings, zero modules and 0 ∈ T are allowed; no finite presentation, flatness or faithful-action assumption is added. The supporting IsLocalizedModule.comp_eq_iff_exists_smul_eq characterizes equality after localization for two maps from a finitely generated semimodule by a single submonoid multiplier making them equal.

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
LeanIsLocalizedModule.map_annihilator

TheoremCoatomicity of two-sided ideals#

For any unital, possibly nonassociative ring R, TwoSidedIdeal.isCoatomic proves IsCoatomic (TwoSidedIdeal R): every proper two-sided ideal lies below a maximal proper two-sided ideal. No nontriviality, commutativity or finiteness assumption is needed. Use this theorem as a local instance with Mathlib's coatom consumers. The simple-quotient example combines it with the congruence correspondence to obtain a nontrivial simple quotient of an arbitrary nontrivial ring, with its surjective unital quotient map.

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
LeanTwoSidedIdeal.isCoatomic

TheoremRadical colons and pointwise annihilators#

For a radical ideal I in a commutative semiring R and an arbitrary subset s : Set R, Ideal.IsRadical.colon proves (I.colon s).IsRadical; use it as hI.colon s. Taking I = ⊥ in a reduced commutative semiring shows that the ideal of scalars a with a * b = 0 for every b ∈ s is radical. No finiteness, nonemptiness or nontriviality assumption is needed.

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.IsRadical.colon

TheoremFinitely generated ideal colons and localization#

For commutative semirings R, S, a submonoid T : Submonoid R and an R-algebra S satisfying [IsLocalization T S], IsLocalization.comap_map_colon gives 

Ideal.comap (algebraMap R S)
    ((I.colon (J : Set R)).map (algebraMap R S)) =
  (Ideal.comap (algebraMap R S) (I.map (algebraMap R S))).colon (J : Set R)
for any ideal I and finitely generated ideal J, with Submodule.FG (J : Submodule R R). Thus multiplicative saturation, expressed by extension followed by contraction, commutes with colon by J. Finite generation concerns the ideal, not its underlying set. The two universes are independent; zero semirings, 0 ∈ T, J = ⊥ and top ideals are allowed. No finiteness or radicality of I is required.

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
LeanIsLocalization.comap_map_colon

TheoremUnit-ideal scalar families#

For an arbitrary family of scalars generating the unit ideal in a semiring S, Ideal.existsUnique_smul_eq_of_span_range_eq_top gives a unique common parameter for compatible elements of an S-semimodule whose scalar actions commute. The index type need not be finite or nonempty, and no subtraction or additive cancellation is needed.

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.existsUnique_smul_eq_of_span_range_eq_top

TheoremCoprime scalar rows#

For a commutative semiring S, an additive commutative S-semimodule M, and Bézout-coprime scalars a, b, IsCoprime.existsUnique_smul_eq_pair gives a unique k with a • k = x and b • k = y whenever b • x = a • y. The companion smul_mem_range_smul_iff reflects membership in the range of multiplication by a after multiplying by b. The two universes are independent; no subtraction, additive cancellation, nontriviality or finiteness is assumed.

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
LeanIsCoprime.existsUnique_smul_eq_pair

DefinitionFinite coprime-kernel decompositions#

Let a commutative semiring A act through a representation τ : A →+* Module.End R M, where R is any semiring and M is an additive commutative R-semimodule. For a finite labelled pairwise Bézout-coprime family a, the sole annihilation premise τ (∏ i, a i) = 0 gives RingHom.linearEquivPiKer, an explicit equivalence with the product of the labelled kernels. Its inverse sums the kernel inclusions, and its projectors are independent of the whole Bézout partition used to compute them. Empty families, zero semirings and noncommutative scalar semirings are allowed; no subtraction or additive cancellation is needed. Polynomial evaluation and scalar torsion decompositions are specializations. Given a second such decomposition from υ : B →+* Module.End T N and a finite family b : J → B, an arbitrary map q : I → J regroups the fine labels. An additive map h : M →+ N intertwining each represented fibre-product τ (∏ i with q i = j, a i) with υ (b j) intertwines the corresponding sum of fine canonical projectors with the target projector; each target coordinate is the fibre-sum of mapped fine coordinates. Empty fibres are allowed. The coefficient and scalar semirings may differ; neither scalar-linearity nor compatibility with other represented elements is required. Same-label naturality is the specialization q = id. The exact projector criterion is RingHom.semiconj_sum_kerProjector_iff_mapsTo_ker: h intertwines all fibre-sums of fine projectors with the target projectors if and only if it maps ker (τ (a i)) into ker (υ (b (q i))) for every i. This criterion requires no scalar-linearity or intertwining of represented elements; its only annihilation premises are that both represented products vanish. The eight coefficient, scalar, module and index universes are independent. Both label sets are finite here because the canonical families are finite.

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
LeanRingHom.linearEquivPiKer

TheoremFinite generation under pointwise unimodular clearing#

For arbitrary, possibly noncommutative semirings R, S and f : M →ₛₗ[φ] N between additive commutative left semimodules, Submodule.fg_of_fg_comap_of_one_mem_span_smul_mem_range proves an S-submodule P finitely generated if P.comap f is finitely generated over R and, for every n ∈ P, the clearers {a : S | ∃ m : M, f m = a • n} generate the unit left ideal. The companion span_image_comap_eq_of_one_mem_span_smul_mem_range identifies P with the target-scalar span of its comap image without any finite-generation premise. The existing single-left-inverse and unit-clearing criteria remain specializations. The four universes are independent; neither Noetherianity nor surjectivity of φ or f is required.

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.fg_of_fg_comap_of_one_mem_span_smul_mem_range

TheoremSemilinear Noetherian ascent#

For arbitrary semirings R, S, additive commutative semimodules M, N and f : M →ₛₗ[φ] N, isNoetherian_of_left_inv_smul_mem_range transfers IsNoetherian R M to IsNoetherian S N if each n admits m, a, b with b * a = 1 and f m = a • n. The four universes are independent; neither φ nor f must be surjective. The isNoetherian_of_unit_smul_mem_range corollary retains the familiar unit-clearing hypothesis, while isNoetherian_of_surjective_semilinear requires only function-surjectivity of f.

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_of_left_inv_smul_mem_range

TheoremArtin–Rees for Noetherian modules#

For an arbitrary commutative ring R, ideal I and submodule K of a Noetherian R-module M, Ideal.exists_pow_inf_eq_pow_smul_of_isNoetherian gives a constant c such that (I ^ n • ⊤) ⊓ K = I ^ (n - c) • ((I ^ c • ⊤) ⊓ K) for every n ≥ c. Neither Noetherianity of R nor finite generation of I is assumed. The ring and module universes are independent. The proof uses Mathlib's full Artin–Rees theorem over the quotient by the module's annihilator. The shifted-cofinality client uses the full equality at Mathlib's Noetherian-ring and finite-module 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.exists_pow_inf_eq_pow_smul_of_isNoetherian

DefinitionSubmodule adic cofinality#

For an arbitrary ideal I of a commutative ring R, Ideal.HasSubmoduleAdicCofinality expresses ∀ n, ∃ m, N ⊓ (I ^ m • ⊤) ≤ I ^ n • N for every submodule N of every finite R-module. This is Fujiwara--Kato's (AP); restricting to finitely generated submodules gives the existing Ideal.HasFiniteSubmoduleAdicCofinality condition (APf). Both .cofinal eliminators allow an independent module universe. Nilpotent ideals satisfy (AP) without Noetherianity or finite generation of the ideal or submodule; every ideal of a Noetherian ring satisfies it by Artin–Rees. The ambient module need not be finitely presented. Cofinality is pointwise, not a full shifted Artin–Rees equality. The APf providers follow from (AP), and the range client applies the APf API to maps between finite modules in independent universes.

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.HasSubmoduleAdicCofinality

TheoremPower-killed submodule criteria#

For an ideal I of a commutative ring R, Ideal.hasSubmoduleAdicCofinality_iff_forall_exists_inf_pow_smul_eq_bot characterizes (AP) by ∃ m, N ⊓ (I ^ m • ⊤) = ⊥ whenever ∃ k, I ^ k • N = ⊥, for every submodule N of every finite R-module. The corresponding (APf) criterion tests only finitely generated N. Both .exists_inf_pow_smul_eq_bot consumers allow an independent module universe. A single common exponent kills the whole submodule; I need not be finitely generated or nilpotent. The converse uses images in canonical module quotients over the original coefficient ring R.

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.hasSubmoduleAdicCofinality_iff_forall_exists_inf_pow_smul_eq_bot

TheoremDescent of adic cofinality#

For commutative rings R, A, Ideal.HasSubmoduleAdicCofinality.of_map_of_faithfullyFlat descends (AP) from I.map (algebraMap R A) to I along a faithfully flat algebra. Alternatively, Ideal.HasSubmoduleAdicCofinality.of_map_of_linearRetraction uses an R-linear map p : A →ₗ[R] R with p 1 = 1, without a flatness hypothesis; p need not preserve multiplication. Both have corresponding HasFiniteSubmoduleAdicCofinality methods for (APf). The algebra need not be module-finite, the ideal need not be finitely generated, and no finite presentation or Noetherian hypothesis is required. The pointwise linear-retraction theorem works over commutative semirings and arbitrary semimodules; its tensor membership and inclusion-reflection lemmas even allow noncommutative scalar algebras. All 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
LeanIdeal.HasSubmoduleAdicCofinality.of_map_of_faithfullyFlat

TheoremAdic cofinality on finite products#

For an arbitrary ideal I of Π i, R i, with [Finite ι] and commutative rings R i, Ideal.hasSubmoduleAdicCofinality_iff_forall_map_evalRingHom gives (AP) for I iff each projection image I.map (Pi.evalRingHom R i) has (AP). The companion hasFiniteSubmoduleAdicCofinality_iff_forall_map_evalRingHom does the same for (APf). The characteristic criteria also cover unary Ideal.pi and binary Ideal.prod, with independent binary ring universes. Empty products and zero factors are allowed. Full (AP) covers every submodule of every finite module; (APf) requires only the submodule to be finitely generated. No ideal-FG, Noetherian or ambient finite-presentation hypothesis is added. Infinite products are not covered by these equivalences.

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.hasSubmoduleAdicCofinality_iff_forall_map_evalRingHom

TheoremCofinal ideal powers#

For ideals I, J of a commutative ring with I ^ a ≤ J and J ^ b ≤ I for some natural numbers a, b, Ideal.hasSubmoduleAdicCofinality_iff_of_pow_le makes (AP) equivalent for I and J; the companion hasFiniteSubmoduleAdicCofinality_iff_of_pow_le does the same for (APf). The witnesses may be zero. In particular, replacing an ideal by any positive power preserves both conditions. The shared pointwise theorem Submodule.adic_cofinality_iff_of_pow_le already applies to arbitrary left ideals of a semiring and arbitrary submodules of an additive commutative semimodule, with its given action and independent carrier universes. This comparison needs no finiteness or additive-inverse 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
LeanIdeal.hasSubmoduleAdicCofinality_iff_of_pow_le

TheoremSemilinear transport of adic cofinality#

For semirings R, S, a coefficient equivalence σ : R ≃+* S and a compatible semilinear equivalence e : M ≃ₛₗ[(σ : R →+* S)] P between additive commutative semimodules with their given actions, Submodule.adic_cofinality_iff_of_semilinearEquiv transports ∀ n, ∃ m, N ⊓ (I ^ m • ⊤) ≤ I ^ n • N to the condition for I.map σ.toRingHom and N.map e.toLinearMap. It allows arbitrary left ideals and submodules in four independent universes, without finiteness or additive inverses. For commutative rings, the companion Ideal.hasSubmoduleAdicCofinality_iff_of_ringEquiv and Ideal.hasFiniteSubmoduleAdicCofinality_iff_of_ringEquiv give (AP)/(APf) invariance under coefficient equivalence. Both predicates quantify over finite ambient modules; only (APf) restricts submodules to be finitely generated.

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.adic_cofinality_iff_of_semilinearEquiv

Stability of adic cofinality under scalar extension. Over commutative rings, both (AP) and (APf) pass from an ideal I to its extension I.map (algebraMap R A) along a module-finite R-algebra A, or along an arbitrary localization algebra. The localization algebra need not be finite over R. The respective .map and .map_of_isLocalization interfaces are in AdicCompatibility. Neither ideal finite generation nor finite presentation or Noetherianity is required; the original target action and independent carrier universes are retained.

Adic cofinality near a closed locus. For an ideal I of a commutative ring R and any set s : Set R with I ⊔ Ideal.span s = ⊤, (AP) holds for I if and only if it holds for every extension to Localization.Away f, f ∈ s; the same equivalence holds for (APf). The hasSubmoduleAdicCofinality_iff_forall_map_away and finite-submodule counterpart need only a distinguished-open cover of V(I), not of the whole spectrum. The set need not be finite. The ambient modules remain finite, with arbitrary submodules for (AP) and finitely generated submodules for (APf); no ideal-FG, ambient finite-presentation or Noetherian hypothesis is added. Cutoffs are pointwise, not a uniform shift or denominator bound, and this is not a stalkwise criterion.

TheoremKrull intersection from adic cofinality#

For a finite module M and an ideal I satisfying finite-submodule adic cofinality, Ideal.HasFiniteSubmoduleAdicCofinality.mem_iInf_pow_smul_top_iff characterizes membership in ⨅ n, I ^ n • ⊤ by a scalar a ∈ I fixing the element. The relative bound I ≤ (Module.annihilator R M).jacobson makes this intersection zero. For any submodule N with finite quotient, membership in ⨅ n, N ⊔ I ^ n • ⊤ is equivalent to (1 - a) • x ∈ N for some a ∈ I; a Jacobson bound relative to the quotient annihilator makes the intersection equal to N. The ambient module and N need not be finite in the quotient statements. No ideal-FG, finite-presentation or Noetherian hypothesis is added, and the ring and module universes are independent. These are algebraic intersection results, not assertions of topological closedness or completeness.

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.HasFiniteSubmoduleAdicCofinality.mem_iInf_pow_smul_top_iff

TheoremFinite generation from the first adic quotient#

For an arbitrary submodule N of a finite original R-module M, Submodule.fg_iff_finite_quotient_smul detects N.FG on the intrinsic quotient N / I N over R, assuming APf and I ≤ (Module.annihilator R M).jacobson. This is not the quotient by N ∩ I M, and neither ideal-FG nor a Noetherian, finite-presentation, flatness or completeness hypothesis is required.

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.fg_iff_finite_quotient_smul

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.