English
If M has a finite presentation and certain tensorial maps are injective, then there exists a basis of M compatible with a given generating family via a base-change process.
Русский
Если M имеет конечную презентацию и определенные тензорные отображения инъективны, существует база M, совместимая с заданным породящим семейством через процесс базового изменения.
LaTeX
$$$ \exists \kappa \; \exists (a: \kappa \to \iota) \; \exists (b: Basis \kappa R M),\; \forall i, b i = v i. $$$
Lean4
/-- If `M` is of finite presentation over a local ring `(R, 𝔪, k)` such that
`𝔪 ⊗ M → M` is injective, then every family of elements that is a `k`-basis of
`k ⊗ M` is an `R`-basis of `M`. -/
theorem exists_basis_of_basis_baseChange [Module.FinitePresentation R M] {ι : Type*} (v : ι → M)
(hli : LinearIndependent k (TensorProduct.mk R k M 1 ∘ v))
(hsp : Submodule.span k (Set.range (TensorProduct.mk R k M 1 ∘ v)) = ⊤)
(H : Function.Injective ((𝔪).subtype.rTensor M)) : ∃ (b : Basis ι R M), ∀ i, b i = v i :=
by
let bk : Basis ι k (k ⊗[R] M) := Basis.mk hli (by rw [hsp])
haveI : Finite ι := Module.Finite.finite_basis bk
letI : Fintype ι := Fintype.ofFinite ι
let i := Finsupp.linearCombination R v
have hi : Surjective i := by
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
refine IsLocalRing.span_eq_top_of_tmul_eq_basis (R := R) (f := v) bk (fun _ ↦ by simp [bk])
have : Module.Finite R (LinearMap.ker i) := by
constructor
exact
(Submodule.fg_top _).mpr
(Module.FinitePresentation.fg_ker i hi)
-- We claim that `i` is actually a bijection,
-- hence `v` induces an isomorphism `M ≃[R] Rᴵ` showing that `v` is a basis.
let iequiv : (ι →₀ R) ≃ₗ[R] M :=
by
refine
LinearEquiv.ofBijective i
⟨?_, hi⟩
-- By Nakayama's lemma, it suffices to show that `k ⊗ ker(i) = 0`.
rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot, ← IsLocalRing.subsingleton_tensorProduct (R := R),
subsingleton_iff_forall_eq 0]
have : Function.Surjective (i.baseChange k) := i.lTensor_surjective _ hi
have hi' : Function.Bijective (i.baseChange k) :=
by
refine ⟨?_, this⟩
rw [← LinearMap.ker_eq_bot (M := k ⊗[R] (ι →₀ R)) (f := i.baseChange k), ←
Submodule.finrank_eq_zero (R := k) (M := k ⊗[R] (ι →₀ R)), ←
Nat.add_right_inj (n := Module.finrank k (LinearMap.range <| i.baseChange k)),
LinearMap.finrank_range_add_finrank_ker (V := k ⊗[R] (ι →₀ R)), LinearMap.range_eq_top.mpr this, finrank_top]
simp only [Module.finrank_tensorProduct, Module.finrank_self, Module.finrank_finsupp_self, one_mul, add_zero]
rw [Module.finrank_eq_card_basis bk]
-- On the other hand, `m ⊗ M → M` injective => `Tor₁(k, M) = 0` => `k ⊗ ker(i) → kᴵ` injective.
intro x
refine
lTensor_injective_of_exact_of_exact_of_rTensor_injective (N₁ := LinearMap.ker i) (N₂ := ι →₀ R) (N₃ := M) (f₁ :=
(𝔪).subtype) (f₂ := Submodule.mkQ 𝔪) (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪)
(Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_
· apply Module.Flat.lTensor_preserves_injective_linearMap
exact Subtype.val_injective
· apply hi'.injective
rw [LinearMap.baseChange_eq_ltensor]
erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp]
rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]
simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero]
use Basis.ofRepr iequiv.symm
intro j
simp [iequiv, i]
