LinearMap.range_coe
theorem LinearMap.range_coe :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] (f : F), ↑(LinearMap.range f) = Set.range ⇑f
The theorem `LinearMap.range_coe` states that for any semirings `R` and `R₂`, any additive commutative monoids `M` and `M₂`, any modules `M` over `R` and `M₂` over `R₂`, any ring homomorphism `τ₁₂` from `R` to `R₂`, any function `F` that is like a function from `M` to `M₂`, any semilinear map from `M` to `M₂` over `R` induced by `τ₁₂`, and assuming `τ₁₂` is surjective, the range of a linear map `f` of type `F` as a subtype (coerced to a set) is equal to the set of all outputs (range) of the function corresponding to `f`.
More concisely: Given a semiring homomorphism τ₁₂, a semilinear map F induced by it between modules M over R and N₂ over R₂, and assuming τ₁₂ is surjective, the range of F as a subtype is equal to the image of M under F.
|
LinearMap.range_comp
theorem LinearMap.range_comp :
∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
[inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₁₂]
[inst_11 : RingHomSurjective τ₂₃] [inst_12 : RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃),
LinearMap.range (g.comp f) = Submodule.map g (LinearMap.range f)
The theorem `LinearMap.range_comp` states that for any three semirings `R`, `R₂`, and `R₃`, and any three additive commutative monoids `M`, `M₂`, and `M₃`, and any three ring homomorphisms `τ₁₂`, `τ₂₃`, and `τ₁₃` such that `τ₁₂`, `τ₂₃`, and `τ₁₃` form a ring homomorphism triple and are surjective, if `f` is a linear map from `M` to `M₂` and `g` is a linear map from `M₂` to `M₃`, then the range of the composition of `g` and `f` is the same as the image of the range of `f` under `g`. In other words, composing two linear maps and then taking the range gives the same result as first taking the range of the first map, and then mapping it through the second map.
More concisely: For any surjective ring homomorphisms τ₁₂, τ₂₃, and τ₁₃ between semirings R, R₂, and R₃, and any linear maps f : M → M₂ and g : M₂ → M₃ between additive commutative monoids M, M₂, and M₃, the range of g ∘ f is equal to the image of the range of f under g.
|
Submodule.range_subtype
theorem Submodule.range_subtype :
∀ {R : Type u_1} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), LinearMap.range p.subtype = p
The theorem `Submodule.range_subtype` states that for any type `R` with a semiring structure, any type `M` with both an addition-commutative monoid structure and a module structure over `R`, and any submodule `p` of `M`, the range of the linear map from the submodule `p` to `M` (given by the function `Submodule.subtype p`) is equal to the submodule `p` itself. Informally, this says that when we apply the embedding of the submodule `p` into `M` to every element of `p`, we get exactly `p` as a result.
More concisely: For any semiring `R`, additive monoid and `R`-module `M`, and submodule `p` of `M`, the image of `p` under the submodule embedding is equal to `p`.
|
LinearMap.map_le_range
theorem LinearMap.map_le_range :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] {f : F} {p : Submodule R M}, Submodule.map f p ≤ LinearMap.range f
The theorem `LinearMap.map_le_range` states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` and `M₂` over the semirings `R` and `R₂` respectively, a ring homomorphism `τ₁₂` from `R` to `R₂` that is surjective, a function `f` of type `F` that behaves like a function from `M` to `M₂` with properties defined by `SemilinearMapClass`, and a submodule `p` of `M`, the image of the submodule `p` under the function `f` is a subset of or equal to the range of the linear map `f`. This essentially means that applying a semilinear map to a submodule will not yield elements outside of the map's range.
More concisely: For any semiring homomorphism τ₁₂, modules M and M₂, a semilinear map f, and submodule p of M, the image of p under f is contained in the range of the linear map f.
|
Submodule.map_top
theorem Submodule.map_top :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] (f : F), Submodule.map f ⊤ = LinearMap.range f
The theorem `Submodule.map_top` states that for any semiring `R` and `R₂`, any additive commutative monoid `M` and `M₂`, any module `R M` and `R₂ M₂`, any ring homomorphism `τ₁₂` from `R` to `R₂`, any function-like `F` from `M` to `M₂`, and any semilinear map `f` from `M` to `M₂` (with these semilinear maps being a class of functions that preserve addition and scalar multiplication), if `τ₁₂` is surjective, then, the image under `f` of the top element of the submodule lattice (which is the whole module `M`) equals the range of the linear map `f`. This is stating that applying `f` to all elements of `M` is equivalent to taking the range of `f`.
More concisely: If `τ₁₂` is a surjective ring homomorphism from semiring `R` to `R₂`, then the image of the top element of the submodule lattice of `R M` under any semilinear map `f` from `M` to `R₂ M₂` equals the range of `f`.
|
LinearMap.range_eq_map
theorem LinearMap.range_eq_map :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] (f : F), LinearMap.range f = Submodule.map f ⊤
The theorem `LinearMap.range_eq_map` states that for all types `R`, `R₂`, `M`, `M₂` and `F`, if `R` and `R₂` are semirings, `M` and `M₂` are additive commutative monoids, `M` and `M₂` are modules over `R` and `R₂` respectively, `τ₁₂` is a surjective ring homomorphism from `R` to `R₂`, `F` is a function-like type from `M` to `M₂`, and `f` is an instance of `F`, then the range of the linear map `f` is equal to the image of the top-level submodule (denoted as `⊤`) under the map `f`. Basically, it says that the set of all possible outputs of a linear map `f` is the same as the set of all results of applying `f` to every element of the top-level submodule.
More concisely: For a surjective ring homomorphism τ₁₂ from semirings R to R₂, and a linear map f from an additive commutative monoid and module M over R to an additive commutative monoid and module M₂ over R₂, the range of f equals the image of the top-level submodule ⊤ under f.
|
LinearMap.ker_eq_bot_of_cancel
theorem LinearMap.ker_eq_bot_of_cancel :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂},
(∀ (u v : ↥(LinearMap.ker f) →ₗ[R] M), f.comp u = f.comp v → u = v) → LinearMap.ker f = ⊥
This theorem states that for any linear map `f` from a module `M` to another module `M₂` over two semirings `R` and `R₂`, if for every pair of linear maps `u` and `v` from the kernel of `f` to `M` the equality `f.comp u = f.comp v` implies `u = v`, then the kernel of `f` is trivial (i.e., it contains only the zero element). This result is a formal statement of the fact that a monomorphism (a map that is left-cancellable) is injective in the context of linear maps.
More concisely: If for any linear maps `u` and `v` from the kernel of a linear map `f` from module `M` to module `M₂` over semirings `R` and `R₂` such that `f.comp u = f.comp v` implies `u = v`, then the kernel of `f` is the zero submodule of `M`.
|
LinearMap.mem_range
theorem LinearMap.mem_range :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂}, x ∈ LinearMap.range f ↔ ∃ y, f y = x
This theorem, named `LinearMap.mem_range`, states that for all types `R`, `R₂`, `M`, `M₂`, and `F`, given certain conditions, an element `x` of type `M₂` is in the range of a linear map `f` if and only if there exists an element `y` such that the result of applying the function `f` to `y` equals `x`.
The conditions required are that `R` and `R₂` are semirings, `M` and `M₂` are additive commutative monoids, `M` and `M₂` are modules over `R` and `R₂` respectively, there is a ring homomorphism `τ₁₂` from `R` to `R₂` which is surjective, `F` is a type that behaves like a function from `M` to `M₂`, and `F` belongs to the class of semilinear maps `SemilinearMapClass` from `M` to `M₂` for `τ₁₂`.
More concisely: Given semirings R and R₂, additive commutative monoids and modules M and M₂ over R and R₂ respectively, a surjective ring homomorphism τ₁₂ from R to R₂, and a semilinear map F from M to M₂ with respect to τ₁₂, an element x of M₂ is in the range of the linear map F if and only if there exists an element y in M such that F(y) = x.
|
Submodule.map_subtype_top
theorem Submodule.map_subtype_top :
∀ {R : Type u_1} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), Submodule.map p.subtype ⊤ = p
The theorem `Submodule.map_subtype_top` states that for any semiring `R`, an additive commutative monoid `M`, and a module `M` over `R`, for any submodule `p` of `M`, the image of the maximal submodule (denoted as `⊤`) of `p` under the canonical linear map from `p` to `M` (defined by the function `Submodule.subtype`) is just `p` itself. In mathematical terms, this is saying that if we map every element of `p` to `M` using the canonical embedding, the resulting set is exactly `p`.
More concisely: For any submodule `p` of an `R`-module `M`, the canonical embedding map from `p` to `M` maps the maximal submodule of `p` to `p` itself.
|
LinearMap.range_eq_top
theorem LinearMap.range_eq_top :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] {f : F}, LinearMap.range f = ⊤ ↔ Function.Surjective ⇑f
The theorem `LinearMap.range_eq_top` states that for any semirings `R` and `R₂`, commutative additive monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` which has a function-like structure from `M` to `M₂`, and a semilinear map from `M` to `M₂` over `τ₁₂`, where `τ₁₂` is surjective, a function `f : F` is such that the range of the linear map corresponding to `f` is the entire codomain (`⊤`) if and only if the function corresponding to `f` is surjective. In other words, the linear map `f` covers the entire codomain if and only if for every element in the codomain, there is a preimage in the domain of `f`.
More concisely: Given a surjective ring homomorphism τ₁₂ from semiring R to R₂, a semilinear map f from module M over R to module M₂ over R₂, then the range of the linear map corresponding to f equals the entire codomain if and only if f is surjective.
|
Submodule.map_comap_eq_self
theorem Submodule.map_comap_eq_self :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂},
q ≤ LinearMap.range f → Submodule.map f (Submodule.comap f q) = q
Theorem `Submodule.map_comap_eq_self` states that for any semirings `R` and `R₂`, additively commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a function `f` of type `F` where `F` is a class that can be injectively coerced to a function from `M` to `M₂`, a semilinear map class over `F`, `τ₁₂`, `M` and `M₂`, a surjective ring homomorphism `τ₁₂`, and a submodule `q` of `M₂` over `R₂`, if `q` is a subset of the range of `f`, then the mapping of the comapping of `q` using `f` equals `q` itself. In other words, if we first comap `q` using `f` and then map the result again using `f`, we end up with `q` itself, provided `q` is within the range of `f`. This theorem is a formal statement of the property about the interplay between mapping and comapping in the context of module theory.
More concisely: If `f` is a semilinear map from a module `M` over a ring `R` to a module `M₂` over a ring `R₂`, `τ₁₂` is a surjective ring homomorphism from `R` to `R₂`, `q` is a submodule of `M₂` that is contained in the image of `f`, then the image of `q` under `f` and the image of `q` under the comappling of `f` are equal.
|
Submodule.map_comap_eq
theorem Submodule.map_comap_eq :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂),
Submodule.map f (Submodule.comap f q) = LinearMap.range f ⊓ q
This theorem, `Submodule.map_comap_eq`, states that for any semiring `R` and `R₂`, any additive commutative monoid `M` and `M₂`, any module `M` over `R`, any module `M₂` over `R₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a function `F` that is `FunLike` from `M` to `M₂`, a semilinear map from `M` to `M₂` that preserves the action of `τ₁₂`, a ring homomorphism `τ₁₂`, a module homomorphism `f` from `M` to `M₂`, and a submodule `q` of `M₂`, the image under `f` of the preimage of `q` under `f` equals the intersection of the range of `f` and `q`.
In simpler terms, if you take a submodule `q` of `M₂`, map it back to `M` using `f`, and then map it forward to `M₂` using the same `f`, you end up precisely with the intersection of the original submodule `q` and the range of `f`.
More concisely: For any ring homomorphism τ₁₂ from semiring R to R₂, module M over R, module M₂ over R₂, FunLike function F from M to M₂, semilinear map g from M to M₂ preserving the action of τ₁₂, module homomorphism f from M to M₂, and submodule q of M₂, the image under f of the preimage of q under f equals the intersection of the range of f and q.
|
LinearMap.mem_range_self
theorem LinearMap.mem_range_self :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] (f : F) (x : M), f x ∈ LinearMap.range f
This theorem states that for any semiring `R`, another semiring `R₂`, an additive commutative monoid `M`, another additive commutative monoid `M₂`, a module structure over `R` on `M`, a module structure over `R₂` on `M₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` such that terms of type `F` have an injective coercion to functions from `M` to `M₂`, and a semilinear map from `M` to `M₂` compatible with `τ₁₂`, where `τ₁₂` is surjective, for every `f` of type `F` and `x` of type `M`, the image of `x` under `f` is in the range of `f`. In other words, any value you get from applying a function `f` to an element `x` is indeed in the set of possible outputs of that function `f`.
More concisely: Given semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, module structures over `R` and `R₂`, a surjective ring homomorphism `τ₁₂` from `R` to `R₂`, a semilinear map `f` from `M` to `M₂` compatible with `τ₁₂`, and an injective coercion from terms of type `F` to functions `M -> M₂`, for all `x in M` and `f of type F`, we have `f x in Im f`.
|
LinearMap.range_le_ker_iff
theorem LinearMap.range_le_ker_iff :
∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
[inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃}, LinearMap.range f ≤ LinearMap.ker g ↔ g.comp f = 0
This theorem states that for all semirings `R`, `R₂`, and `R₃`, additive commutative monoids `M`, `M₂`, `M₃`, and modules over them, ring homomorphisms `τ₁₂`, `τ₂₃`, `τ₁₃`, and `f` & `g` which are linear maps, if the homomorphisms are such that the composition of `τ₁₂` and `τ₂₃` equals `τ₁₃` and `τ₁₂` is surjective, then the range of the linear map `f` is less than or equal to the kernel of the linear map `g` if and only if the composition of `g` and `f` equals zero.
In simpler terms, this theorem is about the relationship between the range and kernel of two linear mappings: if the image of the first map is entirely contained within the null space of the second map, then the composition of the two maps is the zero map.
More concisely: If `τ₁:` R -> R₂, `τ₂:` R₂ -> R₃ are surjective ring homomorphisms, `f:` M -> N and `g:` N -> P are linear maps of modules such that `τ₁∘τ₂ = τ₁₃`, then `∣∣f∣∣ ≤ ∣∣ker g∣∣ if and only if `g∘f = 0`.
|