Flat modules #
A module M over a commutative semiring R is mono-flat if for all monomorphisms of modules
(i.e., injective linear maps) N →ₗ[R] P, the canonical map N ⊗ M → P ⊗ M is injective
(cf. [Katsov2004], [KatsovNam2011]).
To show a module is mono-flat, it suffices to check inclusions of finitely generated
submodules N into finitely generated modules P, and P can be further assumed to lie in
the same universe as R.
M is flat if · ⊗ M preserves finite limits (equivalently, pullbacks, or equalizers).
If R is a ring, an R-module M is flat if and only if it is mono-flat, and to show
a module is flat, it suffices to check inclusions of finitely generated ideals into R.
See https://stacks.math.columbia.edu/tag/00HD.
Currently, Module.Flat is defined to be equivalent to mono-flatness over a semiring.
It is left as a TODO item to introduce the genuine flatness over semirings and rename
the current Module.Flat to Module.MonoFlat.
Main declaration #
Module.Flat: the predicate asserting that anR-moduleMis flat.
Main theorems #
Module.Flat.of_retract: retracts of flat modules are flatModule.Flat.of_linearEquiv: modules linearly equivalent to a flat modules are flatModule.Flat.directSum: arbitrary direct sums of flat modules are flatModule.Flat.of_free: free modules are flatModule.Flat.of_projective: projective modules are flatModule.Flat.preserves_injective_linearMap: IfMis a flat module then tensoring withMpreserves injectivity of linear maps. This lemma is fully universally polymorphic in all arguments, i.e.R,Mand linear mapsN → N'can all have different universe levels.Module.Flat.iff_rTensor_preserves_injective_linearMap: a module is flat iff tensoring modules in the higher universe preserves injectivity .Module.Flat.lTensor_exact: IfMis a flat module then tensoring withMis an exact functor. This lemma is fully universally polymorphic in all arguments, i.e.R,Mand linear mapsN → N' → N''can all have different universe levels.Module.Flat.iff_lTensor_exact: a module is flat iff tensoring modules in the higher universe is an exact functor.
TODO #
- Generalize flatness to noncommutative semirings.
Flatness over a semiring #
An R-module M is flat if for every finitely generated submodule N of every
finitely generated R-module P in the same universe as R,
the canonical map N ⊗ M → P ⊗ M is injective. This implies the same is true for
arbitrary R-modules N and P and injective linear maps N →ₗ[R] P, see
Flat.rTensor_preserves_injective_linearMap. To show a module over a ring R is flat, it
suffices to consider the case P = R, see Flat.iff_rTensor_injective.
- out ⦃P : Type u⦄ [AddCommMonoid P] [Module R P] [Module.Finite R P] (N : Submodule R P) : N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
Instances
If M is a flat module, then f ⊗ 𝟙 M is injective for all injective linear maps f.
If M is a flat module, then 𝟙 M ⊗ f is injective for all injective linear maps f.
M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map
in a universe that R fits in.
M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map
in a universe that R fits in.
An easier-to-use version of Module.flat_iff, with finiteness conditions removed.
A retract of a flat R-module is flat.
A R-module linearly equivalent to a flat R-module is flat.
If an R-module M is linearly equivalent to another R-module N, then M is flat
if and only if N is flat.
A direct sum of flat R-modules is flat.
Free R-modules over discrete types are flat.
Alias of Module.Flat.of_projective.
Flatness over a ring #
M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map.
See Module.Flat.iff_rTensor_preserves_injective_linearMap to specialize the universe of
N, N', N'' to Type (max u v).
M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map.
See Module.Flat.iff_rTensor_preserves_injective_linearMap' to generalize the universe of
N, N', N'' to any universe that is higher than R and M.
M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map.
See Module.Flat.iff_lTensor_preserves_injective_linearMap to specialize the universe of
N, N', N'' to Type (max u v).
M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map.
See Module.Flat.iff_lTensor_preserves_injective_linearMap' to generalize the universe of
N, N', N'' to any universe that is higher than R and M.
Define the character module of M to be M →+ ℚ ⧸ ℤ.
The character module of M is an injective module if and only if
f ⊗ 𝟙 M is injective for any linear map f in the same universe as M.
CharacterModule M is an injective module iff M is flat.
See [Lambek_1964] for a self-contained proof.
CharacterModule M is Baer iff M is flat.
An R-module M is flat iff for all ideals I of R, the tensor product of the
inclusion I → R and the identity M → M is injective. See iff_rTensor_injective to
restrict to finitely generated ideals I.
The lTensor-variant of iff_rTensor_injective'. .
A module M over a ring R is flat iff for all finitely generated ideals I of R, the
tensor product of the inclusion I → R and the identity M → M is injective. See
iff_rTensor_injective' to extend to all ideals I.
The lTensor-variant of iff_rTensor_injective.
An R-module M is flat if for all finitely generated ideals I of R,
the canonical map I ⊗ M →ₗ M is injective.
If M is flat then M ⊗ - is an exact functor.
If M is flat then - ⊗ M is an exact functor.
M is flat if and only if M ⊗ - is an exact functor. See
Module.Flat.iff_lTensor_exact to specialize the universe of N, N', N'' to Type (max u v).
M is flat if and only if M ⊗ - is an exact functor.
See Module.Flat.iff_lTensor_exact' to generalize the universe of
N, N', N'' to any universe that is higher than R and M.
M is flat if and only if - ⊗ M is an exact functor. See
Module.Flat.iff_rTensor_exact to specialize the universe of N, N', N'' to Type (max u v).
M is flat if and only if - ⊗ M is an exact functor.
See Module.Flat.iff_rTensor_exact' to generalize the universe of
N, N', N'' to any universe that is higher than R and M.
If M, N are R-modules, there exists an injective R-linear map from R to N,
and M is a nontrivial flat R-module, then M ⊗[R] N is nontrivial.
If M, N are R-modules, there exists an injective R-linear map from R to M,
and N is a nontrivial flat R-module, then M ⊗[R] N is nontrivial.
Tensor product of injective maps are injective under some flatness conditions.
Also see TensorProduct.map_injective_of_flat_flat' and
TensorProduct.map_injective_of_flat_flat_of_isDomain for different flatness conditions.
Tensor product of injective maps are injective under some flatness conditions.
Also see TensorProduct.map_injective_of_flat_flat and
TensorProduct.map_injective_of_flat_flat_of_isDomain for different flatness conditions.
Tensor product of linearly independent families is linearly independent under some flatness conditions.
The flatness condition could be removed over domains.
See LinearIndependent.tmul_of_isDomain.
Tensor product of linearly independent families is linearly independent under some flatness conditions.
The flatness condition could be removed over domains.
See LinearIndepOn.tmul_of_isDomain.
Tensor product of linearly independent families is linearly independent under some flatness conditions.
The flatness condition could be removed over domains.
See LinearIndependent.tmul_of_isDomain.
Tensor product of linearly independent families is linearly independent under some flatness conditions.
The flatness condition could be removed over domains.
See LinearIndepOn.tmul_of_isDomain.
If p and q are submodules of M and N respectively, and M and q are flat,
then p ⊗ q → M ⊗ N is injective.
If p and q are submodules of M and N respectively, and N and p are flat,
then p ⊗ q → M ⊗ N is injective.
If A, B are R-algebras, R injects into B,
and A is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.
If A, B are R-algebras, R injects into A,
and B is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.