Documentation

Mathlib.RingTheory.Flat.Basic

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 an R-module M is flat.

Main theorems #

Module.Flat.of_retract: retracts of flat modules are flat
Module.Flat.of_linearEquiv: modules linearly equivalent to a flat modules are flat
Module.Flat.directSum: arbitrary direct sums of flat modules are flat
Module.Flat.of_free: free modules are flat
Module.Flat.of_projective: projective modules are flat
Module.Flat.preserves_injective_linearMap: If M is a flat module then tensoring with M preserves injectivity of linear maps. This lemma is fully universally polymorphic in all arguments, i.e. R, M and linear maps N → 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: If M is a flat module then tensoring with M is an exact functor. This lemma is fully universally polymorphic in all arguments, i.e. R, M and linear maps N → 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 #

theorem LinearMap.rTensor_injective_of_fg {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {f : N →ₗ[R] P} (h : ∀ (N' : Submodule R N) (P' : Submodule R P), N'.FG → P'.FG → ∀ (h : N' ≤ Submodule.comap f P'), Function.Injective ⇑(LinearMap.rTensor M (f.restrict h))) :

Function.Injective ⇑(LinearMap.rTensor M f)

theorem LinearMap.rTensor_injective_iff_subtype {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] {f : N →ₗ[R] P} (hf : Function.Injective ⇑f) (e : P ≃ₗ[R] Q) :

Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M (LinearMap.range (↑e ∘ₗ f)).subtype)

class Module.Flat (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :

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

theorem Module.flat_iff (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] [inst_2 : Module.Finite R P] (N : Submodule R P), N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)

theorem Module.Flat.rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module.Flat R M] (f : N →ₗ[R] P) (hf : Function.Injective ⇑f) :

Function.Injective ⇑(LinearMap.rTensor M f)

If M is a flat module, then f ⊗ 𝟙 M is injective for all injective linear maps f.

theorem Module.Flat.lTensor_preserves_injective_linearMap {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module.Flat R M] (f : N →ₗ[R] P) (hf : Function.Injective ⇑f) :

Function.Injective ⇑(LinearMap.lTensor M f)

If M is a flat module, then 𝟙 M ⊗ f is injective for all injective linear maps f.

theorem Module.Flat.iff_rTensor_preserves_injective_linearMapₛ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M 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.

theorem Module.Flat.iff_lTensor_preserves_injective_linearMapₛ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

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.

theorem Module.Flat.iff_rTensor_injectiveₛ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Function.Injective ⇑(LinearMap.rTensor M N.subtype)

An easier-to-use version of Module.flat_iff, with finiteness conditions removed.

theorem Module.Flat.iff_lTensor_injectiveₛ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Function.Injective ⇑(LinearMap.lTensor M N.subtype)

instance Module.Flat.instSubalgebraToSubmodule {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (A : Subalgebra R S) [Module.Flat R ↥A] :

Module.Flat R ↥(Subalgebra.toSubmodule A)

instance Module.Flat.self {R : Type u} [CommSemiring R] :

Module.Flat R R

theorem Module.Flat.of_retract {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [f : Module.Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r ∘ₗ i = LinearMap.id) :

Module.Flat R N

A retract of a flat R-module is flat.

theorem Module.Flat.of_linearEquiv {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Flat R M] (e : N ≃ₗ[R] M) :

Module.Flat R N

A R-module linearly equivalent to a flat R-module is flat.

theorem Module.Flat.equiv_iff {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

Module.Flat R M ↔ Module.Flat R N

If an R-module M is linearly equivalent to another R-module N, then M is flat if and only if N is flat.

instance Module.Flat.ulift {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Flat R M] :

Module.Flat R (ULift.{v', v} M)

theorem Module.Flat.of_ulift {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Flat R (ULift.{v', v} M)] :

Module.Flat R M

instance Module.Flat.shrink {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Small.{v', v} M] [Module.Flat R M] :

Module.Flat R (Shrink.{v', v} M)

theorem Module.Flat.of_shrink {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Small.{v', v} M] [Module.Flat R (Shrink.{v', v} M)] :

Module.Flat R M

theorem Module.Flat.directSum_iff {R : Type u} [CommSemiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :

Module.Flat R (DirectSum ι fun (i : ι) => M i) ↔ ∀ (i : ι), Module.Flat R (M i)

theorem Module.Flat.dfinsupp_iff {R : Type u} [CommSemiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :

Module.Flat R (Π₀ (i : ι), M i) ↔ ∀ (i : ι), Module.Flat R (M i)

instance Module.Flat.directSum {R : Type u} [CommSemiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Flat R (M i)] :

Module.Flat R (DirectSum ι fun (i : ι) => M i)

A direct sum of flat R-modules is flat.

instance Module.Flat.dfinsupp {R : Type u} [CommSemiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Flat R (M i)] :

Module.Flat R (Π₀ (i : ι), M i)

instance Module.Flat.finsupp {R : Type u} [CommSemiring R] (ι : Type v) :

Module.Flat R (ι →₀ R)

Free R-modules over discrete types are flat.

instance Module.Flat.of_projective {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Projective R M] :

Module.Flat R M

@[deprecated Module.Flat.of_projective (since := "2024-12-26")]

theorem Module.Flat.of_projective_surjective {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Projective R M] :

Module.Flat R M

Alias of Module.Flat.of_projective.

instance Module.Flat.of_free {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] :

Module.Flat R M

instance Module.Flat.instTensorProduct {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {S : Type u_4} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.Flat S M] [Module.Flat R N] :

Module.Flat S (TensorProduct R M N)

theorem Module.Flat.linearIndependent_one_tmul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Algebra R S] [Module.Flat R S] {ι : Type u_5} {v : ι → M} (hv : LinearIndependent R v) :

LinearIndependent S fun (x : ι) => 1 ⊗ₜ[R] v x

theorem Module.Flat.tensorProduct_mapIncl_injective_of_right {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (p : Submodule R M) (q : Submodule R N) [Module.Flat R M] [Module.Flat R ↥q] :

Function.Injective ⇑(TensorProduct.mapIncl p q)

If p and q are submodules of M and N respectively, and M and q are flat, then p ⊗ q → M ⊗ N is injective.

theorem Module.Flat.tensorProduct_mapIncl_injective_of_left {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (p : Submodule R M) (q : Submodule R N) [Module.Flat R ↥p] [Module.Flat R N] :

Function.Injective ⇑(TensorProduct.mapIncl p q)

If p and q are submodules of M and N respectively, and N and p are flat, then p ⊗ q → M ⊗ N is injective.

Flatness over a ring #

theorem Module.Flat.iff_rTensor_preserves_injective_linearMap' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

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

theorem Module.Flat.iff_rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

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.

theorem Module.Flat.iff_lTensor_preserves_injective_linearMap' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

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

theorem Module.Flat.iff_lTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

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.

theorem Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Injective R (CharacterModule M) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)

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.

theorem Module.Flat.iff_characterModule_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] :

Module.Flat R M ↔ Module.Injective R (CharacterModule M)

CharacterModule M is an injective module iff M is flat. See [Lambek_1964] for a self-contained proof.

theorem Module.Flat.iff_characterModule_baer {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ Module.Baer R (CharacterModule M)

CharacterModule M is Baer iff M is flat.

theorem Module.Flat.iff_rTensor_injective' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))

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

theorem Module.Flat.iff_lTensor_injective' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))

The lTensor-variant of iff_rTensor_injective'. .

theorem Module.Flat.iff_rTensor_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))

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.

theorem Module.Flat.iff_lTensor_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))

The lTensor-variant of iff_rTensor_injective.

theorem Module.Flat.iff_lift_lsmul_comp_subtype_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

An R-module M is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

theorem Module.Flat.lTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact ⇑f ⇑g) :

Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

If M is flat then M ⊗ - is an exact functor.

theorem Module.Flat.rTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact ⇑f ⇑g) :

Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

If M is flat then - ⊗ M is an exact functor.

theorem Module.Flat.iff_lTensor_exact' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

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

theorem Module.Flat.iff_lTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃N N' N'' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)

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.

theorem Module.Flat.iff_rTensor_exact' {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] :

Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

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

theorem Module.Flat.iff_rTensor_exact {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :

Module.Flat R M ↔ ∀ ⦃N N' N'' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

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.

theorem Algebra.TensorProduct.includeLeft_injective {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CommSemiring S] [Algebra S A] [SMulCommClass R S A] [Module.Flat R A] (hb : Function.Injective ⇑(algebraMap R B)) :

Function.Injective ⇑Algebra.TensorProduct.includeLeft

theorem Algebra.TensorProduct.includeRight_injective {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Module.Flat R B] (ha : Function.Injective ⇑(algebraMap R A)) :

Function.Injective ⇑Algebra.TensorProduct.includeRight

theorem TensorProduct.nontrivial_of_linearMap_injective_of_flat_left (R : Type u_1) [CommSemiring R] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : R →ₗ[R] N) (h : Function.Injective ⇑f) [Module.Flat R M] [Nontrivial M] :

Nontrivial (TensorProduct R M N)

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.

theorem TensorProduct.nontrivial_of_linearMap_injective_of_flat_right (R : Type u_1) [CommSemiring R] (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : R →ₗ[R] M) (h : Function.Injective ⇑f) [Module.Flat R N] [Nontrivial N] :

Nontrivial (TensorProduct R M N)

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.

theorem Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left (R : Type u_1) [CommSemiring R] (A : Type u_2) (B : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (h : Function.Injective ⇑(algebraMap R B)) [Module.Flat R A] [Nontrivial A] :

Nontrivial (TensorProduct R A B)

If A, B are R-algebras, R injects into B, and A is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.

theorem Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_right (R : Type u_1) [CommSemiring R] (A : Type u_2) (B : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (h : Function.Injective ⇑(algebraMap R A)) [Module.Flat R B] [Nontrivial B] :

Nontrivial (TensorProduct R A B)

If A, B are R-algebras, R injects into A, and B is a nontrivial flat R-algebra, then A ⊗[R] B is nontrivial.