Reducing a module modulo an element of the ring

Given a commutative ring R and an element r : R, the association M ↦ M ⧸ rM extends to a functor on the category of R-modules. This functor is isomorphic to the functor of tensoring by R ⧸ (r) on either side, but can be more convenient to work with since we can work with quotient types instead of fiddling with simple tensors.

Tags

module, commutative algebra

@[reducible, inline]

abbrev QuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] : Type u_1

An abbreviation for M⧸rM that keeps us from having to write (⊤ : Submodule R M) over and over to satisfy the typechecker.

def QuotSMulTop.congr {R : Type u_2} [CommRing R] (r : R) {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] (e : M' ≃ₗ[R] M'') : QuotSMulTop r M' ≃ₗ[R] QuotSMulTop r M''

If M' is isomorphic to M'' as R-modules, then M'⧸rM' is isomorphic to M''⧸rM''.

noncomputable def QuotSMulTop.equivQuotTensor {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] : QuotSMulTop r M ≃ₗ[R] TensorProduct R (R ⧸ Ideal.span {r}) M

Reducing a module modulo r is the same as left tensoring with R/(r).

noncomputable def QuotSMulTop.equivTensorQuot {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] : QuotSMulTop r M ≃ₗ[R] TensorProduct R M (R ⧸ Ideal.span {r})

Reducing a module modulo r is the same as right tensoring with R/(r).

def QuotSMulTop.map {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] : (M →ₗ[R] M') →ₗ[R] QuotSMulTop r M →ₗ[R] QuotSMulTop r M'

The action of the functor QuotSMulTop r on morphisms.

@[simp]

theorem QuotSMulTop.map_apply_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) : ((map r) f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)

theorem QuotSMulTop.map_comp_mkQ {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') : (map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f

@[simp]

theorem QuotSMulTop.map_id {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] : (map r) LinearMap.id = LinearMap.id

@[simp]

theorem QuotSMulTop.map_comp {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] (g : M' →ₗ[R] M'') (f : M →ₗ[R] M') : (map r) (g ∘ₗ f) = (map r) g ∘ₗ (map r) f

theorem QuotSMulTop.equivQuotTensor_naturality_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) : (equivQuotTensor r M') (((map r) f) (Submodule.Quotient.mk x)) = (LinearMap.lTensor (R ⧸ Ideal.span {r}) f) ((equivQuotTensor r M) (Submodule.Quotient.mk x))

theorem QuotSMulTop.equivQuotTensor_naturality {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') : ↑(equivQuotTensor r M') ∘ₗ (map r) f = LinearMap.lTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(equivQuotTensor r M)

theorem QuotSMulTop.equivTensorQuot_naturality_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) : (equivTensorQuot r M') (((map r) f) (Submodule.Quotient.mk x)) = (LinearMap.rTensor (R ⧸ Ideal.span {r}) f) ((equivTensorQuot r M) (Submodule.Quotient.mk x))

theorem QuotSMulTop.equivTensorQuot_naturality {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') : ↑(equivTensorQuot r M') ∘ₗ (map r) f = LinearMap.rTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(equivTensorQuot r M)

theorem QuotSMulTop.map_surjective {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑((map r) f)

theorem QuotSMulTop.map_exact {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''} (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Function.Exact ⇑((map r) f) ⇑((map r) g)

noncomputable def QuotSMulTop.tensorQuotSMulTopEquivQuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) (M' : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] : TensorProduct R M (QuotSMulTop r M') ≃ₗ[R] QuotSMulTop r (TensorProduct R M M')

Tensoring on the left and applying QuotSMulTop · r commute.

noncomputable def QuotSMulTop.quotSMulTopTensorEquivQuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) (M' : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] : TensorProduct R (QuotSMulTop r M') M ≃ₗ[R] QuotSMulTop r (TensorProduct R M' M)

Tensoring on the right and applying QuotSMulTop · r commute.

noncomputable def QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop {R : Type u_3} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] (S : Type u_2) [CommRing S] [Algebra R S] : QuotSMulTop ((algebraMap R S) r) (TensorProduct R S M) ≃ₗ[S] TensorProduct R S (QuotSMulTop r M)

Let R be a commutative ring, M be an R-module, S be an R-algebra, then S ⊗[R] (M/rM) is isomorphic to (S ⊗[R] M)⧸r(S ⊗[R] M) as S-modules.

theorem QuotSMulTop.mem_annihilator {R : Type u_2} [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] (x : R) : x ∈ Module.annihilator R (QuotSMulTop x M)