Documentation

Mathlib.RingTheory.Flat.Basic

Flat modules #

A module M over a commutative ring R is flat if for all finitely generated ideals I of R, the canonical map I ⊗ M →ₗ M is injective.

This is equivalent to the claim that for all injective R-linear maps f : M₁ → M₂ the induced map M₁ ⊗ M → M₂ ⊗ M is injective. See https://stacks.math.columbia.edu/tag/00HD.

Main declaration #

Main theorems #

Implementation notes #

In Module.Flat.iff_rTensor_preserves_injective_linearMap, we require that the universe level of the ring is lower than or equal to that of the module. This requirement is to make sure ideals of the ring can be lifted to the universe of the module. It is unclear if this lemma also holds when the module lives in a lower universe.

TODO #

theorem Module.flat_iff (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] :
class Module.Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] :

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

Instances
    theorem Module.Flat.out {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [self : Module.Flat R M] ⦃I : Ideal R :
    instance Module.Flat.self (R : Type u) [CommRing R] :
    Equations
    • =

    An R-module M 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. -

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

    @[deprecated LinearMap.lTensor_inj_iff_rTensor_inj]

    Alias of LinearMap.lTensor_inj_iff_rTensor_inj.


    Given a linear map f : N → P, f ⊗ M is injective if and only if M ⊗ f is injective.

    The lTensor-variant of iff_rTensor_injective. .

    theorem Module.Flat.of_retract (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [f : Module.Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r ∘ₗ i = LinearMap.id) :

    A retract of a flat R-module is flat.

    theorem Module.Flat.of_linearEquiv (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (N : Type w) [AddCommGroup N] [Module R N] [f : Module.Flat R M] (e : N ≃ₗ[R] M) :

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

    instance Module.Flat.directSum (R : Type u) [CommRing R] (ι : Type v) (M : ιType w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [F : ∀ (i : ι), Module.Flat R (M i)] :
    Module.Flat R (DirectSum ι fun (i : ι) => M i)

    A direct sum of flat R-modules is flat.

    Equations
    • =
    instance Module.Flat.finsupp (R : Type u) [CommRing R] (ι : Type v) :

    Free R-modules over discrete types are flat.

    Equations
    • =
    instance Module.Flat.of_free (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] :
    Equations
    • =
    theorem Module.Flat.of_projective_surjective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (ι : Type w) [Module.Projective R M] (p : (ι →₀ R) →ₗ[R] M) (hp : Function.Surjective p) :

    A projective module with a discrete type of generator is flat

    instance Module.Flat.of_projective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [h : Module.Projective R M] :
    Equations
    • =
    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'] (L : N →ₗ[R] N'), Function.Injective LFunction.Injective (LinearMap.rTensor M L)

    Define the character module of M to be M →+ ℚ ⧸ ℤ. The character module of M is an injective module if and only if L ⊗ 𝟙 M is injective for any linear map L in the same universe as M.

    CharacterModule M is an injective module iff M is flat.

    theorem Module.Flat.rTensor_preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [h : Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective L) :

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

    @[deprecated Module.Flat.rTensor_preserves_injective_linearMap]
    theorem Module.Flat.preserves_injective_linearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [h : Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective L) :

    Alias of Module.Flat.rTensor_preserves_injective_linearMap.


    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} [CommRing R] [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module.Flat R M] (L : N →ₗ[R] N') (hL : Function.Injective L) :

    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) [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'] (L : N →ₗ[R] N'), Function.Injective LFunction.Injective (LinearMap.rTensor M L)

    M is flat if and only if f ⊗ 𝟙 M is injective whenever f is an injective linear map.

    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'] (L : N →ₗ[R] N'), Function.Injective LFunction.Injective (LinearMap.lTensor M L)

    M is flat if and only if 𝟙 M ⊗ f is injective whenever f is an injective linear map.

    theorem Module.Flat.lTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] [flat : Module.Flat R M] ⦃N : Type v⦄ ⦃N' : Type v⦄ ⦃N'' : Type v⦄ [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) :
    theorem Module.Flat.rTensor_exact {R : Type u} (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v, u} R] [flat : Module.Flat R M] ⦃N : Type v⦄ ⦃N' : Type v⦄ ⦃N'' : Type v⦄ [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) :
    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 gFunction.Exact (LinearMap.lTensor M f) (LinearMap.lTensor M g)

    M is flat if and only if M ⊗ - is a left exact functor.

    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 gFunction.Exact (LinearMap.rTensor M f) (LinearMap.rTensor M g)

    M is flat if and only if - ⊗ M is a left exact functor.