# Multiplication and division of submodules of an algebra. #

An interface for multiplication and division of sub-R-modules of an R-algebra A is developed.

## Main definitions #

Let `R` be a commutative ring (or semiring) and let `A` be an `R`-algebra.

- `1 : Submodule R A` : the R-submodule R of the R-algebra A
- `Mul (Submodule R A)` : multiplication of two sub-R-modules M and N of A is defined to be the smallest submodule containing all the products `m * n`.
- `Div (Submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such that `a • J ⊆ I`

It is proved that `Submodule R A` is a semiring, and also an algebra over `Set A`.

Additionally, in the `Pointwise` scope we promote `Submodule.pointwiseDistribMulAction` to a `MulSemiringAction` as `Submodule.pointwiseMulSemiringAction`.

When `R` is not necessarily commutative, and `A` is merely a `R`-module with a ring structure such that `IsScalarTower R A A` holds (equivalent to the data of a ring homomorphism `R →+* A` by `ringHomEquivModuleIsScalarTower`), we can still define `1 : Submodule R A` and `Mul (Submodule R A)`, but `1` is only a left identity, not necessarily a right one.

## Tags #

multiplication of submodules, division of submodules, submodule semiring

source
theorem SubMulAction.algebraMap_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
(algebraMap R A) r ∈ 1
source
theorem SubMulAction.mem_one' {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :
x ∈ 1 ↔ ∃ (y : R), (algebraMap R A) y = x
source
instance Submodule.one {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
One (Submodule R A)

`1 : Submodule R A` is the submodule `R ∙ 1` of `A`.

Equations

- Submodule.one = { one := LinearMap.range (LinearMap.toSpanSingleton R A 1) }

source
theorem Submodule.one_eq_span {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
1 = span R {1}
source
theorem Submodule.le_one_toAddSubmonoid {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
1 ≤ toAddSubmonoid 1
source
@[simp]
theorem Submodule.toSubMulAction_one {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
toSubMulAction 1 = 1
source
theorem Submodule.one_eq_span_one_set {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
1 = span R 1
source
@[simp]
theorem Submodule.one_le {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {P : Submodule R A} :
1 ≤ P ↔ 1 ∈ P
source
instance Submodule.instAddCommMonoidWithOne {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
AddCommMonoidWithOne (Submodule R A)
Equations

- One or more equations did not get rendered due to their size.

source
instance Submodule.instSMul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
SMul (Submodule R A) (Submodule R M)
Equations

- One or more equations did not get rendered due to their size.

source
theorem Submodule.smul_toAddSubmonoid {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} :
(I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid
source
theorem Submodule.smul_mem_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} {r : A} {n : M} (hr : r ∈ I) (hn : n ∈ N) :
r • n ∈ I • N
source
theorem Submodule.smul_le {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N P : Submodule R M} :
I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P
source
@[simp]
theorem Submodule.coe_set_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} :
↑I • N = I • N
source
theorem Submodule.smul_induction_on {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} {p : M → Prop} {x : M} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) (add : ∀ (x y : M), p x → p y → p (x + y)) :
p x
source
theorem Submodule.smul_induction_on' {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} {x : M} (hx : x ∈ I • N) {p : (x : M) → x ∈ I • N → Prop} (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯) (add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯) :
p x hx

Dependent version of `Submodule.smul_induction_on`.

source
theorem Submodule.smul_mono {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I J : Submodule R A} {N P : Submodule R M} (hij : I ≤ J) (hnp : N ≤ P) :
I • N ≤ J • P
source
theorem Submodule.smul_mono_left {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I J : Submodule R A} {N : Submodule R M} (h : I ≤ J) :
I • N ≤ J • N
source
instance Submodule.instCovariantClassHSMulLe_1 {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le
source
@[simp]
theorem Submodule.smul_bot {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (I : Submodule R A) :
I • ⊥ = ⊥
source
@[simp]
theorem Submodule.bot_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (N : Submodule R M) :
⊥ • N = ⊥
source
theorem Submodule.smul_sup {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (I : Submodule R A) (N P : Submodule R M) :
I • (N ⊔ P) = I • N ⊔ I • P
source
theorem Submodule.sup_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (I J : Submodule R A) (N : Submodule R M) :
(I ⊔ J) • N = I • N ⊔ J • N
source
theorem Submodule.smul_assoc {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {B : Type u_2} [Semiring B] [Module R B] [Module A B] [Module B M] [IsScalarTower R A B] [IsScalarTower R B M] [IsScalarTower A B M] (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) :
(I • J) • N = I • J • N
source
theorem Submodule.smul_iSup {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {ι : Sort u_2} {I : Submodule R A} {t : ι → Submodule R M} :
I • ⨆ (i : ι), t i = ⨆ (i : ι), I • t i
source
theorem Submodule.iSup_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {ι : Sort u_2} {t : ι → Submodule R A} {N : Submodule R M} :
(⨆ (i : ι), t i) • N = ⨆ (i : ι), t i • N
source
theorem Submodule.one_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (N : Submodule R M) :
1 • N = N
source
theorem Submodule.smul_subset_smul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (I : Submodule R A) (N : Submodule R M) :
↑I • ↑N ⊆ ↑(I • N)
source
instance Submodule.mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
Mul (Submodule R A)

Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N` consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`.

Equations

- Submodule.mul = { mul := fun (x1 x2 : Submodule R A) => x1 • x2 }

source
theorem Submodule.mul_mem_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N : Submodule R A} {m n : A} (hm : m ∈ M) (hn : n ∈ N) :
m * n ∈ M * N
source
theorem Submodule.mul_le {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N P : Submodule R A} :
M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
source
theorem Submodule.mul_toAddSubmonoid {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M N : Submodule R A) :
(M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
source
theorem Submodule.mul_induction_on {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N : Submodule R A} {C : A → Prop} {r : A} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ (x y : A), C x → C y → C (x + y)) :
C r
source
theorem Submodule.mul_induction_on' {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N : Submodule R A} {C : (r : A) → r ∈ M * N → Prop} (mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯) (add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯) {r : A} (hr : r ∈ M * N) :
C r hr

A dependent version of `mul_induction_on`.

source
@[simp]
theorem Submodule.mul_bot {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) :
M * ⊥ = ⊥
source
@[simp]
theorem Submodule.bot_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) :
⊥ * M = ⊥
source
theorem Submodule.one_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) :
1 * M = M
source
instance Submodule.instMulLeftMono {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
MulLeftMono (Submodule R A)
source
instance Submodule.instMulRightMono {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
MulRightMono (Submodule R A)
source
theorem Submodule.mul_comm_of_commute {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N : Submodule R A} (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) :
M * N = N * M
source
theorem Submodule.mul_sup {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M N P : Submodule R A) :
M * (N ⊔ P) = M * N ⊔ M * P
source
theorem Submodule.sup_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M N P : Submodule R A) :
(M ⊔ N) * P = M * P ⊔ N * P
source
theorem Submodule.mul_subset_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M N : Submodule R A) :
↑M * ↑N ⊆ ↑(M * N)
source
theorem Submodule.restrictScalars_mul {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C] {I J : Submodule B C} :
restrictScalars A (I * J) = restrictScalars A I * restrictScalars A J
source
theorem Submodule.iSup_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {ι : Sort uι} (s : ι → Submodule R A) (t : Submodule R A) :
(⨆ (i : ι), s i) * t = ⨆ (i : ι), s i * t
source
theorem Submodule.mul_iSup {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {ι : Sort uι} (t : Submodule R A) (s : ι → Submodule R A) :
t * ⨆ (i : ι), s i = ⨆ (i : ι), t * s i
source
instance Submodule.instNonUnitalSemiring {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
NonUnitalSemiring (Submodule R A)

Sub-`R`-modules of an `R`-module form an idempotent semiring.

Equations

- One or more equations did not get rendered due to their size.

source
instance Submodule.instPowNat {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
Pow (Submodule R A) ℕ
Equations

- Submodule.instPowNat = { pow := fun (s : Submodule R A) (n : ℕ) => npowRec n s }

source
theorem Submodule.pow_eq_npowRec {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} :
M ^ n = npowRec n M
source
theorem Submodule.pow_zero {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) :
M ^ 0 = 1
source
theorem Submodule.pow_succ {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} :
M ^ (n + 1) = M ^ n * M
source
theorem Submodule.pow_add {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {m n : ℕ} (h : n ≠ 0) :
M ^ (m + n) = M ^ m * M ^ n
source
theorem Submodule.pow_one {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) :
M ^ 1 = M
source
theorem Submodule.pow_succ' {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} (h : n ≠ 0) :
M ^ (n + 1) = M * M ^ n

`Submodule.pow_succ` with the right-hand side commuted.

source
@[simp]
theorem Submodule.bot_pow {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {n : ℕ} :
n ≠ 0 → ⊥ ^ n = ⊥
source
theorem Submodule.pow_toAddSubmonoid {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} (h : n ≠ 0) :
(M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
source
theorem Submodule.le_pow_toAddSubmonoid {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} :
M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
source
theorem Submodule.pow_subset_pow {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {n : ℕ} :
↑M ^ n ⊆ ↑(M ^ n)
source
theorem Submodule.pow_mem_pow {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) {x : A} (hx : x ∈ M) (n : ℕ) :
x ^ n ∈ M ^ n
source
theorem Submodule.restrictScalars_pow {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C] {I : Submodule B C} {n : ℕ} (hn : n ≠ 0) :
restrictScalars A (I ^ n) = restrictScalars A I ^ n
source
theorem Submodule.one_eq_range {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
1 = LinearMap.range (Algebra.linearMap R A)
source
theorem Submodule.algebraMap_mem {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (r : R) :
(algebraMap R A) r ∈ 1
source
@[simp]
theorem Submodule.mem_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {x : A} :
x ∈ 1 ↔ ∃ (y : R), (algebraMap R A) y = x
source
theorem Submodule.smul_one_eq_span {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (x : A) :
x • 1 = span R {x}
source
theorem Submodule.map_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
map f.toLinearMap 1 = 1
source
@[simp]
theorem Submodule.map_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
map (↑(MulOpposite.opLinearEquiv R)) 1 = 1
source
@[simp]
theorem Submodule.comap_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
comap (↑(MulOpposite.opLinearEquiv R)) 1 = 1
source
@[simp]
theorem Submodule.map_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
map (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
source
@[simp]
theorem Submodule.comap_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
comap (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
source
theorem Submodule.mul_eq_map₂ {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M N : Submodule R A} :
M * N = map₂ (LinearMap.mul R A) M N
source
theorem Submodule.span_mul_span (R : Type u) [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (S T : Set A) :
span R S * span R T = span R (S * T)
source
theorem Submodule.mul_def (R : Type u) [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) :
M * N = span R (↑M * ↑N)
source
theorem Submodule.mul_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) :
M * 1 = M
source
theorem Submodule.map_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N
source
theorem Submodule.map_op_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) :
map (↑(MulOpposite.opLinearEquiv R)) (M * N) = map (↑(MulOpposite.opLinearEquiv R)) N * map (↑(MulOpposite.opLinearEquiv R)) M
source
theorem Submodule.comap_unop_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) :
comap (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = comap (↑(MulOpposite.opLinearEquiv R).symm) N * comap (↑(MulOpposite.opLinearEquiv R).symm) M
source
theorem Submodule.map_unop_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A ᵐᵒᵖ) :
map (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = map (↑(MulOpposite.opLinearEquiv R).symm) N * map (↑(MulOpposite.opLinearEquiv R).symm) M
source
theorem Submodule.comap_op_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A ᵐᵒᵖ) :
comap (↑(MulOpposite.opLinearEquiv R)) (M * N) = comap (↑(MulOpposite.opLinearEquiv R)) N * comap (↑(MulOpposite.opLinearEquiv R)) M
source
instance Submodule.instIsScalarTower {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {α : Type u_1} [Monoid α] [DistribMulAction α A] [SMulCommClass α R A] [IsScalarTower α A A] :
IsScalarTower α (Submodule R A) (Submodule R A)
source
instance Submodule.instSMulCommClass {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {α : Type u_1} [Monoid α] [DistribMulAction α A] [SMulCommClass α R A] [SMulCommClass α A A] :
SMulCommClass α (Submodule R A) (Submodule R A)
source
instance Submodule.instSMulCommClass_1 {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {α : Type u_1} [Monoid α] [DistribMulAction α A] [SMulCommClass α R A] [SMulCommClass A α A] :
SMulCommClass (Submodule R A) α (Submodule R A)
source
def Submodule.hasDistribPointwiseNeg {R : Type u} [CommSemiring R] {A : Type u_1} [Ring A] [Algebra R A] :
HasDistribNeg (Submodule R A)

`Submodule.pointwiseNeg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale.

Equations

- Submodule.hasDistribPointwiseNeg = Function.Injective.hasDistribNeg Submodule.toAddSubmonoid ⋯ ⋯ ⋯

Instances For

source
theorem Submodule.mem_span_mul_finite_of_mem_span_mul {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] {S S' : Set A} {x : A} (hx : x ∈ span R (S * S')) :
∃ (T : Finset A) (T' : Finset A), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
source
theorem Submodule.mul_eq_span_mul_set {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s t : Submodule R A) :
s * t = span R (↑s * ↑t)
source
theorem Submodule.mem_span_mul_finite_of_mem_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) :
∃ (T : Finset A) (T' : Finset A), ↑T ⊆ ↑P ∧ ↑T' ⊆ ↑Q ∧ x ∈ span R (↑T * ↑T')
source
theorem Submodule.mem_span_singleton_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} {x y : A} :
x ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x
source
theorem Submodule.mem_mul_span_singleton {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} {x y : A} :
x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x
source
theorem Submodule.span_singleton_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {x : A} {p : Submodule R A} :
span R {x} * p = x • p
source
theorem Submodule.mem_smul_iff_inv_mul_mem {R : Type u} [CommSemiring R] {S : Type u_1} [DivisionSemiring S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ≠ 0) :
y ∈ x • p ↔ x⁻¹ * y ∈ p
source
theorem Submodule.mul_mem_smul_iff {R : Type u} [CommSemiring R] {S : Type u_1} [Ring S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ∈ nonZeroDivisors S) :
x * y ∈ x • p ↔ y ∈ p
source
theorem Submodule.mul_smul_mul_eq_smul_mul_smul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) (x y : R) :
(x * y) • (M * N) = x • M * y • N
source
instance Submodule.idemSemiring {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
IdemSemiring (Submodule R A)

Sub-R-modules of an R-algebra form an idempotent semiring.

Equations

- One or more equations did not get rendered due to their size.

source
instance Submodule.instIsOrderedRing {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
IsOrderedRing (Submodule R A)
source
theorem Submodule.span_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : Set A) (n : ℕ) :
span R s ^ n = span R (s ^ n)
source
theorem Submodule.pow_eq_span_pow_set {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) :
M ^ n = span R (↑M ^ n)
source
theorem Submodule.pow_induction_on_left' {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop} (algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) (mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯) {n : ℕ} {x : A} (hx : x ∈ M ^ n) :
C n x hx

Dependent version of `Submodule.pow_induction_on_left`.

source
theorem Submodule.pow_induction_on_right' {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop} (algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) (mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯) {n : ℕ} {x : A} (hx : x ∈ M ^ n) :
C n x hx

Dependent version of `Submodule.pow_induction_on_right`.

source
theorem Submodule.pow_induction_on_left {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : A → Prop} (hr : ∀ (r : R), C ((algebraMap R A) r)) (hadd : ∀ (x y : A), C x → C y → C (x + y)) (hmul : ∀ m ∈ M, ∀ (x : A), C x → C (m * x)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) :
C x

To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars, is closed under addition, and holds for `m * x` where `m ∈ M` and it holds for `x`

source
theorem Submodule.pow_induction_on_right {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : A → Prop} (hr : ∀ (r : R), C ((algebraMap R A) r)) (hadd : ∀ (x y : A), C x → C y → C (x + y)) (hmul : ∀ (x : A), C x → ∀ m ∈ M, C (x * m)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) :
C x

To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars, is closed under addition, and holds for `x * m` where `m ∈ M` and it holds for `x`

source
def Submodule.mapHom {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
Submodule R A →+* Submodule R A'

`Submonoid.map` as a `RingHom`, when applied to an `AlgHom`.

Equations

- Submodule.mapHom f = { toFun := Submodule.map f.toLinearMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.mapHom_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (p : Submodule R A) :
(mapHom f) p = map f.toLinearMap p
source
theorem Submodule.mapHom_id {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
mapHom (AlgHom.id R A) = RingHom.id (Submodule R A)
source
def Submodule.equivOpposite {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
Submodule R A ᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ

The ring of submodules of the opposite algebra is isomorphic to the opposite ring of submodules.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Submodule.equivOpposite_symm_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (p : (Submodule R A)ᵐᵒᵖ) :
equivOpposite.symm p = comap (↑(MulOpposite.opLinearEquiv R).symm) (MulOpposite.unop p)
source
@[simp]
theorem Submodule.equivOpposite_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (p : Submodule R A ᵐᵒᵖ) :
equivOpposite p = MulOpposite.op (comap (↑(MulOpposite.opLinearEquiv R)) p)
source
theorem Submodule.map_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) :
map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n
source
theorem Submodule.comap_unop_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) :
comap (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = comap (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
source
theorem Submodule.comap_op_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (n : ℕ) (M : Submodule R A ᵐᵒᵖ) :
comap (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = comap (↑(MulOpposite.opLinearEquiv R)) M ^ n
source
theorem Submodule.map_op_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) :
map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = map (↑(MulOpposite.opLinearEquiv R)) M ^ n
source
theorem Submodule.map_unop_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (n : ℕ) (M : Submodule R A ᵐᵒᵖ) :
map (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = map (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
source
noncomputable def Submodule.span.ringHom {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
SetSemiring A →+* Submodule R A

`span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets on either side).

Equations

- Submodule.span.ringHom = { toFun := fun (s : SetSemiring A) => Submodule.span R (SetSemiring.down s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.span.ringHom_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : SetSemiring A) :
ringHom s = span R (SetSemiring.down s)
source
def Submodule.pointwiseMulSemiringAction {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {α : Type u_1} [Monoid α] [MulSemiringAction α A] [SMulCommClass α R A] :
MulSemiringAction α (Submodule R A)

The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.

This is a stronger version of `Submodule.pointwiseDistribMulAction`.

Equations

- Submodule.pointwiseMulSemiringAction = { toDistribMulAction := Submodule.pointwiseDistribMulAction, smul_one := ⋯, smul_mul := ⋯ }

Instances For

source
theorem Submodule.mul_mem_mul_rev {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {M N : Submodule R A} {m n : A} (hm : m ∈ M) (hn : n ∈ N) :
n * m ∈ M * N
source
theorem Submodule.mul_comm {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (M N : Submodule R A) :
M * N = N * M
source
instance Submodule.instIdemCommSemiring {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] :
IdemCommSemiring (Submodule R A)

Sub-R-modules of an R-algebra A form a semiring.

Equations

- One or more equations did not get rendered due to their size.

source
theorem Submodule.prod_span {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {ι : Type u_1} (s : Finset ι) (M : ι → Set A) :
∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)
source
theorem Submodule.prod_span_singleton {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {ι : Type u_1} (s : Finset ι) (x : ι → A) :
∏ i ∈ s, span R {x i} = span R {∏ i ∈ s, x i}
source
noncomputable instance Submodule.moduleSet (R : Type u) [CommSemiring R] (A : Type v) [CommSemiring A] [Algebra R A] :
Module (SetSemiring A) (Submodule R A)

R-submodules of the R-algebra A are a module over `Set A`.

Equations

- One or more equations did not get rendered due to their size.

source
theorem Submodule.setSemiring_smul_def {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (s : SetSemiring A) (P : Submodule R A) :
s • P = span R (SetSemiring.down s) * P
source
theorem Submodule.smul_le_smul {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {s t : SetSemiring A} {M N : Submodule R A} (h₁ : SetSemiring.down s ⊆ SetSemiring.down t) (h₂ : M ≤ N) :
s • M ≤ t • N
source
theorem Submodule.singleton_smul {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (a : A) (M : Submodule R A) :
Set.up {a} • M = map (LinearMap.mulLeft R a) M
source
instance Submodule.instDiv {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] :
Div (Submodule R A)

The elements of `I / J` are the `x` such that `x • J ⊆ I`.

In fact, we define `x ∈ I / J` to be `∀ y ∈ J, x * y ∈ I` (see `mem_div_iff_forall_mul_mem`), which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nicer to use in proofs.

This is the general form of the ideal quotient, traditionally written $I : J$.

Equations

- Submodule.instDiv = { div := fun (I J : Submodule R A) => { carrier := {x : A | ∀ y ∈ J, x * y ∈ I}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

source
theorem Submodule.mem_div_iff_forall_mul_mem {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {x : A} {I J : Submodule R A} :
x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
source
theorem Submodule.mem_div_iff_smul_subset {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {x : A} {I J : Submodule R A} :
x ∈ I / J ↔ x • ↑J ⊆ ↑I
source
theorem Submodule.le_div_iff {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I J K : Submodule R A} :
I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J
source
theorem Submodule.le_div_iff_mul_le {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I J K : Submodule R A} :
I ≤ J / K ↔ I * K ≤ J
source
theorem Submodule.one_le_one_div {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I : Submodule R A} :
1 ≤ 1 / I ↔ I ≤ 1
source
@[simp]
theorem Submodule.one_mem_div {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I J : Submodule R A} :
1 ∈ I / J ↔ J ≤ I
source
theorem Submodule.le_self_mul_one_div {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I : Submodule R A} (hI : I ≤ 1) :
I ≤ I * (1 / I)
source
theorem Submodule.mul_one_div_le_one {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I : Submodule R A} :
I * (1 / I) ≤ 1
source
@[simp]
theorem Submodule.map_div {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (I J : Submodule R A) (h : A ≃ₐ[R] B) :
map h.toLinearMap (I / J) = map h.toLinearMap I / map h.toLinearMap J