Documentation

Mathlib.Algebra.Algebra.Operations

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.

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.

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

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} [Semiring R] {A : Type v} [Semiring A] [Module R A] :

1 : Submodule R A is the submodule R ∙ 1 of A. TODO: potentially change this back to LinearMap.range (Algebra.linearMap R A) once a version of Algebra without the commutes' field is introduced. See issue https://github.com/leanprover-community/mathlib4/issues/18110.

Equations
theorem Submodule.one_eq_span {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
1 = span R {1}
@[simp]
theorem Submodule.toSubMulAction_one {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] :
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
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] :
Equations
  • One or more equations did not get rendered due to their size.
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} :
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 rI, nN, 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 : MProp} {x : M} (H : x I N) (smul : rI, nN, p (r n)) (add : ∀ (x y : M), p xp yp (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 NProp} (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 hxp y hyp (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
@[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) :
@[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) :
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)
instance Submodule.mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A 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
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 mM, nN, m * n P
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 : AProp} {r : A} (hr : r M * N) (hm : mM, nN, C (m * n)) (ha : ∀ (x y : A), C xC yC (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 * NProp} (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 hxC y hyC (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) :
@[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) :
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
theorem Submodule.mul_le_mul {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N P Q : Submodule R A} (hmp : M P) (hnq : N Q) :
M * N P * Q
theorem Submodule.mul_le_mul_left {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N P : Submodule R A} (h : M N) :
M * P N * P
theorem Submodule.mul_le_mul_right {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N P : Submodule R A} (h : N P) :
M * N M * P
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 : mM, nN, 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} :
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

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

Equations
instance Submodule.instPowNat {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] :
Equations
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.

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) :
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 : } :
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) :
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.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') :
@[simp]
theorem Submodule.map_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
@[simp]
theorem Submodule.comap_op_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
@[simp]
theorem Submodule.map_unop_one {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
@[simp]
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') :
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] :
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] :
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] :

Submodule.pointwiseNeg distributes over multiplication.

This is available as an instance in the Pointwise locale.

Equations
Instances For
    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 span R {y} * P zP, 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 * span R {y} zP, 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} :
    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 N : Submodule R A) (x 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] :

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

    Equations
    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.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 ^ nProp} (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 hxC i y hyC i (x + y) ) (mem_mul : ∀ (m : A) (hm : m M) (i : ) (x : A) (hx : x M ^ i), C i x hxC 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 ^ nProp} (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 hxC i y hyC 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 : AProp} (hr : ∀ (r : R), C ((algebraMap R A) r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : mM, ∀ (x : A), C xC (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 : AProp} (hr : ∀ (r : R), C ((algebraMap R A) r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : ∀ (x : A), C xmM, 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') :

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

    Equations
    Instances For
      @[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) :

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

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

        Equations
        Instances For
          @[simp]

          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
          Instances For
            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

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

            Equations
            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) :
            is, span R (M i) = span R (∏ is, 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) :
            is, span R {x i} = span R {is, x i}
            instance Submodule.moduleSet (R : Type u) [CommSemiring R] (A : Type v) [CommSemiring A] [Algebra R A] :

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

            Equations
            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) :
            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) :
            instance Submodule.instDiv {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra 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
            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 yJ, 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 xI, zK, 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) :