English
If R is a ring and M is an R-module with FaithfullyFlat structure, then for any nontrivial N, N ⊗_R M is nontrivial.
Русский
Если R кольцо и M — модуль над R с полезной структурой FaithfullyFlat, то для любого не тривиального N тензорное произведение не тривиально.
LaTeX
$$Nontrivial (N ⊗_R M) for Nontrivial N$$
Lean4
instance rTensor_nontrivial [fl : FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N] [Nontrivial N] :
Nontrivial (N ⊗[R] M) :=
by
obtain ⟨n, hn⟩ := nontrivial_iff_exists_ne (0 : N) |>.1 inferInstance
let I := (Submodule.span R { n }).annihilator
by_cases I_ne_top : I = ⊤
· rw [Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul] at I_ne_top
contradiction
let inc : R ⧸ I →ₗ[R] N :=
Submodule.liftQ _ ((LinearMap.lsmul R N).flip n) <| fun r hr => by
simpa only [LinearMap.mem_ker, LinearMap.flip_apply, LinearMap.lsmul_apply,
Submodule.mem_annihilator_span_singleton, I] using hr
have injective_inc : Function.Injective inc :=
LinearMap.ker_eq_bot.1 <|
eq_bot_iff.2 <| by
intro r hr
induction r using Quotient.inductionOn' with
| h r =>
simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply, LinearMap.flip_apply,
LinearMap.lsmul_apply, I, inc] using hr
have ne_top := iff_flat_and_proper_ideal R M |>.1 fl |>.2 I I_ne_top
refine subsingleton_or_nontrivial _ |>.resolve_left fun rid => ?_
exact
False.elim <|
ne_top <|
Submodule.subsingleton_quotient_iff_eq_top.1 <|
Function.Injective.comp (g := LinearMap.rTensor M inc)
(fl.toFlat.rTensor_preserves_injective_linearMap inc injective_inc)
((quotTensorEquivQuotSMul M I).symm.injective) |>.subsingleton
