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

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

@[implicit_reducible]

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.

theorem Submodule.one_eq_span {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] : 1 = R ∙ 1

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

@[simp]

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

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

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

@[implicit_reducible]

instance Submodule.instAddCommMonoidWithOne {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] : AddCommMonoidWithOne (Submodule R A)

@[implicit_reducible]

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)

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

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

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

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

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

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.

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

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

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

@[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 • ⊥ = ⊥

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

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

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

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

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

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

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

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)

@[implicit_reducible]

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.

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

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

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

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

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.

@[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 * ⊥ = ⊥

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

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

instance Submodule.instMulLeftMono {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] : MulLeftMono (Submodule R A)

instance Submodule.instMulRightMono {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] : MulRightMono (Submodule R A)

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

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

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

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)

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

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

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

theorem Submodule.mul_top_eq_top_of_mul_eq_one {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] (N P : Submodule R A) (h : N * P = 1) : N * ⊤ = ⊤

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

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

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

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

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

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.

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

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

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

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)

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

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

theorem Submodule.one_eq_range {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : 1 = (Algebra.linearMap R A).range

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

theorem Submodule.smul_one_eq_span {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (x : A) : x • 1 = R ∙ x

theorem Submodule.span_singleton_algebraMap_of_isUnit {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {r : R} (h : IsUnit r) : R ∙ (algebraMap R A) r = 1

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

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

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

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

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

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

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)

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)

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

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

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

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

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

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)

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)

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)

@[implicit_reducible]

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.

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

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)

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

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 ∈ (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 y : A} : x ∈ P * (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} : (R ∙ x) * p = x • p

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

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

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

@[implicit_reducible]

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.

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

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)

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)

theorem Submodule.top_mul_eq_top_of_mul_eq_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {N P : Submodule R A} (h : N * P = 1) : ⊤ * P = ⊤

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.

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.

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

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.

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

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)

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.

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

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

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

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

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

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

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

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

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

noncomputable def Submodule.spanSingleton (R : Type u) [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : A →*₀ Submodule R A

(span R {·}) as a MonoidWithZeroHom.

@[simp]

theorem Submodule.spanSingleton_apply {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (x : A) : (spanSingleton R) x = R ∙ x

theorem Submodule.span_singleton_eq_one_iff {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] [FaithfulSMul R A] {x : A} : R ∙ x = 1 ↔ ∃ (r : Rˣ), x = (algebraMap R A) ↑r

theorem Submodule.mker_spanSingleton {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] [FaithfulSMul R A] : MonoidHom.mker (spanSingleton R) = Submonoid.map (algebraMap R A) (IsUnit.submonoid R)

theorem Submodule.ker_unitsMap_spanSingleton {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] [FaithfulSMul R A] : (Units.map ↑(spanSingleton R)).ker = (Units.map ↑(algebraMap R A)).range

Exactness of the sequence 1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A at Aˣ. See Exercise I.3.7(iv) in [Weibel2013] or Theorem 2.4 in [RobertsSingh1993].

@[implicit_reducible]

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.

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

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

@[implicit_reducible]

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.

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)

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, R ∙ x i = R ∙ ∏ i ∈ s, x i

@[implicit_reducible]

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.

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

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

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

@[implicit_reducible]

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

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

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

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

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

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

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

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

theorem Submodule.restrictScalars_image_smul_eq {R : Type u} [CommSemiring R] {S : Type u_1} {M : Type u_2} [CommSemiring S] [Algebra S R] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower S R M] (s : Set S) (N : Submodule R M) : restrictScalars S (⇑(algebraMap S R) '' s • N) = s • restrictScalars S N