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.

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

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

Equations
theorem Submodule.le_one_toAddSubmonoid {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
1 1.toAddSubmonoid
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.one_eq_span {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] :
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') :
@[simp]
instance Submodule.mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra 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
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 mM, nN, 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 : 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} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {M : Submodule R A} {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.

theorem Submodule.span_mul_span (R : Type u) [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (S : Set A) (T : Set A) :
@[simp]
theorem Submodule.mul_bot {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) :
@[simp]
theorem Submodule.bot_mul {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) :
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.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 : 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] :

    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 : ) :
    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 ^ nProp} (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 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 (Nat.succ i) (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 ((_root_.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 (Nat.succ i) (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

    @[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) :
    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 MonoidWithZeroHom, when applied to AlgHoms.

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

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

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

            Equations
            • One or more equations did not get rendered due to their size.
            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)
            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}
            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.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

            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
            • One or more equations did not get rendered due to their size.
            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 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 : 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 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 : 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