English
In a setting with a nontrivial base, linear independence of a family over S implies linear independence over R after an injective transfer of scalars, under suitable tower conditions.
Русский
Если основание не тривиально, линейная независимость семейства над S поднимается на R через инъективное перемещение скалярных полей в соответствующей башне.
LaTeX
$$$\\text{LinearIndependent}_{K}(f\\circ b)$ given $\\text{LinearIndependent}_{S}(b)$ and appropriate tower conditions$$
Lean4
/-- Let `V` be a vector space over `K = Frac(R)`, `S / R` a ring extension
and `V'` a module over `S`. If `b`, in the intersection `V''` of `V` and `V'`,
is linear independent over `S` in `V'`, then it is linear independent over `R` in `V`.
The statement we prove is actually slightly more general:
* it suffices that the inclusion `algebraMap R S : R → S` is nontrivial
* the function `f' : V'' → V'` doesn't need to be injective
-/
theorem linearIndependent_of_nontrivial [IsDedekindDomain R] (hRS : RingHom.ker (algebraMap R S) ≠ ⊤) (f : V'' →ₗ[R] V)
(hf : Function.Injective f) (f' : V'' →ₗ[R] V') {ι : Type*} {b : ι → V''} (hb' : LinearIndependent S (f' ∘ b)) :
LinearIndependent K (f ∘ b) := by
contrapose! hb' with hb
simp only [linearIndependent_iff', not_forall] at hb ⊢
obtain ⟨s, g, eq, j', hj's, hj'g⟩ := hb
use s
obtain ⟨a, hag, j, hjs, hgI⟩ := Ideal.exist_integer_multiples_notMem hRS s g hj's hj'g
choose g'' hg'' using hag
letI := Classical.propDecidable
let g' i := if h : i ∈ s then g'' i h else 0
have hg' : ∀ i ∈ s, algebraMap _ _ (g' i) = a * g i := by intro i hi;
exact
(congr_arg _ (dif_pos hi)).trans
(hg'' i hi)
-- Because `R/I` is nontrivial, we can lift `g` to a nontrivial linear dependence in `S`.
have hgI : algebraMap R S (g' j) ≠ 0 :=
by
simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI
exact hgI _ (hg' j hjs)
refine ⟨fun i => algebraMap R S (g' i), ?_, j, hjs, hgI⟩
have eq : f (∑ i ∈ s, g' i • b i) = 0 :=
by
rw [map_sum, ← smul_zero a, ← eq, Finset.smul_sum]
refine Finset.sum_congr rfl ?_
intro i hi
rw [LinearMap.map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc, smul_eq_mul, Function.comp_apply]
simp only [IsScalarTower.algebraMap_smul, ← map_smul, ← map_sum, (f.map_eq_zero_iff hf).mp eq, LinearMap.map_zero,
(· ∘ ·)]
