Documentation

Mathlib.RingTheory.LocalRing.Module

Finite modules over local rings #

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

Main results #

theorem LocalRing.map_mkQ_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [LocalRing R] {N₁ : Submodule R M} {N₂ : Submodule R M} (h : N₁ N₂) (h' : N₂.FG) :
Submodule.map (LocalRing.maximalIdeal R N₂).mkQ N₁ = Submodule.map (LocalRing.maximalIdeal R N₂).mkQ N₂ N₁ = N₂
theorem LocalRing.span_eq_top_of_tmul_eq_basis {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [LocalRing R] [Module.Finite R M] {ι : Type u_3} (f : ιM) (b : Basis ι (LocalRing.ResidueField R) (TensorProduct R (LocalRing.ResidueField R) M)) (hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i) :
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₁)) :

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.

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.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) [LocalRing 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 (LocalRing.ResidueField R) f)) :

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 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] [LocalRing 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 (LocalRing.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.