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 locale we promote Submodule.pointwiseDistribMulAction to a MulSemiringAction as Submodule.pointwiseMulSemiringAction.

Tags

multiplication of submodules, division of submodules, submodule semiring

theorem SubMulAction.algebraMap_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R A) r ∈ 1

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

instance Submodule.one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : One (Submodule R A)

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

Equations

• Submodule.one = { one := LinearMap.range (Algebra.linearMap R A) }

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)

theorem Submodule.le_one_toAddSubmonoid {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : 1 ≤ Submodule.toAddSubmonoid 1

theorem Submodule.algebraMap_mem {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (r : R) : (algebraMap R A) r ∈ 1

@[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

@[simp]

theorem Submodule.toSubMulAction_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.toSubMulAction 1 = 1

theorem Submodule.one_eq_span {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : 1 = Submodule.span R {1}

theorem Submodule.one_eq_span_one_set {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : 1 = Submodule.span R 1

theorem Submodule.one_le {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} : 1 ≤ P ↔ 1 ∈ P

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') : Submodule.map f.toLinearMap 1 = 1

@[simp]

theorem Submodule.map_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.map (↑(MulOpposite.opLinearEquiv R)) 1 = 1

@[simp]

theorem Submodule.comap_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.comap (↑(MulOpposite.opLinearEquiv R)) 1 = 1

@[simp]

theorem Submodule.map_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1

@[simp]

theorem Submodule.comap_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1

instance Submodule.mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Mul (Submodule R A)

Multiplication of sub-R-modules of an R-algebra A. The submodule M * N is the smallest R-submodule of A containing the elements m * n for m ∈ M and n ∈ N.

Equations

• Submodule.mul = { mul := Submodule.map₂ (LinearMap.mul R A) }

theorem Submodule.mul_mem_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} {m : A} {n : A} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N

theorem Submodule.mul_le {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} {P : Submodule R A} : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

theorem Submodule.mul_toAddSubmonoid {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) : (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid

theorem Submodule.mul_induction_on {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {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

theorem Submodule.mul_induction_on' {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {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.

theorem Submodule.span_mul_span (R : Type u) [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (S : Set A) (T : Set A) : Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)

@[simp]

theorem Submodule.mul_bot {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) : M * ⊥ = ⊥

@[simp]

theorem Submodule.bot_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) : ⊥ * M = ⊥

theorem Submodule.one_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) : 1 * M = M

theorem Submodule.mul_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) : M * 1 = M

theorem Submodule.mul_le_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} {P : Submodule R A} {Q : Submodule R A} (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q

theorem Submodule.mul_le_mul_left {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} {P : Submodule R A} (h : M ≤ N) : M * P ≤ N * P

theorem Submodule.mul_le_mul_right {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {N : Submodule R A} {P : Submodule R A} (h : N ≤ P) : M * N ≤ M * P

theorem Submodule.mul_sup {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) (P : Submodule R A) : M * (N ⊔ P) = M * N ⊔ M * P

theorem Submodule.sup_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) (P : Submodule R A) : (M ⊔ N) * P = M * P ⊔ N * P

theorem Submodule.mul_subset_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) : ↑M * ↑N ⊆ ↑(M * N)

theorem Submodule.map_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N

theorem Submodule.map_op_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) : Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) N * Submodule.map (↑(MulOpposite.opLinearEquiv R)) M

theorem Submodule.comap_unop_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) : Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M

theorem Submodule.map_unop_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R Aᵐᵒᵖ) (N : Submodule R Aᵐᵒᵖ) : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M

theorem Submodule.comap_op_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R Aᵐᵒᵖ) (N : Submodule R Aᵐᵒᵖ) : Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M * N) = Submodule.comap (↑(MulOpposite.opLinearEquiv R)) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M

theorem Submodule.restrictScalars_mul {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] {I : Submodule B C} {J : Submodule B C} : Submodule.restrictScalars A (I * J) = Submodule.restrictScalars A I * Submodule.restrictScalars A J

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 ⋯ ⋯ ⋯

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 : Set A} {S' : Set A} {x : A} (hx : x ∈ Submodule.span R (S * S')) : ∃ (T : Finset A) (T' : Finset A), ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ Submodule.span R (↑T * ↑T')

theorem Submodule.mul_eq_span_mul_set {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : Submodule R A) (t : Submodule R A) : s * t = Submodule.span R (↑s * ↑t)

theorem Submodule.iSup_mul {ι : Sort uι} {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : ι → Submodule R A) (t : Submodule R A) : (⨆ (i : ι), s i) * t = ⨆ (i : ι), s i * t

theorem Submodule.mul_iSup {ι : Sort uι} {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (t : Submodule R A) (s : ι → Submodule R A) : t * ⨆ (i : ι), s i = ⨆ (i : ι), t * s i

theorem Submodule.mem_span_mul_finite_of_mem_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} {Q : Submodule R A} {x : A} (hx : x ∈ P * Q) : ∃ (T : Finset A) (T' : Finset A), ↑T ⊆ ↑P ∧ ↑T' ⊆ ↑Q ∧ x ∈ Submodule.span R (↑T * ↑T')

theorem Submodule.mem_span_singleton_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} {x : A} {y : A} : x ∈ Submodule.span R {y} * P ↔ ∃ z ∈ P, y * z = x

theorem Submodule.mem_mul_span_singleton {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {P : Submodule R A} {x : A} {y : A} : x ∈ P * Submodule.span R {y} ↔ ∃ z ∈ P, z * y = x

theorem Submodule.span_singleton_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {x : A} {p : Submodule R A} : Submodule.span R {x} * p = x • p

theorem Submodule.mem_smul_iff_inv_mul_mem {R : Type u} [CommSemiring R] {S : Type u_1} [Field S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ≠ 0) : y ∈ x • p ↔ x⁻¹ * y ∈ p

theorem Submodule.mul_mem_smul_iff {R : Type u} [CommSemiring R] {S : Type u_1} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ∈ nonZeroDivisors S) : x * y ∈ x • p ↔ y ∈ p

theorem Submodule.mul_smul_mul_eq_smul_mul_smul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) (x : R) (y : R) : (x * y) • (M * N) = x • M * y • N

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.

theorem Submodule.span_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : Set A) (n : ℕ) : Submodule.span R s ^ n = Submodule.span R (s ^ n)

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 = Submodule.span R (↑M ^ n)

theorem Submodule.pow_subset_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {n : ℕ} : ↑M ^ n ⊆ ↑(M ^ n)

theorem Submodule.pow_mem_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n

theorem Submodule.pow_toAddSubmonoid {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n

theorem Submodule.le_pow_toAddSubmonoid {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

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 ((_root_.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.

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 ((_root_.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.

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

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

@[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) : (Submodule.mapHom f) p = Submodule.map f.toLinearMap p

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 MonoidWithZeroHom, when applied to AlgHoms.

Equations

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

@[simp]

theorem Submodule.equivOpposite_symm_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (p : (Submodule R A)ᵐᵒᵖ) : Submodule.equivOpposite.symm p = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (MulOpposite.unop p)

@[simp]

theorem Submodule.equivOpposite_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (p : Submodule R Aᵐᵒᵖ) : Submodule.equivOpposite p = MulOpposite.op (Submodule.comap (↑(MulOpposite.opLinearEquiv R)) p)

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.

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 : ℕ) : Submodule.map f.toLinearMap (M ^ n) = Submodule.map f.toLinearMap M ^ n

theorem Submodule.comap_unop_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) : Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M ^ n

theorem Submodule.comap_op_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (n : ℕ) (M : Submodule R Aᵐᵒᵖ) : Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M ^ n

theorem Submodule.map_op_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) : Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) M ^ n

theorem Submodule.map_unop_pow {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (n : ℕ) (M : Submodule R Aᵐᵒᵖ) : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M ^ n

@[simp]

theorem Submodule.span.ringHom_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (s : SetSemiring A) : Submodule.span.ringHom s = Submodule.span R (SetSemiring.down s)

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' := ⋯ }

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 = let __src := Submodule.pointwiseDistribMulAction; MulSemiringAction.mk ⋯ ⋯

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

theorem Submodule.mul_comm {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (M : Submodule R A) (N : Submodule R A) : M * N = N * M

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

• Submodule.instIdemCommSemiring = let __src := Submodule.idemSemiring; IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

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, Submodule.span R (M i) = Submodule.span R (∏ i ∈ s, M i)

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, Submodule.span R {x i} = Submodule.span R {∏ i ∈ s, x i}

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

• Submodule.moduleSet R A = Module.mk ⋯ ⋯

theorem Submodule.smul_def {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (s : SetSemiring A) (P : Submodule R A) : s • P = Submodule.span R (SetSemiring.down s) * P

theorem Submodule.smul_le_smul {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {s : SetSemiring A} {t : SetSemiring A} {M : Submodule R A} {N : Submodule R A} (h₁ : SetSemiring.down s ⊆ SetSemiring.down t) (h₂ : M ≤ N) : s • M ≤ t • N

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 = Submodule.map (LinearMap.mulLeft R a) M

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' := ⋯ } }

theorem Submodule.mem_div_iff_forall_mul_mem {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {x : A} {I : Submodule R A} {J : Submodule R A} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

theorem Submodule.mem_div_iff_smul_subset {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {x : A} {I : Submodule R A} {J : Submodule R A} : x ∈ I / J ↔ x • ↑J ⊆ ↑I

theorem Submodule.le_div_iff {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I : Submodule R A} {J : Submodule R A} {K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J

theorem Submodule.le_div_iff_mul_le {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {I : Submodule R A} {J : Submodule R A} {K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J

@[simp]

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

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)

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

@[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 : Submodule R A) (J : Submodule R A) (h : A ≃ₐ[R] B) : Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J