Finite modules over local rings #

This file gathers various results about finite modules over a local ring (R, 𝔪, k).

Main results #

IsLocalRing.subsingleton_tensorProduct: If M is finitely generated, k ⊗ M = 0 ↔ M = 0.
Module.free_of_maximalIdeal_rTensor_injective: If M is a finitely presented module such that m ⊗ M → M is injective (for example when M is flat), then M is free.
Module.free_of_lTensor_residueField_injective: If N → M → P → 0 is a presentation of P with N finite and M finite free, then injectivity of k ⊗ N → k ⊗ M implies that P is free.
IsLocalRing.split_injective_iff_lTensor_residueField_injective: Given an R-linear map l : M → N with M finite and N finite free, l is a split injection if and only if k ⊗ l is 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) :

Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₁ = Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₂ ↔ N₁ = N₂

source

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] :

Submodule.map (IsLocalRing.maximalIdeal R • ⊤).mkQ N = ⊤ ↔ N = ⊤

source

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] :

Submodule.map ((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) N = ⊤ ↔ N = ⊤

source

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] :

Subsingleton (TensorProduct R (IsLocalRing.ResidueField R) M) ↔ Subsingleton M

source

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 ι (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) M)) (hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i) :

Submodule.span R (Set.range f) = ⊤

source

@[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.

source

@[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] :

Submodule.map (IsLocalRing.maximalIdeal R • ⊤).mkQ N = ⊤ ↔ N = ⊤

Alias of IsLocalRing.map_mkQ_eq_top.

source

@[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] :

Submodule.map ((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) N = ⊤ ↔ N = ⊤

Alias of IsLocalRing.map_tensorProduct_mk_eq_top.

source

@[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] :

Subsingleton (TensorProduct R (IsLocalRing.ResidueField R) M) ↔ Subsingleton M

Alias of IsLocalRing.subsingleton_tensorProduct.

source

@[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) :

Submodule.span R (Set.range f) = ⊤

Alias of IsLocalRing.span_eq_top_of_tmul_eq_basis.

source

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.

source

theorem Module.exists_basis_of_basis_baseChange {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.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)))) :

∃ (b : Basis ι R M), ∀ (i : ι), b i = v i

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.

source

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] [Module.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) = ⊤) :

∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), b i = v (a i)

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.

source

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] [Module.FinitePresentation R M] [Module.Flat R M] {ι : Type u} (v : ι → M) (hv : Submodule.span R (Set.range v) = ⊤) :

∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), b i = v (a i)

source

theorem Module.free_of_maximalIdeal_rTensor_injective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] (H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R)))) :

Module.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.

source

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.FinitePresentation R P] [Module.Flat R P] :

Module.Free R P

source

@[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.FinitePresentation R P] [Module.Flat R P] :

Module.Free R P

Alias of Module.free_of_flat_of_isLocalRing.

source

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] [Module.Free R N] (hf : Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField R) f)) :

Module.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.

source

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 (IsLocalRing.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.

source

@[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.

Documentation

Mathlib.RingTheory.LocalRing.Module

Finite modules over local rings #

Main results #