Finite presentation from… to Faithfully flat tensor products

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

TheoremFinite presentation from cofinal ideal quotients#

For a finite module M over a commutative ring R and an ideal I satisfying full submodule adic cofinality and I ≤ Ideal.jacobson ⊥, Ideal.finitePresentation_iff_forall_quotient_smul detects finite presentation over R on all reductions M / J j M over R / J j, for any family J : ι → Ideal R with ∀ n : ℕ, ∃ j, J j ≤ I ^ n. The positive-powers criterion Ideal.finitePresentation_iff_forall_quotient_pow_smul is a specialization. The ring, module and index universes are independent; no ideal finite generation or ordering condition on the family 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
LeanIdeal.finitePresentation_iff_forall_quotient_smul

TheoremEssentially finite-type scalar extension#

For commutative rings R, S, an essentially finite-type R-algebra structure on S, and a Noetherian R-module M, Algebra.EssFiniteType.isNoetherian_tensorProduct makes S ⊗[R] M Noetherian over S with its canonical left-factor action. The three universes are independent, and M need only be an additive commutative monoid with its given module structure. Neither ambient ring must be Noetherian; no flatness, faithfulness or finite presentation is assumed. This includes finite-type algebras and arbitrary localizations.

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
LeanAlgebra.EssFiniteType.isNoetherian_tensorProduct

ClassCoherent modules and kernels#

For a ring and an additive commutative monoid with its given module structure, Module.IsCoherent means finite generation together with finite presentation of every finitely generated submodule. Module.IsCoherent.iff_finite_and_fg_ker characterizes this by finitely generated kernels of all linear maps from finite-rank free modules, including rank zero. The same leaf proves closure under finitely generated submodules, finite products, kernels and cokernels, quotients by finitely generated submodules, and extensions (with the stated exactness and endpoint conditions). For rings R and S, Module.IsCoherent.of_restrictScalars transfers coherence of an additive commutative group N from R to S when S is finite over R and the given module structures form scalar towers R → S → S and R → S → N. No coherence of S over R is required, and the three 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.IsCoherent

TheoremCoherent homology#

Over any possibly noncommutative Ring R, a three-term complex S : CategoryTheory.ShortComplex (ModuleCat.{v} R) with finite left term S.X₁ and coherent middle and right terms S.X₂, S.X₃ has coherent homology, by CategoryTheory.ShortComplex.isCoherent_homology. The conclusion concerns the chosen categorical S.homology with its given R-action. Neither the left term nor R is assumed coherent, and no exactness hypothesis is imposed. The ring universe is independent of the common object universe v.

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
LeanCategoryTheory.ShortComplex.isCoherent_homology

TheoremCoherence along semilinear retractions#

For arbitrary rings R, S and additive commutative monoids N, M with their given R- and S-module structures, let σ : R →+* S, τ : S →+* R, f : N →ₛₗ[σ] M and g : M →ₛₗ[τ] N satisfy τ ∘ σ = id and g ∘ f = id. Then Module.IsCoherent.of_semilinear_retract descends coherence of M over S to coherence of N over R. The four carrier universes are independent; no additional scalar action, finiteness, flatness, Noetherianity, faithfulness or nontriviality assumption is required. The regular-module corollary IsCoherentRing.of_retract says that a ring retract of a coherent ring is coherent, including noncommutative rings.

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.IsCoherent.of_semilinear_retract

TheoremCoherent dependent direct sums#

For an arbitrary index type, a possibly noncommutative ring R, and additive commutative monoids M i with their given R-module structures, Module.IsCoherent.directSum_iff gives 

Module.IsCoherent R (DirectSum ι M) ↔
  (∀ i, Module.IsCoherent R (M i)) ∧ Set.Finite {i | ¬ Subsingleton (M i)}
Thus the nontrivial summands, not the ambient index type, must form a finite set. Coherence means finite generation and finite presentation of every finitely generated submodule. Empty index types, zero summands and zero rings are allowed; no base-ring coherence, Noetherianity, faithfulness or commutativity assumption is added. The index, ring and summand universes are independent. Module.IsCoherent.of_directSum reflects coherence to each original coordinate without a finite-index assumption. The supporting Module.Finite.finite_nontrivial_summands already obtains finiteness of the nontrivial summands from finite generation over a 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
LeanModule.IsCoherent.directSum_iff

TheoremCoherence over product coefficient rings#

For any dependent family of possibly noncommutative rings R i and additive commutative monoids M i with their given R i-module structures, Module.IsCoherent.of_piRing reflects coherence of the product to each coordinate. For [Finite ι], Module.IsCoherent.piRing_iff gives the converse as well: 

Module.IsCoherent (∀ i, R i) (∀ i, M i) ↔
  ∀ i, Module.IsCoherent (R i) (M i)
The action is (r • m) i = r i • m i, with independently variable coordinate scalars, not a common diagonal scalar ring. The index, coefficient and module universes are independent. Reflection allows an arbitrary index type; the equivalence requires only [Finite ι]. Empty products, zero rings and zero modules are allowed. No Noetherianity, commutativity, faithfulness or extra finite-generation hypothesis is assumed. The regular-module specialization isCoherentRing_pi_iff characterizes coherence of the product ring by coherence of every factor. Coherence of an arbitrary coordinate module does not assert coherence of its coefficient ring. The supporting Module.Finite.piRing_iff proves the corresponding finite-generation equivalence already for semirings and additive commutative monoids. These equivalences concern finite products; coordinatewise coherence does not in general imply coherence of an infinite product module over its product coefficient ring.

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.IsCoherent.of_piRing

TheoremFinite presentation over product coefficient rings#

For any dependent family of possibly noncommutative rings R i and additive commutative monoids M i with their given R i-module structures, Module.FinitePresentation.of_piRing reflects finite presentation of Π i, M i over Π i, R i to each coordinate. This direction allows an arbitrary index type. For [Finite ι], Module.FinitePresentation.piRing_iff gives the converse as well: 

Module.FinitePresentation (∀ i, R i) (∀ i, M i) ↔
  ∀ i, Module.FinitePresentation (R i) (M i)
The action is (r • m) i = r i • m i; the index, coefficient and module universes are independent. No supplied additive group structure, coherence, Noetherianity, commutativity or nontriviality is required. Empty products and zero factors are allowed. The varying-rank client combines free modules over the integers and a noncommutative integer matrix ring.

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.FinitePresentation.of_piRing

TheoremFinite presentation along scalar towers#

For possibly noncommutative rings R, S and an additive commutative monoid N with its given R- and S-module structures and towers R → S → S and R → S → N, Module.FinitePresentation.trans_of_tower gives finite presentation of N over R from finite presentation of S over R and of N over S. Conversely, of_restrictScalars gives finite presentation over S from finite presentation over R assuming only that S is finite over R. Thus restrictScalars_iff equates the two finite- presentation properties when S is finitely presented over R, without assuming either property of N in advance. The three universes are independent; no coherence, Noetherianity, centrality or faithfulness is required. trans_of_algebra recovers the type and argument order of Mathlib's commutative-algebra Module.FinitePresentation.trans as a corollary of the scalar-tower theorem.

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.FinitePresentation.trans_of_tower

TheoremCoherence along quotient coefficients#

For possibly noncommutative rings R, S and additive commutative monoids N, M with their given R- and S-module structures, Module.isCoherent_iff_of_bijective_of_fg_ker gives Module.IsCoherent R N ↔ Module.IsCoherent S M along a bijective semilinear map f : N →ₛₗ[σ] M, provided σ : R →+* S is surjective and (RingHom.ker σ).FG. Kernel finite generation is as a left ideal, not merely as a two-sided ideal. The four carrier universes are independent; σ need not be injective. No extra action, scalar inverse, coherence of an ambient ring, Noetherianity, flatness or nontriviality 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
LeanModule.isCoherent_iff_of_bijective_of_fg_ker

TheoremCoherence under scalar restriction#

For possibly noncommutative rings R and S, if S is coherent as an R-module, then Module.FinitePresentation.isCoherent_restrictScalars makes every finitely presented S-module N coherent for its given R-action. The additive commutative group N has its given module structures and scalar towers R → S → S and R → S → N; the three universes are independent. Under these hypotheses, coherence over R, coherence over S, and finite presentation over S are equivalent. No coherence assumption on R, Noetherianity, centrality or faithfulness is required. The identity-scalar specialization Module.isCoherent_iff_finitePresentation identifies the two properties over an IsCoherentRing R, yielding finite presentation of kernels between finitely presented modules. The of_exact_five criterion gives finite presentation of M₃ in M₁ → M₂ → M₃ → M₄ → M₅ when the sequence is exact at M₂, M₃, M₄, M₁ is finite, and M₂, M₄, M₅ are finitely presented. It requires neither endpoint injectivity nor surjectivity.

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.FinitePresentation.isCoherent_restrictScalars

Localization and descent. of_isLocalizedModule transports coherence along an arbitrary commutative-ring/module localization realized by its universal property, not a surjective map. The of_localizationSpan' theorem descends coherence from localizations away from a family whose ideal span is ⊤.

TheoremHom, tensor, and categories#

For semirings R, R₂, a ring S, and any σ : R →+* R₂, Module.IsCoherent.semilinearMap makes M →ₛₗ[σ] N coherent over S when the additive commutative group M is finitely presented over R and the additive commutative group N is coherent over S, with commuting given R₂- and S-actions on N. The five universes are independent and the Hom action is pointwise. No S-action on M, R-action on N, scalar commutativity or surjectivity of σ is required. The existing linearMap theorem is its same-base commutative-ring specialization. For a commutative base ring R and an independent, possibly noncommutative ring S, tensorProduct_left makes M ⊗[R] N coherent over S when M is coherent over S, N is finitely presented over R, and the given R- and S-actions on M commute. No R-module structure on S or S-action on N is required. The existing tensorProduct theorem retains the same-base, finitely-presented-first specialization. These are theorems, not global instances, and assume neither coherence nor Noetherianity of an ambient scalar ring. CoherentModuleCat is a transparent full subcategory with abelian structure obtained through generic category constructions.

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.IsCoherent.semilinearMap

TheoremCoherent right duals#

For a possibly noncommutative Ring R and a finitely presented left R-module M with its given AddCommMonoid and module structure, Module.FinitePresentation.isCoherent_dual gives Module.IsCoherent Rᵐᵒᵖ (Module.Dual R M) assuming only right coherence [IsCoherentRing Rᵐᵒᵖ] of the ring. The dual uses the canonical right action (q • f) x = f x * MulOpposite.unop q for q : Rᵐᵒᵖ, induced by right multiplication on the codomain R. The ring and module universes are independent; neither left coherence nor a supplied additive group structure on M 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
LeanModule.FinitePresentation.isCoherent_dual

TheoremFinite-module tensor zero detection#

For an arbitrary additive commutative R-module P over a CommRing R, Module.forall_maximal_smul_top_ne_top_iff_forall_finite_tensorProduct characterizes zero-object detection on all finite modules by m • (⊤ : Submodule R P) ≠ ⊤ for every maximal ideal m. Module.subsingleton_tensorProduct_iff_of_finite gives Subsingleton (P ⊗[R] M) ↔ Subsingleton M for a single finite module in an independent universe. No flatness, faithfulness or finiteness of P is required. This detects zero objects, not zero maps or isomorphisms. The clients recover the finite faithfully-flat and local residue-field criteria and use a countable direct sum of residue fields.

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

TheoremIdeal action on finite coefficients#

For an FG submodule N of an arbitrary additive commutative module over a CommRing R, Submodule.FG.ideal_smul_eq_self_iff_sup_annihilator_eq_top says I • N = N ↔ I ⊔ N.annihilator = ⊤ for every ideal I. For finite P, Module.forall_maximal_smul_top_ne_top_iff_annihilator_le_jacobson characterizes proper image under every maximal ideal by Module.annihilator R P ≤ Ideal.jacobson ⊥, with no flatness or faithful-action assumption. The clients recover relative Jacobson properness and supply the finite tensor-detection input.

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

TheoremSemilinear invariance of flatness#

For equivalent commutative semirings e : R ≃+* S and a compatible semilinear equivalence from an additive commutative R-module M to an additive commutative S-module N, Module.Flat.semilinearEquiv_iff gives Module.Flat R M ↔ Module.Flat S N for both given scalar actions. Module.Flat.of_semilinearEquiv e E takes flatness of N to flatness of M. The four carrier universes are independent. Over semirings, this is Mathlib's mono-flatness (tensoring preserves injective linear maps); over rings it is usual flatness. No faithful action, finiteness or additive cancellation is required. The identity coefficient equivalence accepts the same ordinary linear equivalence as Mathlib's fixed-ring flatness API.

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.Flat.semilinearEquiv_iff

TheoremAnnihilators under finite-limit-preserving scalar extension#

For a CommSemiring R, a possibly noncommutative Semiring S with Algebra R S, and a finitely generated semimodule M, Module.annihilator_tensorProduct_eq_map_of_finite_of_preservesFiniteLimits gives 

Module.annihilator S (S ⊗[R] M) =
  Ideal.map (algebraMap R S) (Module.annihilator R M)
provided the stock SemimoduleCat tensor-left functor for the lifted S preserves finite limits over the lifted R, at the common universe max uR (max uS uM). The conclusion uses the original S and original tensor product; the three original universes are independent. Here finite means Module.Finite R M, not a finite carrier. No additive cancellation, subtractivity, faithful action, finite presentation or Noetherianity is required. This condition is not identified with mono-flatness over semirings. Over commutative rings, flatness supplies this condition through the existing module–semimodule equivalence. For any module M over a commutative ring R and a flat, possibly noncommutative R-algebra S, Module.annihilator_tensorProduct_eq_iInf_map_of_flat identifies the annihilator of S ⊗[R] M with the intersection of the ideals generated by the images of Module.annihilator R N, over all finitely generated original submodules N ≤ M. This is not a claim that ideal extension commutes with arbitrary intersections. For finite M, Module.annihilator_tensorProduct_eq_map_of_finite_of_flat identifies it with the ideal generated by Module.annihilator R M itself. The tensor has its canonical left-factor action; M needs no S-action. S need only be a semiring and M an additive commutative monoid with the given structures. The three universes are independent. No Noetherianity, finite presentation, flatness or faithfulness of M, or faithful flatness of S is required. The clients evaluate the intersection for the nonfinite free abelian group ℕ →₀ ℤ after rational scalar extension and recover finite faithful-action preservation over ring coefficients. The existing FaithfulSMul.baseChange_of_finite_of_flat additionally allows commutative semiring coefficients.

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

TheoremAnnihilator contraction under faithfully flat extension#

Over a CommRing R, Module.FaithfullyFlat.annihilator_tensorProduct_eq says tensoring an arbitrary R-module M with a faithfully flat module P preserves its annihilator over R. Here P is only a module group, while M needs only an additive commutative monoid structure. For a faithfully flat, possibly noncommutative ring algebra S, Module.comap_annihilator_tensorProduct_of_faithfullyFlat identifies contraction of the annihilator of S ⊗[R] M with the original annihilator. The tensor has its canonical left-factor action and M needs no S-action. All three carrier universes are independent, with no finiteness, flatness or faithfulness assumption on M. The module client derives preservation and reflection of faithful action over the coefficient ring; this does not assert faithful action over a larger scalar algebra.

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.FaithfullyFlat.annihilator_tensorProduct_eq

TheoremFaithfully flat tensor products#

Over a CommRing R, for additive commutative groups C and D with R-module structures, Module.FaithfullyFlat.tensorProduct_iff says that C ⊗[R] D is faithfully flat over R if and only if both C and D are faithfully flat over R. The ring and the two module universes are independent; no finiteness, projectivity 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
LeanModule.FaithfullyFlat.tensorProduct_iff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.