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

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, ↑(algebraMap R A) y = x

source

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.

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

1 ≤ 1.toAddSubmonoid

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, ↑(algebraMap R A) y = x

source

@[simp]

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

Submodule.toSubMulAction 1 = 1

source

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

1 = Submodule.span R {1}

source

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

source

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

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') :

Submodule.map (AlgHom.toLinearMap f) 1 = 1

source

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

source

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

source

@[simp]

theorem Submodule.map_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :

Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) 1 = 1

source

@[simp]

theorem Submodule.comap_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :

Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) 1 = 1

source

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.

source

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

source

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 : A), m ∈ M → ∀ (n : A), n ∈ N → m * n ∈ P

source

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

source

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 : A) → m ∈ M → (n : A) → 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} [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} (hm : (m : A) → (x : m ∈ M) → (n : A) → (x_1 : n ∈ N) → C (m * n) (_ : m * n ∈ M * N)) (ha : (x : A) → (hx : x ∈ M * N) → (y : A) → (hy : y ∈ M * N) → C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)) {r : A} (hr : r ∈ M * N) :

C r hr

A dependent version of mul_induction_on.

source

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)

source

@[simp]

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

M * ⊥ = ⊥

source

@[simp]

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

⊥ * M = ⊥

source

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

1 * M = M

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

source

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

source

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

source

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

source

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

source

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)

source

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 (AlgHom.toLinearMap f) (M * N) = Submodule.map (AlgHom.toLinearMap f) M * Submodule.map (AlgHom.toLinearMap f) N

source

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

source

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 (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) (M * N) = Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) N * Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) M

source

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 (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) (M * N) = Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) N * Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) M

source

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

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.

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 : Set A} {S' : Set A} {x : A} (hx : x ∈ Submodule.span R (S * S')) :

∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ Submodule.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 : Submodule R A) (t : Submodule R A) :

s * t = Submodule.span R (↑s * ↑t)

source

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

source

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

source

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 T', ↑T ⊆ ↑P ∧ ↑T' ⊆ ↑Q ∧ x ∈ Submodule.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 : A} {y : A} :

x ∈ Submodule.span R {y} * P ↔ ∃ z, 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 : A} {y : A} :

x ∈ P * Submodule.span R {y} ↔ ∃ z, z ∈ P ∧ z * y = x

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.

source

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)

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

source

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)

source

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

source

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

source

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

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} (hr : (r : R) → C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)) (hadd : (x y : A) → (i : ℕ) → (hx : x ∈ M ^ i) → (hy : y ∈ M ^ i) → C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)) (hmul : (m : A) → (hm : m ∈ M) → (i : ℕ) → (x : A) → (hx : x ∈ M ^ i) → C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)) {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} (hr : (r : R) → C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)) (hadd : (x y : A) → (i : ℕ) → (hx : x ∈ M ^ i) → (hy : y ∈ M ^ i) → C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)) (hmul : (i : ℕ) → (x : A) → (hx : x ∈ M ^ i) → C i x hx → (m : A) → (hm : m ∈ M) → C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))) {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 : A) → 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 : A) → 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

@[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 (AlgHom.toLinearMap f) p

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

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)ᵐᵒᵖ) :

↑(RingEquiv.symm Submodule.equivOpposite) p = Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) (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ᵐᵒᵖ) :

↑Submodule.equivOpposite p = MulOpposite.op (Submodule.comap (↑(MulOpposite.opLinearEquiv R)) p)

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.

Instances For

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 : ℕ) :

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

Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) (M ^ n) = Submodule.comap (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) 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ᵐᵒᵖ) :

Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.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 : ℕ) :

Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.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ᵐᵒᵖ) :

Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) (M ^ n) = Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))) M ^ n

source

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

source

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).

Instances For

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.

Instances For

source

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

source

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

source

instance Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule {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.

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) :

(Finset.prod s fun i => Submodule.span R (M i)) = Submodule.span R (Finset.prod s fun i => 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) :

(Finset.prod s fun i => Submodule.span R {x i}) = Submodule.span R {Finset.prod s fun i => x i}

source

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.

source

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

source

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

source

theorem Submodule.smul_singleton {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

source

instance Submodule.instDivSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule {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$.

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 : Submodule R A} {J : Submodule R A} :

x ∈ I / J ↔ ∀ (y : A), 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 : Submodule R A} {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 : Submodule R A} {J : Submodule R A} {K : Submodule R A} :

I ≤ J / K ↔ ∀ (x : A), x ∈ I → ∀ (z : A), 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 : Submodule R A} {J : Submodule R A} {K : Submodule R A} :

I ≤ J / K ↔ I * K ≤ J

source

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

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 : Submodule R A) (J : Submodule R A) (h : A ≃ₐ[R] B) :

Submodule.map (AlgEquiv.toLinearMap h) (I / J) = Submodule.map (AlgEquiv.toLinearMap h) I / Submodule.map (AlgEquiv.toLinearMap h) J