Submodule.quotientRel_r_def
theorem Submodule.quotientRel_r_def :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{x y : M}, Setoid.r x y ↔ x - y ∈ p
This theorem states that for any ring `R`, any additive commutative group `M`, any `R`-module structure on `M`, and any submodule `p` of `M`, the relation `Setoid.r` between two elements `x` and `y` of `M` is equivalent to the assertion that the difference `x - y` is an element of the submodule `p`. In other words, two elements `x` and `y` in the module `M` are related by the equivalence relation defined by the setoid if and only if their difference is in the given submodule `p`.
More concisely: For any ring `R`, additive commutative group `M`, `R`-module structure on `M`, and submodule `p` of `M`, the equivalence relation defined by the setoid `Setoid.r` on `M` is equivalent to the submodule membership relation for the differences of elements in `M` with respect to `p`.
|
Submodule.mkQ_apply
theorem Submodule.mkQ_apply :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
(x : M), p.mkQ x = Submodule.Quotient.mk x
The theorem `Submodule.mkQ_apply` states that for any ring `R`, any additive commutative group `M` that is also an `R`-module, and any submodule `p` of `M`, the function `Submodule.mkQ` applied to an element `x` of `M` is equal to the function `Submodule.Quotient.mk` applied to the same element `x`. In other words, the mapping from a module `M` to the quotient of `M` by a submodule `p` as a linear map, when applied to an element of the module, yields the same result as the map associating to an element of `M` the corresponding element of `M/p`, where `p` is a submodule of `M`.
More concisely: For any ring `R`, additive commutative group `M` that is an `R`-module, and submodule `p` of `M`, the application of `Submodule.mkQ` to an element `x` of `M` is equivalent to the application of `Submodule.Quotient.mk` to `x`, i.e., `Submodule.mkQ x = Submodule.Quotient.mk x` in `M/p`.
|
Submodule.Quotient.eq
theorem Submodule.Quotient.eq :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{x y : M}, Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ p
The theorem `Submodule.Quotient.eq` states that for any ring `R`, additively commutative group `M`, a module `M` over a ring `R`, and a submodule `p` of `M`, and any two elements `x` and `y` of `M`, the quotient of `x` and `y` under the submodule (i.e., `Submodule.Quotient.mk x` and `Submodule.Quotient.mk y`) are equal if and only if the difference of `x` and `y` is an element of the submodule `p`. In other words, `x` and `y` are equivalent modulo the submodule `p` precisely when their difference is in `p`.
More concisely: For any ring `R`, additively commutative group `M`, module `M` over `R`, submodule `p` of `M`, and elements `x`, `y` in `M`, `Submodule.Quotient.mk x = Submodule.Quotient.mk y` if and only if `x - y` is in `p`.
|
Mathlib.LinearAlgebra.Quotient._auxLemma.1
theorem Mathlib.LinearAlgebra.Quotient._auxLemma.1 :
∀ {R : Type u_1} {M : Type u_2} {x : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(p : Submodule R M), (Submodule.Quotient.mk x = 0) = (x ∈ p)
This theorem states that for any ring `R`, additive commutative group `M`, and submodule `p` of `M`, an element `x` of `M` maps to zero in the quotient module `M / p` (that is, `Submodule.Quotient.mk x = 0`) if and only if `x` belongs to the submodule `p` (that is, `x ∈ p`). In other words, the kernel of the quotient map is precisely the submodule `p`.
More concisely: The kernel of the quotient map from a module `M` to its submodule `p` is equal to `p` itself.
|
Submodule.Quotient.mk_surjective
theorem Submodule.Quotient.mk_surjective :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
Function.Surjective Submodule.Quotient.mk
The theorem `Submodule.Quotient.mk_surjective` states that for any ring `R`, any additive commutative group `M` which is also a `R`-module, and any submodule `p` of `M`, the function `Submodule.Quotient.mk` is surjective. In other words, every element in the quotient space `M/p` is the image of some element from `M` under the function `Submodule.Quotient.mk`. This maps an element of `M` to its corresponding element in the quotient space `M/p`.
More concisely: For any ring `R`, `R-module` `M`, and submodule `p` of `M`, the natural quotient map `M → M/p` is surjective.
|
Submodule.quotEquivOfEq.proof_1
theorem Submodule.quotEquivOfEq.proof_1 :
∀ {R : Type u_2} {M : Type u_1} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(p p' : Submodule R M), p = p' → ∀ (a b : M), Setoid.r a b ↔ Setoid.r ((Equiv.refl M) a) ((Equiv.refl M) b)
The theorem `Submodule.quotEquivOfEq.proof_1` states that for any two submodules `p` and `p'` of a module `M` over a ring `R`, if `p` is equal to `p'`, then for any two elements `a` and `b` of the module `M`, the equivalence relation `Setoid.r` between `a` and `b` is the same as the equivalence relation `Setoid.r` between `a` and `b` under the identity equivalence relation on `M` (i.e., where each element of `M` is mapped to itself). In essence, it says that the identity map does not affect the equivalence relationship between elements of the module.
More concisely: For any submodules `p` and `p'` of a module `M` over a ring `R`, if `p = p'`, then the equivalence relations `Setoid.r` on `M` induced by `p` and `p'` are equal.
|
Submodule.Quotient.mk_add
theorem Submodule.Quotient.mk_add :
∀ {R : Type u_1} {M : Type u_2} {x y : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(p : Submodule R M), Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.mk y
The theorem `Submodule.Quotient.mk_add` states that for any type `R` which forms a ring, a type `M` that forms an additive commutative group, a module `M` over `R`, and a submodule `p` of `M`, the mapping that associates to an element of `M` the corresponding element of `M/p` preserves the operation of addition. In other words, if `x` and `y` are elements of `M`, then the image of the sum `x + y` under this map is equal to the sum of the images of `x` and `y`. This can be expressed mathematically as: for all `x, y` in `M`, `Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.mk y`.
More concisely: For any ring `R`, additive commutative group `M`, module `M` over `R`, and submodule `p` of `M`, the quotient map from `M` to `M/p` preserves addition, i.e., `Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.mk y` for all `x, y` in `M`.
|
Submodule.ker_mkQ
theorem Submodule.ker_mkQ :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
LinearMap.ker p.mkQ = p
The theorem `Submodule.ker_mkQ` states that for any ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, and for any submodule `p` of `M`, the kernel of the linear map from `M` to the quotient of `M` by `p` (denoted as `M ⧸ p`), which is created by `Submodule.mkQ p`, is equal to `p`. In other words, this means that the set of all elements of `M` which are mapped to the zero element of the quotient module `M ⧸ p` by this linear map is exactly the submodule `p`.
More concisely: The kernel of the quotient map from an `R`-module `M` to `M/p` is equal to the submodule `p`, where `p` is a submodule of `M` and `M/p` is the quotient of `M` by `p`.
|
Submodule.range_mkQ
theorem Submodule.range_mkQ :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
LinearMap.range p.mkQ = ⊤
This theorem states that for any ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, if `p` is a submodule of `M`, then the range of the linear map from `M` to the quotient of `M` by `p` (denoted as `Submodule.mkQ p`) is the entire quotient module `M/p`. In other words, every element in the quotient module `M/p` can be mapped to by some element in the original module `M` via the `Submodule.mkQ p` linear map.
More concisely: For any ring `R`, additive commutative group `M`, and `R`-module structure on `M`, the `Submodule.mkQ` linear map from `M` to `M/p` is a surjection, where `p` is a submodule of `M`.
|
Submodule.Quotient.eq'
theorem Submodule.Quotient.eq' :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{x y : M}, Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ -x + y ∈ p
The theorem `Submodule.Quotient.eq'` states that for any ring `R`, additive commutative group `M`, and `M` being a module over `R`, given a submodule `p` of `M`, and any two elements `x` and `y` of `M`, the equivalence class of `x` in the quotient module `M/p` is equal to the equivalence class of `y` if and only if the element `-x + y` belongs to the submodule `p`. This theorem encapsulates the fundamental property of quotient structures in module theory.
More concisely: For any ring R, additive commutative group M, and submodule p of M, two elements x and y of M belong to the same equivalence class in M/p if and only if x - y belongs to p.
|
LinearMap.range_eq_top_of_cancel
theorem LinearMap.range_eq_top_of_cancel :
∀ {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
(∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ LinearMap.range f), u.comp f = v.comp f → u = v) → LinearMap.range f = ⊤
The theorem `LinearMap.range_eq_top_of_cancel` states that for any Rings `R` and `R₂`, additive commutative monoids `M` and `M₂`, and modules `M` and `M₂` over `R` and `R₂` respectively, given a surjective ring homomorphism `τ₁₂` from `R` to `R₂`, and a linear map `f` from `M` to `M₂` under `τ₁₂`, if for all linear maps `u` and `v` from `M₂` to the quotient of `M₂` by the range of `f` such that `u` composed with `f` is equal to `v` composed with `f` implies `u` is equal to `v`, then the range of the linear map `f` is the whole of `M₂` (i.e., `f` is surjective or an "epimorphism").
More concisely: If `τ₁₂` is a surjective ring homomorphism from `R` to `R₂`, `f` is a linear map from module `M` over `R` to module `M₂` over `R₂`, and for all `u` and `v` linear maps from `M₂` to the quotient of `M₂` by the range of `f` such that `u ∘ f = v ∘ f`, then `f` is surjective (i.e., the range of `f` equals `M₂`).
|
Submodule.linearMap_qext
theorem Submodule.linearMap_qext :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄, f.comp p.mkQ = g.comp p.mkQ → f = g
This theorem states that for any ring `R`, additive commutative group `M`, and a submodule `p` of the module `M` over `R`, and for any other ring `R₂`, additive commutative group `M₂`, and two `LinearMap`s `f` and `g` from the quotient module `M/p` to `M₂` (where the ring homomorphism `τ₁₂` is responsible for the ring change from `R` to `R₂`), if the compositions of `f` and `g` with the quotient making function of `p` are equal, then `f` and `g` themselves are equal.
In other words, if two linear maps from the quotient module `M/p` to `M₂` yield the same result when composed with the same function that creates the quotient space, they must be the same linear map.
More concisely: If two linear maps from the quotient module `M/p` to `M₂`, when composed with the quotient making function of `p`, yield the same image, then they are equal.
|
Submodule.Quotient.mk_eq_zero
theorem Submodule.Quotient.mk_eq_zero :
∀ {R : Type u_1} {M : Type u_2} {x : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(p : Submodule R M), Submodule.Quotient.mk x = 0 ↔ x ∈ p
The theorem `Submodule.Quotient.mk_eq_zero` states that for any ring `R`, any additive commutative group `M`, and any module `M` over `R`, for any submodule `p` of `M` and any element `x` of `M`, the quotient of `x` by `p` (represented by `Submodule.Quotient.mk x`) is equal to zero if and only if `x` is an element of the submodule `p`. In other words, when considering the quotient space `M/p`, an element `x` in `M` becomes zero if it belongs to the submodule `p` being quotiented out.
More concisely: For any ring `R`, additive commutative group `M`, module `M` over `R`, submodule `p` of `M`, and element `x` in `M`, `Submodule.Quotient.mk x = 0` if and only if `x` is in `p` in the quotient space `M/p`.
|
Submodule.mkQ_surjective
theorem Submodule.mkQ_surjective :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (A : Submodule R M),
Function.Surjective ⇑A.mkQ
This theorem states that for any given ring `R`, additive commutative group `M`, and `A` as a submodule of the `R`-module `M`, the function `Submodule.mkQ A` is surjective. In other words, every element in the quotient module `M/A` is the image of some element of `M` under the `mkQ` function associated with the submodule `A`. This function essentially maps each element of `M` to its equivalence class in the quotient set `M/A`.
More concisely: For any submodule `A` of an additive commutative group `M` over a ring `R`, the `Submodule.mkQ` function maps every element of `M` to some coset in the quotient group `M/A`.
|
Submodule.Quotient.mk_smul
theorem Submodule.Quotient.mk_smul :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{S : Type u_3} [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (r : S) (x : M),
Submodule.Quotient.mk (r • x) = r • Submodule.Quotient.mk x
The theorem `Submodule.Quotient.mk_smul` states that for any ring `R`, any additive commutative group `M` which is also a `R`-module, a submodule `p` of `M`, a type `S` such that `S` can be multiplied by `R` and `M` (denoted by `SMul S R` and `SMul S M` respectively), and such that multiplication of `S` over `R` over `M` is associative (denoted by `IsScalarTower S R M`), and any element `r` of type `S` and `x` of type `M`, scalar multiplication of `r` and `x` followed by the quotient mapping equals to the quotient of `x` followed by scalar multiplication by `r`. In essence, it shows that the map of moving an element of `M` to the quotient group `M/p` commutes with scalar multiplication from `S`.
More concisely: For any ring `R`, additive commutative group `M` that is an `R`-module, submodule `p` of `M`, type `S` with associative scalar multiplication on `M`, and any `r` in `S` and `x` in `M`, we have `(r • x + p) = r • (x + p)` in `M/p`, where `•` denotes scalar multiplication.
|
Submodule.mapQ_comp
theorem Submodule.mapQ_comp :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
{R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {R₃ : Type u_5} {M₃ : Type u_6} [inst_6 : Ring R₃] [inst_7 : AddCommGroup M₃]
[inst_8 : Module R₃ M₃] (p₂ : Submodule R₂ M₂) (p₃ : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃}
[inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ Submodule.comap f p₂)
(hg : p₂ ≤ Submodule.comap g p₃) (h : optParam (p ≤ Submodule.comap f (Submodule.comap g p₃)) ⋯),
p.mapQ p₃ (g.comp f) h = (p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)
This theorem states that for given submodules `p`, `p₂`, and `p₃` of modules `M`, `M₂`, and `M₃` over rings `R`, `R₂`, and `R₃` respectively, and given linear maps `f` from `M` to `M₂` and `g` from `M₂` to `M₃`, if `p` is included in the preimage of `p₂` under `f`, and `p₂` is included in the preimage of `p₃` under `g`, then the quotient map induced by the composition `g ∘ f` from `M` to `M₃` is the composition of the quotient map induced by `f` from `M` to `M₂` and the quotient map induced by `g` from `M₂` to `M₃`. In terms of notation, `mapQ (g ∘ f) = (mapQ g) ∘ (mapQ f)`. Here, `mapQ` refers to the quotient map associated with a given submodule.
More concisely: If submodules $p \subseteq \text{im}(f) \subseteq p'_2$ in modules $M, M_2$ over rings $R, R_2$ respectively, and linear maps $f: M \to M_2$ and $g: M_2 \to M_3$ satisfy $p'_2 \subseteq \text{im}(g)$, then $(\text{quot } M/p) \cong (\text{quot } M_2/p'_2) \cong (\text{quot } M_3/(\text{im } g \cap p'_3})$, where $\text{quot } X/Y$ denotes the quotient module of $X$ by $Y$ and $\cong$ denotes isomorphism.
|