English
A variant of the previous equivalence for rTensor with primed formulation.
Русский
Вариант эквивалентности через rTensor с другой формулировкой.
LaTeX
$$$Flat\ R\ M \iff \forall {N} {N'} (f:\ N \to N') , Injective(f) \Rightarrow Injective(f\mathrm{rTensor} M)$$$
Lean4
/-- `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 iff_rTensor_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.rTensor M) (g.rTensor M) :=
by
refine
⟨fun _ ↦ rTensor_exact _, fun H ↦
iff_rTensor_preserves_injective_linearMap'.mpr fun N' N'' _ _ _ _ f hf ↦
LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr fun x (hx : _ = 0) ↦ ?_⟩
simpa [Eq.comm] using
@H PUnit N' N'' _ _ _ _ _ _ 0 f
(fun x ↦ by
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
exact (f.map_eq_zero_iff hf).trans eq_comm)
x |>.mp
hx
