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} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] {N₁ N₂ : Submodule R M} (h : N₁ ≤ N₂) (h' : N₂.FG) : Submodule.map (maximalIdeal R • N₂).mkQ N₁ = Submodule.map (maximalIdeal R • N₂).mkQ N₂ ↔ N₁ = N₂

theorem IsLocalRing.map_mkQ_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] {N : Submodule R M} [Module.Finite R M] : Submodule.map (maximalIdeal R • ⊤).mkQ N = ⊤ ↔ N = ⊤

theorem IsLocalRing.map_tensorProduct_mk_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] {N : Submodule R M} [Module.Finite R M] : Submodule.map ((TensorProduct.mk R (ResidueField R) M) 1) N = ⊤ ↔ N = ⊤

theorem IsLocalRing.subsingleton_tensorProduct {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.Finite R M] : Subsingleton (TensorProduct R (ResidueField R) M) ↔ Subsingleton M

theorem IsLocalRing.span_eq_top_of_tmul_eq_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.Finite R M] {ι : Type u_5} (f : ι → M) (b : Module.Basis ι (ResidueField R) (TensorProduct R (ResidueField R) M)) (hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i) : Submodule.span R (Set.range f) = ⊤

theorem Module.mem_support_iff_nontrivial_residueField_tensorProduct {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : PrimeSpectrum R) : p ∈ support R M ↔ Nontrivial (TensorProduct R p.asIdeal.ResidueField M)

theorem lTensor_injective_of_exact_of_exact_of_rTensor_injective {R : Type u_1} [CommRing R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N₁ : Type u_8} {N₂ : Type u_9} {N₃ : Type u_10} [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} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [FinitePresentation R M] {ι : Type u_5} (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.

theorem Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [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) = ⊤) : ∃ (κ : 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.

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

theorem Module.free_of_maximalIdeal_rTensor_injective {R : Type u_1} {M : Type u_2} [CommRing R] [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} {M : Type u_2} [CommRing R] [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)) : LinearIndependent R v

theorem Module.IsLocalRing.linearCombination_bijective_of_flat {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.Finite R M] [Flat R M] {ι : Type u} (v : ι → M) (h : Function.Bijective ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v))) : Function.Bijective ⇑(Finsupp.linearCombination R v)

theorem Module.free_of_flat_of_isLocalRing {R : Type u_1} {P : Type u_4} [CommRing R] [AddCommGroup P] [Module R P] [IsLocalRing R] [Module.Finite R P] [Flat R P] : Free R P

Stacks Tag 00NZ

theorem Module.free_of_lTensor_residueField_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [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} {M : Type u_2} {N : Type u_3} [CommRing R] [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.

theorem Module.nonempty_basis_of_flat_of_finrank_eq (R : Type u_1) (M : Type u_2) [CommRing R] [Finite (MaximalSpectrum R)] [AddCommGroup M] [Module R M] [Module.Finite R M] [Flat R M] (n : ℕ) (rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) (TensorProduct R (R ⧸ P.asIdeal) M) = n) : Nonempty (Basis (Fin n) R M)

If M is a finite flat module over a commutative semilocal ring R that has the same rank n at every maximal ideal, then M is free of rank n.

theorem Module.free_of_flat_of_finrank_eq (R : Type u_1) (M : Type u_2) [CommRing R] [Finite (MaximalSpectrum R)] [AddCommGroup M] [Module R M] [Module.Finite R M] [Flat R M] (n : ℕ) (rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) (TensorProduct R (R ⧸ P.asIdeal) M) = n) : Free R M

Stacks Tag 02M9