mathlib documentation

ring_theory.flat

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. This result is not yet formalised.

Main declaration #

TODO #

@[class]
structure module.flat (R : Type u_1) (M : Type (max u_2 u_3)) [comm_ring R] [add_comm_group M] [module R M] :
Prop

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

Instances
@[instance]
def module.flat.self (R : Type (max u_1 u_2)) [comm_ring R] :