English
If R,S satisfy the hypotheses, then the unramified property provides instances yielding finite modules after base change and various separability properties.
Русский
Если R,S удовлетворяют гипотезам, то свойство неразветвленности обеспечивает инстанции, дающие модульность над базой и раздельность.
LaTeX
$$$[FormallyUnramified R S] \\Rightarrow [EssFiniteType R S] \\Rightarrow [Module.Finite (ResidueField R) (ResidueField S)]$$$
Lean4
/-- An unramified free algebra is finitely generated. Iversen I.2.8 -/
theorem finite_of_free [Module.Free R S] : Module.Finite R S := by
classical
let I := Module.Free.ChooseBasisIndex R S
let b : Basis I R S := Module.Free.chooseBasis R S
have ⟨f, hf⟩ : ∃ (a : I →₀ S), elem R S = a.sum (fun i x ↦ x ⊗ₜ b i) :=
by
let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
use b'.repr (elem R S)
conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
congr! with _ i x
simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']
constructor
-- I claim that `{ fᵢbⱼ | i, j ∈ s }` spans `S` over `R`.
use Finset.image₂ (fun i j ↦ f i * b j) f.support f.support
rw [← top_le_iff]
-- For all `x : S`, let `bᵢx = ∑ aᵢⱼbⱼ`.
rintro x -
let a : I → I →₀ R := fun i ↦
b.repr
(b i * x)
-- Consider `F` such that `fⱼx = ∑ Fᵢⱼbⱼ`.
let F : I →₀ I →₀ R :=
Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j))
(fun j ↦ not_imp_comm.mp fun hj ↦ by simp [Finsupp.notMem_support_iff.mp hj])
have hG : ∀ j ∉ (Finset.biUnion f.support fun i ↦ (a i).support), b.repr (f.sum (fun i y ↦ a i j • y)) = 0 :=
by
intro j hj
simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and, not_not] at hj
simp only [Finsupp.sum]
trans b.repr (f.support.sum (fun _ ↦ 0))
· refine congr_arg b.repr (Finset.sum_congr rfl ?_)
simp only [Finsupp.mem_support_iff]
intro i hi
rw [hj i hi, zero_smul]
·
simp only [Finset.sum_const_zero, map_zero]
-- And `G` such that `∑ₛ aᵢⱼfᵢ = ∑ Gᵢⱼbⱼ`, where `aᵢⱼ` are the coefficients `bᵢx = ∑ aᵢⱼbⱼ`.
let G : I →₀ I →₀ R :=
Finsupp.onFinset (Finset.biUnion f.support (fun i ↦ (a i).support)) (fun j ↦ b.repr (f.sum (fun i y ↦ a i j • y)))
(fun j ↦ not_imp_comm.mp (hG j))
-- Then `∑ Fᵢⱼ(bⱼ ⊗ bᵢ) = ∑ fⱼx ⊗ bᵢ = ∑ fⱼ ⊗ xbᵢ = ∑ aᵢⱼ(fⱼ ⊗ bᵢ) = ∑ Gᵢⱼ(bⱼ ⊗ bᵢ)`.
-- Since `bⱼ ⊗ bᵢ` forms an `R`-basis of `S ⊗ S`, we conclude that `F = G`.
have : F = G := by
apply Finsupp.finsuppProdEquiv.symm.injective
apply (Finsupp.equivCongrLeft (Equiv.prodComm I I)).injective
apply (b.tensorProduct b).repr.symm.injective
suffices (F.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) = G.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a
by simpa [Finsupp.linearCombination_apply, Finsupp.sum_uncurry_index]
rw [Finsupp.onFinset_sum, Finsupp.onFinset_sum]
have : ∀ i, ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i :=
by
intro i
simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]
congr 1
exact b.linearCombination_repr _
trans (x ⊗ₜ 1) * elem R S
· simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_mul]
· rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
rfl
· intro; simp
· intro;
simp
-- In particular, `fⱼx = ∑ Fᵢⱼbⱼ = ∑ Gᵢⱼbⱼ = ∑ₛ aᵢⱼfᵢ` for all `j`.
have : ∀ j, x * f j = f.sum fun i y ↦ a i j • y := by
intro j
apply b.repr.injective
exact DFunLike.congr_fun this j
rw [← mul_one x, ← @lmul_elem R, hf, map_finsuppSum, Finsupp.sum, Finset.mul_sum]
simp only [TensorProduct.lmul'_apply_tmul, Finset.coe_image₂, ← mul_assoc, this, Finsupp.sum, Finset.sum_mul,
smul_mul_assoc]
apply Submodule.sum_mem; intro i hi
apply Submodule.sum_mem; intro j hj
apply Submodule.smul_mem
apply Submodule.subset_span
use j, hj, i, hi
