English
A technical identity relating a basis of a free module over R, a finitely supported S-valued function, and a fixed element x ∈ S; it expresses how a certain tensor product sum can be rewritten in terms of a refined double sum using the basis coefficients.
Русский
Техническое тождество, связывающее базис свободного модуля над R, удобно ограниченную по поддержке функцию со значениями в S и фиксированный элемент x ∈ S; выражает преобразование тензорного произведения в двойную сумму через коэффициенты базиса.
LaTeX
$$$(1 \\otimes_R x) \\cdot \\sum_i f_i \\otimes b_i = \\sum_k \\sum_j c_{j,k} \\; b_j \\otimes b_k$, где $f: I \\to S$ имеет конечную опору и $b$ — база модуля, а $c_{j,k}$ задаются через представления $f$ и $a$ с опорой (детали в доказательстве).$$
Lean4
theorem finite_of_free_aux (I) [DecidableEq I] (b : Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R)
(ha : a = fun i ↦ b.repr (b i * x)) :
(1 ⊗ₜ[R] x * Finsupp.sum f fun i y ↦ y ⊗ₜ[R] b i) =
Finset.sum (f.support.biUnion fun i ↦ (a i).support) fun k ↦
Finsupp.sum (b.repr (f.sum fun i y ↦ a i k • y)) fun j c ↦ c • b j ⊗ₜ[R] b k :=
by
rw [Finsupp.sum, Finset.mul_sum]
subst ha
let a i := b.repr (b i * x)
conv_lhs =>
simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from fun _ ↦ b.linearCombination_repr _]
conv_lhs =>
simp only [Finsupp.linearCombination, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq,
Finsupp.sum, TensorProduct.tmul_sum, ← TensorProduct.smul_tmul]
have h₁ :
∀ k,
(Finsupp.sum (Finsupp.sum f fun i y ↦ a i k • b.repr y) fun j z ↦ z • b j ⊗ₜ[R] b k) =
(f.sum fun i y ↦ (b.repr y).sum fun j z ↦ a i k • z • b j ⊗ₜ[R] b k) :=
by
intro i
rw [Finsupp.sum_sum_index]
congr
ext j s
rw [Finsupp.sum_smul_index]
simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]
· intro; simp only [zero_smul]
· intro; simp only [zero_smul]
· intros; simp only [add_smul]
have h₂ : ∀ (x : S), ((b.repr x).support.sum fun a ↦ b.repr x a • b a) = x := by
simpa only [Finsupp.linearCombination_apply, Finsupp.sum] using b.linearCombination_repr
simp only [a] at h₁
simp_rw [map_finsuppSum, map_smul, h₁, Finsupp.sum, Finset.sum_comm (t := f.support), TensorProduct.smul_tmul', ←
TensorProduct.sum_tmul, ← Finset.smul_sum, h₂]
apply Finset.sum_congr rfl
intro i hi
apply Finset.sum_subset_zero_on_sdiff
· exact Finset.subset_biUnion_of_mem (fun i ↦ (a i).support) hi
· simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not, and_imp,
forall_exists_index]
simp +contextual
· exact fun _ _ ↦ rfl
