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)
:
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)
:
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)
:
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)
:
theorem
isSMulRegular_iff_mem_nonZeroSMulDivisors
{R : Type u_1}
(M : Type u_3)
[Ring R]
[AddCommGroup M]
[Module R M]
(r : R)
:
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)
:
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)
:
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]
:
theorem
isSMulRegular_iff_ker_lsmul_eq_bot
{R : Type u_1}
(M : Type u_3)
[CommRing R]
[AddCommGroup M]
[Module R M]
(r : 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)
:
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)
:
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)
:
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 ⇑((map r) f₁) ⇑((map r) f₂)