Finite modules over local rings #
This file gathers various results about finite modules over a local ring (R, 𝔪, k).
Main results #
IsLocalRing.subsingleton_tensorProduct: IfMis finitely generated,k ⊗ M = 0 ↔ M = 0.Module.free_of_maximalIdeal_rTensor_injective: IfMis a finitely presented module such thatm ⊗ M → Mis injective (for example whenMis flat), thenMis free.Module.free_of_lTensor_residueField_injective: IfN → M → P → 0is a presentation ofPwithNfinite andMfinite free, then injectivity ofk ⊗ N → k ⊗ Mimplies thatPis free.IsLocalRing.split_injective_iff_lTensor_residueField_injective: Given anR-linear mapl : M → NwithMfinite andNfinite free,lis a split injection if and only ifk ⊗ lis a (split) injection.
theorem
IsLocalRing.map_mkQ_eq
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N₁ N₂ : Submodule R M}
(h : N₁ ≤ N₂)
(h' : N₂.FG)
:
theorem
IsLocalRing.map_mkQ_eq_top
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N : Submodule R M}
[Module.Finite R M]
:
theorem
IsLocalRing.map_tensorProduct_mk_eq_top
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N : Submodule R M}
[Module.Finite R M]
:
theorem
IsLocalRing.subsingleton_tensorProduct
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[Module.Finite R M]
:
theorem
IsLocalRing.span_eq_top_of_tmul_eq_basis
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[Module.Finite R M]
{ι : Type u_3}
(f : ι → M)
(b : Basis ι (ResidueField R) (TensorProduct R (ResidueField R) M))
(hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i)
:
theorem
Module.mem_support_iff_nontrivial_residueField_tensorProduct
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
(p : PrimeSpectrum R)
:
@[deprecated IsLocalRing.map_mkQ_eq (since := "2024-11-11")]
theorem
LocalRing.map_mkQ_eq
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N₁ N₂ : Submodule R M}
(h : N₁ ≤ N₂)
(h' : N₂.FG)
:
Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₁ = Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₂ ↔ N₁ = N₂
Alias of IsLocalRing.map_mkQ_eq.
@[deprecated IsLocalRing.map_mkQ_eq_top (since := "2024-11-11")]
theorem
LocalRing.map_mkQ_eq_top
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N : Submodule R M}
[Module.Finite R M]
:
Alias of IsLocalRing.map_mkQ_eq_top.
@[deprecated IsLocalRing.map_tensorProduct_mk_eq_top (since := "2024-11-11")]
theorem
LocalRing.map_tensorProduct_mk_eq_top
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
{N : Submodule R M}
[Module.Finite R M]
:
Alias of IsLocalRing.map_tensorProduct_mk_eq_top.
@[deprecated IsLocalRing.subsingleton_tensorProduct (since := "2024-11-11")]
theorem
LocalRing.subsingleton_tensorProduct
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[Module.Finite R M]
:
Alias of IsLocalRing.subsingleton_tensorProduct.
@[deprecated IsLocalRing.span_eq_top_of_tmul_eq_basis (since := "2024-11-11")]
theorem
LocalRing.span_eq_top_of_tmul_eq_basis
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[Module.Finite R M]
{ι : Type u_3}
(f : ι → M)
(b : Basis ι (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) M))
(hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i)
:
Alias of IsLocalRing.span_eq_top_of_tmul_eq_basis.
theorem
lTensor_injective_of_exact_of_exact_of_rTensor_injective
{R : Type u_7}
[CommRing R]
{M₁ : Type u_1}
{M₂ : Type u_2}
{M₃ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_6}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
{f₁ : M₁ →ₗ[R] M₂}
{f₂ : M₂ →ₗ[R] M₃}
{g₁ : N₁ →ₗ[R] N₂}
{g₂ : N₂ →ₗ[R] N₃}
(hfexact : Function.Exact ⇑f₁ ⇑f₂)
(hfsurj : Function.Surjective ⇑f₂)
(hgexact : Function.Exact ⇑g₁ ⇑g₂)
(hgsurj : Function.Surjective ⇑g₂)
(hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁))
(hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁))
:
Function.Injective ⇑(LinearMap.lTensor M₃ g₁)
Given M₁ → M₂ → M₃ → 0 and N₁ → N₂ → N₃ → 0,
if M₁ ⊗ N₃ → M₂ ⊗ N₃ and M₂ ⊗ N₁ → M₂ ⊗ N₂ are both injective,
then M₃ ⊗ N₁ → M₃ ⊗ N₂ is also injective.
theorem
Module.exists_basis_of_basis_baseChange
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[FinitePresentation R M]
{ι : Type u}
(v : ι → M)
(hli : LinearIndependent (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v))
(hsp :
Submodule.span (IsLocalRing.ResidueField R)
(Set.range (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v)) = ⊤)
(H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))))
:
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
Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[FinitePresentation R M]
(H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))))
{ι : Type u}
(v : ι → M)
(hv : Submodule.span R (Set.range v) = ⊤)
:
If M is a finitely presented module over a local ring (R, 𝔪) such that m ⊗ M → M is
injective, then every generating family contains a basis.
theorem
Module.exists_basis_of_span_of_flat
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[FinitePresentation R M]
[Flat R M]
{ι : Type u}
(v : ι → M)
(hv : Submodule.span R (Set.range v) = ⊤)
:
theorem
Module.free_of_maximalIdeal_rTensor_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[FinitePresentation R M]
(H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))))
:
Free R M
If M is a finitely presented module over a local ring (R, 𝔪) such that m ⊗ M → M is
injective, then M is free.
theorem
Module.IsLocalRing.linearIndependent_of_flat
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
[IsLocalRing R]
[Flat R M]
{ι : Type u}
(v : ι → M)
(h : LinearIndependent (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v))
:
theorem
Module.free_of_flat_of_isLocalRing
{R : Type u_1}
[CommRing R]
{P : Type u_2}
[AddCommGroup P]
[Module R P]
[IsLocalRing R]
[Module.Finite R P]
[Flat R P]
:
Free R P
@[deprecated Module.free_of_flat_of_isLocalRing (since := "2024-11-12")]
theorem
Module.free_of_flat_of_localRing
{R : Type u_1}
[CommRing R]
{P : Type u_2}
[AddCommGroup P]
[Module R P]
[IsLocalRing R]
[Module.Finite R P]
[Flat R P]
:
Free R P
Alias of Module.free_of_flat_of_isLocalRing.
theorem
Module.free_of_lTensor_residueField_injective
{R : Type u_3}
[CommRing R]
{M : Type u_4}
{N : Type u_1}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
{P : Type u_2}
[AddCommGroup P]
[Module R P]
(f : M →ₗ[R] N)
(g : N →ₗ[R] P)
[IsLocalRing R]
(hg : Function.Surjective ⇑g)
(h : Function.Exact ⇑f ⇑g)
[Module.Finite R M]
[Module.Finite R N]
[Free R N]
(hf : Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField R) f))
:
Free R P
If M → N → P → 0 is a presentation of P over a local ring (R, 𝔪, k) with
M finite and N finite free, then injectivity of k ⊗ M → k ⊗ N implies that P is free.
theorem
IsLocalRing.split_injective_iff_lTensor_residueField_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[IsLocalRing R]
[Module.Finite R M]
[Module.Finite R N]
[Module.Free R N]
(l : M →ₗ[R] N)
:
(∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id) ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField R) l)
Given a linear map l : M → N over a local ring (R, 𝔪, k)
with M finite and N finite free,
l is a split injection if and only if k ⊗ l is a (split) injection.
@[deprecated IsLocalRing.split_injective_iff_lTensor_residueField_injective (since := "2024-11-09")]
theorem
LocalRing.split_injective_iff_lTensor_residueField_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[IsLocalRing R]
[Module.Finite R M]
[Module.Finite R N]
[Module.Free R N]
(l : M →ₗ[R] N)
:
(∃ (l' : N →ₗ[R] M), l' ∘ₗ l = LinearMap.id) ↔ Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField R) l)
Alias of IsLocalRing.split_injective_iff_lTensor_residueField_injective.
Given a linear map l : M → N over a local ring (R, 𝔪, k)
with M finite and N finite free,
l is a split injection if and only if k ⊗ l is a (split) injection.