Lemmas about the IsSMulRegular Predicate

For modules over a ring the proposition IsSMulRegular r M is equivalent to r being a non-zero-divisor, i.e. r • x = 0 only if x = 0 for x ∈ M. This specific result is isSMulRegular_iff_smul_eq_zero_imp_eq_zero. Lots of results starting from this, especially ones about quotients (which don't make sense without some algebraic assumptions), are in this file. We don't pollute the Mathlib/Algebra/Regular/SMul.lean file with these because it's supposed to import a minimal amount of the algebraic hierarchy.

Tags

module, regular element, commutative algebra

theorem LinearEquiv.isSMulRegular_congr' {R : Type u_3} {S : Type u_2} {M : Type u_4} {N : Type u_1} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] (e : M ≃ₛₗ[σ] N) (r : R) : IsSMulRegular M r ↔ IsSMulRegular N (σ r)

theorem LinearEquiv.isSMulRegular_congr {R : Type u_2} {M : Type u_3} {N : Type u_1} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (r : R) : IsSMulRegular M r ↔ IsSMulRegular N r

theorem IsSMulRegular.submodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (r : R) (h : IsSMulRegular M r) : IsSMulRegular (↥N) r

theorem IsSMulRegular.lTensor {R : Type u_1} (M : Type u_3) {M' : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] [Module.Flat R M] {r : R} (h : IsSMulRegular M' r) : IsSMulRegular (TensorProduct R M M') r

theorem IsSMulRegular.rTensor {R : Type u_1} (M : Type u_3) {M' : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] [Module.Flat R M] {r : R} (h : IsSMulRegular M' r) : IsSMulRegular (TensorProduct R M' M) r

theorem isSMulRegular_submodule_iff_right_eq_zero_of_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsSMulRegular (↥N) r ↔ ∀ x ∈ N, r • x = 0 → x = 0

theorem isSMulRegular_quotient_iff_mem_of_smul_mem {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsSMulRegular (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N → x ∈ N

theorem mem_of_isSMulRegular_quotient_of_smul_mem {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} {r : R} (h1 : IsSMulRegular (M ⧸ N) r) {x : M} (h2 : r • x ∈ N) : x ∈ N

theorem isSMulRegular_of_range_eq_ker {R : Type u_1} {M : Type u_3} {M' : Type u_4} {M'' : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] {r : R} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''} (hf : Function.Injective ⇑f) (hfg : f.range = g.ker) (h1 : IsSMulRegular M r) (h2 : IsSMulRegular M'' r) : IsSMulRegular M' r

Given a left exact sequence 0 → M → M' → M'', if r is regular on both M and M'' it's regular M' too.

theorem isSMulRegular_of_isSMulRegular_on_submodule_on_quotient {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} {r : R} (h1 : IsSMulRegular (↥N) r) (h2 : IsSMulRegular (M ⧸ N) r) : IsSMulRegular M r

theorem biUnion_associatedPrimes_eq_compl_regular (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] : ⋃ p ∈ associatedPrimes R M, ↑p = {r : R | IsSMulRegular M r}ᶜ

theorem isSMulRegular_iff_ker_lsmul_eq_bot {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : IsSMulRegular M r ↔ ((LinearMap.lsmul R M) r).ker = ⊥

theorem isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsSMulRegular (↥N) r ↔ Disjoint ((LinearMap.lsmul R M) r).ker N

theorem isSMulRegular_on_quot_iff_lsmul_comap_le {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N ≤ N

theorem isSMulRegular_on_quot_iff_lsmul_comap_eq {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) : IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N = N

theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) {r : R} : IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)

theorem isSMulRegular_of_ker_lsmul_eq_bot {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {r : R} (h : ((LinearMap.lsmul R M) r).ker = ⊥) : IsSMulRegular M r

theorem smul_top_inf_eq_smul_of_isSMulRegular_on_quot {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {N : Submodule R M} {r : R} : IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N

theorem QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last {R : Type u_1} {M : Type u_3} {M' : Type u_4} {M'' : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] {M''' : Type u_6} [AddCommGroup M'''] [Module R M'''] {r : R} {f₁ : M →ₗ[R] M'} {f₂ : M' →ₗ[R] M''} {f₃ : M'' →ₗ[R] M'''} (h₁₂ : Function.Exact ⇑f₁ ⇑f₂) (h₂₃ : Function.Exact ⇑f₂ ⇑f₃) (h : IsSMulRegular M''' r) : Function.Exact ⇑((map r) f₁) ⇑((map r) f₂)