Linear maps out of a cyclic quotient

For an ideal J of a commutative ring R and an R-module M, evaluation at 1 identifies the linear maps R ⧸ J → M with the elements of M killed by J: Hom_R(R ⧸ J, M) ≅ M[J]. This is the quotient form of Mathlib's ringLmapEquivSelf, which is the case J = 0. In Matlis duality it identifies the layer E[𝔪ⁿ] of an injective hull E with the Matlis dual of R ⧸ 𝔪ⁿ.

Main declarations

• LinearMap.apply_quotient_mk_eq_smul_apply_one: a linear map f out of R ⧸ J is determined by f 1, taking the value r • f 1 at the class of r.
• Ideal.quotientLinearMapEquivTorsionBySet: the linear equivalence ((R ⧸ J) →ₗ[R] M) ≃ₗ[R] torsionBySet R M J, given by evaluation at 1.

theorem LinearMap.apply_quotient_mk_eq_smul_apply_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {J : Ideal R} (f : R ⧸ J →ₗ[R] M) (r : R) : f ((Ideal.Quotient.mk J) r) = r • f 1

A linear map out of R ⧸ J takes the value r • f 1 at the class of r.

def Ideal.quotientLinearMapEquivTorsionBySet {R : Type u_1} [CommRing R] (J : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : (R ⧸ J →ₗ[R] M) ≃ₗ[R] ↥(Submodule.torsionBySet R M ↑J)

Evaluation at 1 identifies linear maps R ⧸ J → M with the elements of M killed by J.

@[simp]

theorem Ideal.coe_quotientLinearMapEquivTorsionBySet_apply {R : Type u_1} [CommRing R] (J : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : R ⧸ J →ₗ[R] M) : ↑((J.quotientLinearMapEquivTorsionBySet M) f) = f 1

@[simp]

theorem Ideal.quotientLinearMapEquivTorsionBySet_symm_apply_mk {R : Type u_1} [CommRing R] (J : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (x : ↥(Submodule.torsionBySet R M ↑J)) (r : R) : ((J.quotientLinearMapEquivTorsionBySet M).symm x) ((Quotient.mk J) r) = r • ↑x