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 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_algebraMap_iff
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
[CommSemiring R]
[Semiring S]
[Algebra R S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(r : R)
:
IsSMulRegular M ((algebraMap R S) r) ↔ IsSMulRegular M r
theorem
isSMulRegular_iff_smul_eq_zero_imp_eq_zero
{R : Type u_1}
(M : Type u_3)
[Ring R]
[AddCommGroup M]
[Module R M]
(r : R)
:
IsSMulRegular M r ↔ ∀ (x : M), r • x = 0 → x = 0
theorem
isSMulRegular_iff_mem_nonZeroSMulDivisors
{R : Type u_1}
(M : Type u_3)
[Ring R]
[AddCommGroup M]
[Module R M]
(r : R)
:
IsSMulRegular M r ↔ r ∈ nonZeroSMulDivisors R M
theorem
isSMulRegular_of_smul_eq_zero_imp_eq_zero
{R : Type u_1}
{M : Type u_3}
[Ring R]
[AddCommGroup M]
[Module R M]
{r : R}
(h : ∀ (x : M), r • x = 0 → x = 0)
:
IsSMulRegular M r
theorem
isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero
{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_on_quot_iff_smul_mem_implies_mem
{R : Type u_1}
{M : Type u_3}
[Ring R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(r : R)
:
theorem
mem_of_isSMulRegular_on_quot_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 : LinearMap.range f = LinearMap.ker g)
(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.ker ((LinearMap.lsmul R M) r) = ⊥
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.ker ((LinearMap.lsmul R M) r)) 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.ker ((LinearMap.lsmul R M) r) = ⊥)
:
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}
:
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 ⇑((QuotSMulTop.map r) f₁) ⇑((QuotSMulTop.map r) f₂)