English
Flatness over R is equivalent to the condition that for all P, N, N', the map N'.subtype.rTensor M is injective.
Русский
Плоскость над R эквивалентна условию: для всех P,N,N' отображение N'.subtype.rTensor M инъективно.
LaTeX
$$Flat R M ↔ ∀ ⦃P⦄ [AddCommMonoid P] [Module R P] (N : Submodule R P), Injective (N.subtype.rTensor M)$$
Lean4
/-- `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 iff_rTensor_preserves_injective_linearMapₛ [Small.{v'} R] :
Flat R M ↔
∀ ⦃N N' : Type v'⦄ [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (f : N →ₗ[R] N'),
Function.Injective f → Function.Injective (f.rTensor M) :=
⟨by introv _; apply rTensor_preserves_injective_linearMap, fun h ↦
⟨fun P _ _ _ _ _ ↦ by
have := Finite.small.{v'} R P
rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv R P).symm]
exact h _ Subtype.val_injective⟩⟩
