Faithfully flat dependent… to Finite-type ideal/module…

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

TheoremFaithfully flat dependent direct sums#

For arbitrary families of additive commutative groups with module structures over a CommRing R, Module.FaithfullyFlat.directSum_iff characterizes faithful flatness of the direct sum by flatness of every component and a nontrivial quotient-tensor fiber in some component for each proper ideal of R. The detecting component may depend on the ideal; the components need not individually be faithfully flat. The ring, index and carrier universes are independent, and empty indexing types are allowed. One faithfully flat component is sufficient when every component is flat.

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

TheoremFinitely generated ideals and dependent products#

Over a CommSemiring R, Submodule.smul_pi_of_fg says that multiplication by a finitely generated ideal commutes with the full dependent product of submodules of additive commutative R-modules. The index type is arbitrary, including empty, and the semiring, index and 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
LeanSubmodule.smul_pi_of_fg

TheoremFaithful flatness after base change covering maximal ideals#

For commutative rings R and S with an R-algebra structure on S, suppose every maximal ideal m of R satisfies m.map (algebraMap R S) ≠ ⊤. For any additive commutative group M with an R-module structure, Module.FaithfullyFlat.iff_flat_and_baseChange_of_map_maximal_ne_top characterizes faithful flatness over R by original flatness Module.Flat R M and faithful flatness over S of S ⊗[R] M, with the canonical left tensor-factor action. The three universes are independent. No flatness of S over R, surjectivity, algebra structure on M, finiteness, Noetherianity, localness, topology or completion is assumed. For I ≤ Ideal.jacobson (⊥ : Ideal R), Module.FaithfullyFlat.iff_flat_and_baseChange_of_le_jacobson specializes this to the canonical quotient R ⧸ I. For commutative R-algebras S, Module.FaithfullyFlat.iff_flat_and_quotient_of_le_jacobson gives the equivalent formulation using the canonical quotient algebra R ⧸ I → S ⧸ I.map (algebraMap R S). Conversely, Algebra.map_maximal_ne_top_iff_forall_faithfullyFlat_baseChange characterizes the maximal-ideal hypothesis itself: it holds if and only if scalar extension preserves and reflects faithful flatness for every originally flat R-module in Type (max u w), where R : Type u and w is arbitrary. The universe of S remains independent. The converse uses the direct sum of principal localizations indexed by all elements of a maximal ideal, without assuming that ideal is finitely generated. The quotient client applies this corollary to the nonsurjective rank-two diagonal over ZMod 4 with the proper nonzero square-zero ideal (2). Its inputs are obtained independently from basis-derived faithful flatness.

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

TheoremFaithful flatness of unital algebras#

For a CommRing R and a unital R-algebra A whose underlying ring may be noncommutative, Module.FaithfullyFlat.algebra_iff_flat_and_fg_proper_ideal characterizes faithful flatness by flatness and I • (⊤ : Submodule R A) ≠ ⊤ for every finitely generated proper ideal I. The algebra structure is material; this finitely generated ideal criterion is not asserted for arbitrary modules.

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

TheoremFaithfully flat products of algebras#

Over a CommRing R, for an arbitrary dependent family of unital, possibly noncommutative R-algebras A i, Module.FaithfullyFlat.pi_algebra_iff characterizes faithful flatness of Π i, A i by flatness of the whole product and a nontrivial fiber (R ⧸ I) ⊗[R] A i in some component for every finitely generated proper ideal I. The detecting component may depend on the ideal. Componentwise flatness cannot replace whole-product flatness, and the components need not individually be faithfully flat. The ring, index and carrier universes are independent, and empty products are allowed.

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

TheoremProducts of localizations at submonoids#

For a CommRing R, arbitrary submonoids S i and commutative R-algebras A i realizing the localizations at S i, Module.FaithfullyFlat.pi_localization_iff characterizes faithful flatness of Π i, A i by flatness of the whole product and, for every finitely generated proper ideal I, disjointness of I from some S i. These are products with the common diagonal R-action; neither finite nor nonempty indexing is required, and zero rings are allowed.

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

TheoremFamilies of principal localizations#

For a CommRing R and any family s : ι → R, Module.FaithfullyFlat.directSum_away_iff characterizes faithful flatness of ⨁ i, Localization.Away (s i) by Ideal.span (Set.range s) = ⊤, without finite or nonempty indexing. For finite index types, Module.FaithfullyFlat.pi_away_iff gives the same unit-span criterion for Π i, Localization.Away (s i). The localizations need not individually be faithfully flat; zero rings and independent ring and index universes are allowed. The finite-index hypothesis for the product unit-span criterion is essential: the coordinate-idempotent product is faithfully flat although its generators span a proper ideal. The ideal-detection consequences show that this ideal is not 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
LeanModule.FaithfullyFlat.directSum_away_iff

TheoremFaithfully flat coherence descent#

Module.IsCoherent.of_isCoherent_tensorProduct_of_faithfullyFlat descends coherence of the canonical scalar extension S ⊗[R] M to the original module M. The scalar algebra S may be noncommutative; no finiteness hypothesis on M or module-finiteness of S is needed. The regular-module consequence IsCoherentRing.of_faithfullyFlat descends ring coherence. The original module's additive monoid and action are retained, with independent ring, algebra and module 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
LeanModule.IsCoherent.of_isCoherent_tensorProduct_of_faithfullyFlat

ClassUniversal coherence#

IsUniversallyCoherent asserts coherence for finitely presented commutative algebras in an independently chosen target universe; the library derives base coherence at v = u and supplies the Noetherian case. Finitely presented algebra extensions preserve universal coherence with independent base, extension and target universes. In particular, polynomial rings over universally coherent rings are universally coherent; no module-finiteness hypothesis is needed. Coherence of all finite-variable polynomial rings characterizes universal coherence at the base-ring universe and implies universal coherence in every independently chosen target universe. In particular, base-universe universal coherence suffices for arbitrary target universes; no converse from an arbitrary smaller target universe is asserted. Polynomial rings in an arbitrary type of variables over a base-universe universally coherent ring are universally coherent, with independent variable and target universes; neither finitely many variables nor a Noetherian base is required. Arbitrary localizations of base-universe universally coherent rings are universally coherent, with independent localization and target universes. No finite denominator family or algebra finite-presentation hypothesis on the localization 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
LeanIsUniversallyCoherent

TheoremAssociative square-zero multiplication#

For a type R with multiplication and an additive monoid M with distributive left and right actions, TrivSqZeroExt.mul_assoc_iff characterizes associativity by coefficient associativity, composition of each action (in reversed coefficient order on the right), and commutation of the two actions. Addition need not commute, the carrier universes are independent, and no coefficient zero, one, or identity law for either action 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
LeanTrivSqZeroExt.mul_assoc_iff

TheoremCommutativity of square-zero extensions#

For Mul R, AddZeroClass M, IsAddCommutative M, and two given zero-preserving scalar actions [SMulZeroClass R M] and [SMulZeroClass Rᵐᵒᵖ M], TrivSqZeroExt.isMulCommutative_iff characterizes IsMulCommutative (TrivSqZeroExt R M) by IsMulCommutative R ∧ IsCentralScalar R M. It retains the original multiplication, addition, zero and both actions, with independent carrier universes. No additive associativity, coefficient zero or one, module structure, action compatibility or finiteness is required. This is a criterion for the multiplication alone, not an assertion of a unit or a square-zero ideal at these 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
LeanTrivSqZeroExt.isMulCommutative_iff

DefinitionSquare-zero kernels and projection base change#

For a commutative semiring R and an additive commutative R-module M, TrivSqZeroExt.kerIdealLinearEquiv identifies the projection kernel with M. If M is finite over R, kerIdeal_finite makes the kernel finite over the whole extension. kerIdealBaseChange identifies the projection-base-changed kernel with M without a finiteness assumption; its pure-tensor and inverse formulas are simp lemmas.

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
LeanTrivSqZeroExt.kerIdealLinearEquiv

DefinitionFull left-ideal lattice of square-zero extensions#

For a possibly noncommutative division semiring D : Type u and an additive commutative group M : Type v with its given actions [Module D M], [Module Dᵐᵒᵖ M] and [SMulCommClass D Dᵐᵒᵖ M], TrivSqZeroExt.idealOrderIsoWithTop identifies Ideal (TrivSqZeroExt D M) with WithTop (Submodule D M) as ordered lattices. The two carrier universes are independent. A coefficient submodule N corresponds to 0 × N, using the original left action. The adjoined top is the whole extension, whereas the coerced internal top is the proper projection kernel K = RingHom.ker (TrivSqZeroExt.fstHom ℕ D M : TrivSqZeroExt D M →+* D), even when M is zero. The coatom client derives maximality of this kernel through the order isomorphism. No ring structure on D, centrality or finiteness assumption is required. Coefficient submodules can be cones rather than additive subgroups and need not be stable under the right action; this classifies left ideals, not only two-sided ideals.

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
LeanTrivSqZeroExt.idealOrderIsoWithTop

TheoremModule length and square-zero extensions#

For modules over arbitrary rings, LinearMap.length_eq_of_bijective preserves length under a bijective semilinear map whose scalar homomorphism is surjective, without requiring that scalar homomorphism to be injective. The rings and modules have four independent universes, and infinite lengths are included. Its algebra-map specialization recovers Mathlib's surjective-algebra comparison under the same hypotheses. For a division ring D and the original compatible left/right actions on M, TrivSqZeroExt.length computes the regular left-module length as Module.length D M + 1, directly from the ideal-lattice classification. Only the finrank corollary adds [Module.Finite D M]; neither centrality nor right-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
LeanLinearMap.length_eq_of_bijective

DefinitionOpposites of square-zero extensions#

TrivSqZeroExt.opEquiv identifies (TrivSqZeroExt R M)ᵐᵒᵖ with TrivSqZeroExt Rᵐᵒᵖ M by op (r, m) ↦ (op r, m). The target uses the original right action on the left and the original left action pulled back by double unop on the right. The equivalence needs only Add R, Mul R, AddCommMagma M, and the two given scalar actions. For a division ring D and an AddCommGroup M with commuting bimodule actions, the double-opposite module is Module.compHom M (RingEquiv.opOp D).symm.toRingHom. The preceding left criterion and coherence transport then give the right-coherence criterion IsCoherentRing ((TrivSqZeroExt D M)ᵐᵒᵖ) ↔ Module.Finite Dᵐᵒᵖ M, with finiteness measured using the original right action, without centrality or a comparison of left and right dimensions.

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
LeanTrivSqZeroExt.opEquiv

TheoremLeft Noetherian square-zero extensions#

For a possibly noncommutative Ring R and an AddCommMonoid M with commuting left and right R-module actions, TrivSqZeroExt.isNoetherianRing_iff characterizes IsNoetherianRing (TrivSqZeroExt R M) by IsNoetherianRing R ∧ Module.Finite R M. Finiteness here is as a left R-module. The companion TrivSqZeroExt.isNoetherianRing_iff_isNoetherian replaces Module.Finite R M by IsNoetherian R M. Centrality is not required, and the two 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
LeanTrivSqZeroExt.isNoetherianRing_iff

TheoremFinite-type ideal/module transfer#

Over a commutative base ring, Ideal.ideal_property_iff_module_property equates a property on all finitely generated ideals with one on all finite modules over finite-type algebras. The property must be invariant under compatible algebra/module isomorphisms and descend along every compatible surjective square-zero algebra map for finite source modules. The base universe is independent of the common algebra/module universe. Finite type does not mean module-finite over the base, and arbitrary ideals need not 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
LeanIdeal.ideal_property_iff_module_property

The foundation, finite-presentation and coherent-module category results allow arbitrary Ring. Coherent semilinear Hom allows arbitrary source and target scalar Semirings with a commuting Ring action on the target. Localization of coherent modules and universal coherence use CommRing. Coherent tensor closure uses a CommRing base but allows an independent, possibly noncommutative Ring acting on the coherent factor. The square-zero commutativity criterion uses only Mul, AddZeroClass, IsAddCommutative and the two given SMulZeroClass actions. The square-zero kernel and base-change results use CommSemiring and AddCommMonoid; the full left-ideal classification uses DivisionSemiring and AddCommGroup with both given commuting module actions. The square-zero Noetherian criterion allows Ring and AddCommMonoid with commuting bimodule actions. The coherent-extension sufficiency and injective-vector necessity use Ring and AddCommGroup, without centrality. The finite-generation biconditional uses an arbitrary division ring and the given compatible bimodule with AddCommGroup; its canonical-field specialization gives finite dimensionality. The predicate transfer uses CommRing and AddCommGroup. The ideal/product identity and semilinear mono-flatness invariance use CommSemiring and AddCommMonoid; the faithful-flatness criteria use CommRing and require no coherence or projectivity assumption. Module carrier universes are independent where stated. Zero rings/modules, empty indexing sets and rank-zero finite free modules are not excluded. Consult the linked source statements and guide for exact hypotheses. This is not a coherent-sheaf theory or a claim to formalize an entire source.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.