English
A more general tensor product flatness result with a scalar tower, leading to flatness of the tensor product over S.
Русский
Обобщенный результат плоскостности тензорного произведения через башню скаляров; плоскостность тензорного произведения над S.
LaTeX
$$$\forall S\, [\text{CommSemiring } S] [\text{Algebra } R S] [\text{Module } S M] [\text{IsScalarTower } R S M] [\text{Flat } S M] [\text{Flat } R N],\flat S( M \otimes_R N)$$$
Lean4
/-- `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 iff_lTensor_exact' [Small.{v'} R] :
Flat R M ↔
∀ ⦃N N' 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''⦄,
Function.Exact f g → Function.Exact (f.lTensor M) (g.lTensor M) :=
by
refine
⟨fun _ ↦ lTensor_exact _, fun H ↦
iff_lTensor_preserves_injective_linearMap'.mpr fun N' N'' _ _ _ _ L hL ↦
LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr fun x (hx : _ = 0) ↦ ?_⟩
simpa [Eq.comm] using
@H PUnit N' N'' _ _ _ _ _ _ 0 L
(fun x ↦ by
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
exact (L.map_eq_zero_iff hL).trans eq_comm)
x |>.mp
hx
