English
Let A ⊆ S be a finitely generated subalgebra over R, and let t, t' be elements of A ⊗R N such that rTensor_N A⋅toLinearMap t = rTensor_N A⋅toLinearMap t'. Then there exists a subalgebra B of S with A ≤ B and B FG, such that after passing to B via inclusion, t and t' give the same tensor.
Русский
Пусть A — FG-подалгебра S над R, а t, t' ∈ A ⊗R N удовлетворяют равенству after rTensor для A. Тогда существует подалгебра B ⊇ A с свойством FG, для которого после включения тензоризованный образ t и t' совпадают.
LaTeX
$$$\exists B \,(hAB : A \le B) (hB : Subalgebra.FG B) \land\ rTensor N (Subalgebra.inclusion hAB)\,t = rTensor N (Subalgebra.inclusion hAB)\,t',\text{ where } hAB \text{ is such that } A \le B.$$$
Lean4
theorem eq_of_fg_of_subtype_eq (h : rTensor N A.val.toLinearMap t = rTensor N A.val.toLinearMap t') :
∃ (B : Subalgebra R S) (hAB : A ≤ B),
Subalgebra.FG B ∧
rTensor N (Subalgebra.inclusion hAB).toLinearMap t =
LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap t' :=
by
classical
let ⟨P, hP, u, hu⟩ := TensorProduct.exists_of_fg t
let ⟨P', hP', u', hu'⟩ := TensorProduct.exists_of_fg t'
let P₁ := Submodule.map A.toSubmodule.subtype (P ⊔ P')
have hP₁ : Submodule.FG P₁ :=
Submodule.FG.map _
(Submodule.FG.sup hP hP')
-- the embeddings from P and P' to P₁
let j : P →ₗ[R] P₁ :=
(Subalgebra.toSubmodule A).subtype.restrict
(fun p hp ↦ by
simp only [coe_subtype, Submodule.map_sup, P₁]
exact Submodule.mem_sup_left ⟨p, hp, rfl⟩)
let j' : P' →ₗ[R] P₁ :=
(Subalgebra.toSubmodule A).subtype.restrict
(fun p hp ↦ by
simp only [coe_subtype, Submodule.map_sup, P₁]
exact Submodule.mem_sup_right ⟨p, hp, rfl⟩)
-- we map u and u' to P₁ ⊗[R] N, getting u₁ and u'₁
set u₁ := rTensor N j u with hu₁
set u'₁ := rTensor N j' u' with hu'₁
have : rTensor N P₁.subtype u₁ = rTensor N P₁.subtype u'₁ :=
by
rw [hu₁, hu'₁]
simp only [← comp_apply, ← rTensor_comp]
have hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype := rfl
have hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype := rfl
rw [hj₁, hj'₁]
simp only [rTensor_comp, comp_apply]
rw [hu, hu', h]
let ⟨P'₁, hP₁_le, hP'₁, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq hP₁ this
let ⟨s, hs⟩ := hP'₁
let ⟨w, hw⟩ := hA
let B := Algebra.adjoin R ((s ∪ w : Finset S) : Set S)
have hBA : A ≤ B := by
simp only [B, ← hw]
apply Algebra.adjoin_mono
simp only [Finset.coe_union, Set.subset_union_right]
use B, hBA, Subalgebra.fg_adjoin_finset _
rw [← hu, ← hu']
simp only [← comp_apply, ← rTensor_comp]
have hP'₁_le : P'₁ ≤ B.toSubmodule :=
by
simp only [← hs, Finset.coe_union, Submodule.span_le, Subalgebra.coe_toSubmodule, B]
exact subset_trans Set.subset_union_left Algebra.subset_adjoin
have k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j := by ext;
rfl
have k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j' := by
ext; rfl
rw [k, k']
simp only [rTensor_comp, comp_apply]
rw [← hu₁, ← hu'₁, h]
