English
If a flat module over a local ring satisfies certain conditions, then a family of vectors is linearly independent over the residue field implies independence over the base ring.
Русский
Если модуль над локальным кольцом удовлетворяет условиям, то множество векторов, линейно независимое над остаточным полем, линейно независимо над основанием.
LaTeX
$$$ \text{LinearIndependent}_k( v ) \Rightarrow \text{LinearIndependent}_R(v). $$$
Lean4
theorem linearIndependent_of_flat [Flat R M] {ι : Type u} (v : ι → M)
(h : LinearIndependent k (TensorProduct.mk R k M 1 ∘ v)) : LinearIndependent R v :=
by
rw [linearIndependent_iff']; intro s f hfv i hi
classical
induction s using Finset.induction generalizing v i with
| empty => exact (Finset.notMem_empty _ hi).elim
| insert n s hn ih => ?_
rw [← Finset.sum_coe_sort] at hfv
have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv
have : v n ∉ 𝔪 • (⊤ : Submodule R M) := by simpa only [← LinearMap.ker_tensorProductMk] using h.ne_zero n
set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def
obtain ⟨j, hj⟩ : ∃ j, IsUnit (a n j) := by
contrapose! this
rw [show v n = _ from hay n]
exact sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩
let a' (i : ι) : R := if hi : _ then a ⟨i, hi⟩ j else 0
have a_eq i : a i j = a' i.1 := by simp_rw [a', dif_pos i.2]
have hfn : f n = -(∑ i ∈ s, f i * a' i) * hj.unit⁻¹ :=
by
rw [← hj.mul_left_inj, mul_assoc, hj.val_inv_mul, mul_one, eq_neg_iff_add_eq_zero]
convert hfa j
simp_rw [a_eq, Finset.sum_coe_sort _ (fun i ↦ f i * a' i), s.sum_insert hn, n_def]
let c (i : ι) : R := -(if i = n then 0 else a' i) * hj.unit⁻¹
specialize ih (v + (c · • v n)) ?_ ?_
· convert (linearIndependent_add_smul_iff (c := Ideal.Quotient.mk _ ∘ c) (i := n.1) ?_).mpr h
· ext; simp [tmul_add]; rfl
simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
· rw [Finset.sum_coe_sort _ (fun i ↦ f i • v i), s.sum_insert hn, add_comm, hfn] at hfv
simp_rw [Pi.add_apply, smul_add, s.sum_add_distrib, c, smul_smul, ← s.sum_smul, ← mul_assoc, ← s.sum_mul, mul_neg,
s.sum_neg_distrib, ← hfv]
congr 4
exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]
obtain hi | hi := Finset.mem_insert.mp hi
· rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]
intro i hi; rw [ih i hi, zero_mul]
· exact ih i hi
