Submodule.map_mono
theorem Submodule.map_mono :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} [inst_6 : RingHomSurjective σ₁₂] {F : Type u_9} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p p' : Submodule R M},
p ≤ p' → Submodule.map f p ≤ Submodule.map f p'
The theorem `Submodule.map_mono` states that for any semirings `R` and `R₂`, additively commutative monoids `M` and `M₂`, `R`-module structure on `M`, `R₂`-module structure on `M₂`, a surjective ring homomorphism `σ₁₂ : R →+* R₂`, a function `f : F` that behaves like a function from `M` to `M₂`, semilinear map `F` with respect to `σ₁₂`, if we have two submodules `p` and `p'` of `M` such that `p` is a subset of `p'` (`p ≤ p'`), then the image of `p` under the function `f` is a subset of the image of `p'` under `f` (`Submodule.map f p ≤ Submodule.map f p'`). In other words, the mapping of submodules by a function respects the inclusion relation between submodules.
More concisely: If `σ₁₂ : R → R₂` is a surjective ring homomorphism, `f : M → M₂` is a semilinear map respecting `σ₁₂`, `p ≤ p'` are submodules of an `R`-module `M`, then `Submodule.map f p ≤ Submodule.map f p'`.
|
Submodule.map_le_iff_le_comap
theorem Submodule.map_le_iff_le_comap :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂]
[inst_8 : RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂},
Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q
The theorem `Submodule.map_le_iff_le_comap` states that for all semirings `R` and `R₂`, additive 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` which is "fun-like" from `M` to `M₂`, and is a semilinear map between `M` and `M₂` under the ring homomorphism `σ₁₂`, and submodules `p` of `M` and `q` of `M₂`, the image of `p` under `f` is a subset of `q` if and only if `p` is a subset of the preimage of `q` under `f`. In other words, the theorem establishes a correspondence between direct mapping and inverse mapping of submodules under the conditions mentioned. This theorem is particularly useful in the study of linear algebra and module theory, where such transformations and their properties play a crucial role.
More concisely: For a ring homomorphism σ₁₂ from semirings R and R₂, fun-like semilinear map f between modules M over R and M₂ over R₂, and submodules p of M and q of M₂, p ⊆ f⁻¹(q) if and only if f(p) ⊆ q.
|
Submodule.mem_map_of_mem
theorem Submodule.mem_map_of_mem :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} [inst_6 : RingHomSurjective σ₁₂] {F : Type u_9} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {r : M}, r ∈ p → f r ∈ Submodule.map f p
The theorem `Submodule.mem_map_of_mem` states that given two semirings `R` and `R₂`, two additive commutative monoids `M` and `M₂` that are also modules over `R` and `R₂` respectively, a surjective ring homomorphism from `R` to `R₂`, and a function `f` that has a `FunLike` relationship between `M` and `M₂`, then for any submodule `p` of `M` and any element `r` of `M`, if `r` is in `p`, then `f(r)` is in the image of `p` under the map `f`. This is a property of submodule maps in the context of semilinear algebra.
More concisely: If `f` is a surjective homomorphism of semirings from `R` to `R₂`, `M` and `M₂` are modules over `R` and `R₂` respectively, `p` is a submodule of `M`, and `r` is an element of `M` in `p`, then `f(r)` is in the image of `p` under `f`.
|
Submodule.map_sup
theorem Submodule.map_sup :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} (p p' : Submodule R M) {F : Type u_9} [inst_6 : FunLike F M M₂]
[inst_7 : SemilinearMapClass F σ₁₂ M M₂] [inst_8 : RingHomSurjective σ₁₂] (f : F),
Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p'
The theorem `Submodule.map_sup` asserts that for any two submodules `p` and `p'` of a module `M` over a semiring `R`, and a function `f` of type `F`, which is a semilinear map from `M` to a module `M₂` over another semiring `R₂` (via a ring homomorphism `σ₁₂` from `R` to `R₂`), the image under `f` of the sup (join) of `p` and `p'` is equal to the sup of the images of `p` and `p'` under `f`. This statement holds under the condition that the ring homomorphism `σ₁₂` is surjective and the function `f` respects the module structure. It roughly corresponds to the distributive property in a lattice structure.
More concisely: For any surjective ring homomorphism σ₁₂ from a semiring R to another semiring R₂, and any semilinear map f : M → M₂ between modules M and M₂ over R and R₂ respectively, the image of the sup of two submodules p and p' of M under f is equal to the sup of the images of p and p' under f.
|
Submodule.gc_map_comap
theorem Submodule.gc_map_comap :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂]
[inst_8 : RingHomSurjective σ₁₂] (f : F), GaloisConnection (Submodule.map f) (Submodule.comap f)
The theorem `Submodule.gc_map_comap` establishes a Galois connection between the map and comap functions in the context of submodules of modules over semirings. Specifically, for any types `R`, `R₂`, `M`, `M₂`, and `F`, given semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, `R`-module structure on `M`, `R₂`-module structure on `M₂`, a semiring homomorphism `σ₁₂` from `R` to `R₂`, a function `f` of type `F` from `M` to `M₂` (with `F` being a type that has an injective coercion to functions from `M` to `M₂`), and when `σ₁₂` is surjective and `F` acts as a semilinear map with respect to `σ₁₂`, then the function `Submodule.map f` and `Submodule.comap f` form a Galois connection. In simpler terms, this means that for all submodules `a` and `b`, `Submodule.map f a` is a subset of `b` if and only if `a` is a subset of `Submodule.comap f b`.
More concisely: Given semirings `R` and `R₂`, additive commutative monoids `M` and `M₂` with `R`-module structures, a semiring homomorphism `σ₁₂` from `R` to `R₂`, a function `f` from `M` to `M₂` acting as a semilinear map with respect to `σ₁₂`, and when `σ₁₂` is surjective, the map and comap functions of `f` on submodules of `M` form a Galois connection.
|
LinearMap.iInf_invariant
theorem LinearMap.iInf_invariant :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {σ : R →+* R}
[inst_3 : RingHomSurjective σ] {ι : Sort u_10} (f : M →ₛₗ[σ] M) {p : ι → Submodule R M},
(∀ (i : ι), ∀ v ∈ p i, f v ∈ p i) → ∀ v ∈ iInf p, f v ∈ iInf p
This theorem states that for a given semiring `R`, an additively commutative monoid `M` that is also a module over `R`, and a surjective ring homomorphism `σ` from `R` to `R`, if we have a linear map `f` from `M` to `M` and a family of submodules `p` of `M`, then if `f` maps each `v` in each submodule `p i` to within `p i`, then `f` will likewise map every `v` in the infimum of the family of submodules `p`, denoted `iInf p`, to within `iInf p`. In other words, the infimum of a family of invariant submodules of an endomorphism is also an invariant submodule.
More concisely: Given a semiring `R`, an additively commutative `R`-module `M`, a surjective ring homomorphism `σ : R -> R`, an endomorphism `f : M -> M`, and a family `{p_i : Submodule M | i in I}` of submodules of `M` such that `f(v) - v` belongs to each `p_i` for all `v` in `M`, then `f(iInf p)` equals `iInf p`.
|
Submodule.map_comp
theorem Submodule.map_comp :
∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {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₃)
(p : Submodule R M), Submodule.map (g.comp f) p = Submodule.map g (Submodule.map f p)
This theorem states that for three semirings R, R₂, R₃ and three modules M, M₂, M₃ over them, given three ring homomorphisms σ₁₂, σ₂₃, σ₁₃ (with σ₁₂ and σ₂₃ composing to σ₁₃), and two linear maps f : M → M₂ and g : M₂ → M₃ with respect to these homomorphisms, for any submodule p of M, mapping the submodule p through the composition of the linear maps g and f is the same as first mapping p through f, creating a new submodule, and then mapping this submodule through g. This theorem is essentially expressing the property that the map operation for submodules is compatible with the composition of linear maps.
More concisely: For three semirings R, R₂, R₃ and modules M, M₂, M₃, if σ₁₂ and σ₂₃ are ring homomorphisms, σ₁₂σ₃ = σ₁₃ is their composition, and f : M → M₂ and g : M₂ → M₃ are linear maps, then the image of a submodule p of M under the composition gf is equal to the image of the submodule p under f followed by g.
|
Submodule.comap_equiv_eq_map_symm
theorem Submodule.comap_equiv_eq_map_symm :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂), Submodule.comap (↑e) K = Submodule.map (↑e.symm) K
This theorem states that for any two semirings `R` and `R₂`, commutative additive monoids `M` and `M₂`, modules over `R` and `R₂` respectively, a pair of inverse ring homomorphisms `τ₁₂` and `τ₂₁` between `R` and `R₂`, a linear equivalence `e` between `M` and `M₂`, and a submodule `K` of `M₂`, the comap of the linear equivalence `e` over the submodule `K` is equal to the map of the inverse of the linear equivalence `e` over the submodule `K`.
In simpler terms, this is about a transformation between two algebraic structures (`M` and `M₂`), preserving the submodule `K` under the mapping and inverse mapping of a linear equivalence.
More concisely: For any commutative semirings R and R₂, modules M over R and M₂ over R₂, ring homomorphisms τ₁₂: R -> R₂ and τ₂₁: R₂ -> R, linear equivalences e: M -> M₂, and submodule K of M₂, the following diagram commutes:
```
M �� injects e ��jet K
|___| |___|
| | | |
| e |---| e^{-1} |
| | | |
|___| |___|
M/K �� incl ��jet M₂/K
```
Here "injects" denotes the inclusion of M into its quotient M/K, and "�� jet" represents the respective quotient maps. In other words, e(m + K) = e(m) + K for all m ∈ M. Similarly, e^{-1}(m₂ + K) = e^{-1}(m₂) + K for all m₂ ∈ M₂.
|
Submodule.map_id
theorem Submodule.map_id :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), Submodule.map LinearMap.id p = p
The theorem `Submodule.map_id` states that for any ring `R` and an `R`-module `M`, with `R` being a semiring and `M` being an additive commutative monoid, the identity map when applied to any submodule `p` of `M`, leaves `p` unchanged. In other words, mapping a submodule `p` of `M` under the identity linear map results in the same submodule `p`. This is similar to the concept in mathematics where applying the identity function to any element of a set leaves the element unchanged.
More concisely: For any ring `R`, `R`-module `M`, and submodule `p` of `M`, the identity map leaves `p` invariant.
|
Submodule.map_bot
theorem Submodule.map_bot :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂]
[inst_8 : RingHomSurjective σ₁₂] (f : F), Submodule.map f ⊥ = ⊥
The theorem `Submodule.map_bot` states that for any semirings `R` and `R₂`, any additive commutative monoids `M` and `M₂`, and any modules over these semirings, given a ring homomorphism from `R` to `R₂` denoted by `σ₁₂`, and a function `f` which is a semilinear map from `M` to `M₂`, if the ring homomorphism `σ₁₂` is surjective, then the image of the zero submodule (denoted by `⊥`) under `f` is again the zero submodule. This simply means that mapping the zero submodule under a semilinear map yields the zero submodule.
More concisely: If `σ₁₂` is a surjective ring homomorphism from `R` to `R₂`, then the image of the zero submodule of `M` under a semilinear map `f` from `M` to `M₂` is the zero submodule of `M₂`.
|
Submodule.map_comap_subtype
theorem Submodule.map_comap_subtype :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p p' : Submodule R M), Submodule.map p.subtype (Submodule.comap p.subtype p') = p ⊓ p'
The theorem `Submodule.map_comap_subtype` states that for any two submodules `p` and `p'` of the module `M` over the semiring `R`, the result of mapping the submodule `p` using the embedding function `Submodule.subtype p`, and then preimage mapping (`Submodule.comap`) with `Submodule.subtype p` applied to `p'`, is equal to the intersection of `p` and `p'`. In other words, applying these two operations (embedding and then preimage mapping) is equivalent to taking the intersection of the two submodules.
More concisely: For any submodules $p, p'$ of an $R$-module $M$, we have $(\text{Submodule.subtype } p)(\text{Submodule.comap } \text{ Submodule.subtype } p')(p) = p \cap p'$.
|
Submodule.mem_comap
theorem Submodule.mem_comap :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} {x : M} {F : Type u_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {f : F}
{p : Submodule R₂ M₂}, x ∈ Submodule.comap f p ↔ f x ∈ p
The theorem `Submodule.mem_comap` states that for all types `R`, `R₂`, `M`, `M₂`, `F` and `x` of type `M`, together with the instances of `Semiring R`, `Semiring R₂`, `AddCommMonoid M`, `AddCommMonoid M₂`, `Module R M`, `Module R₂ M₂`, `FunLike F M M₂`, `SemilinearMapClass F σ₁₂ M M₂`, and given a function `f` of type `F` and a submodule `p` of `R₂` and `M₂`, a term `x` of type `M` is in the preimage of `p` under `f` (denoted as `Submodule.comap f p`) if and only if `f x` is in `p`. This theorem essentially defines how the preimage operation (`Submodule.comap`) works for submodules and functions that are `FunLike`.
More concisely: For any `FunLike` function `F` between modules `M` and `M₂` over semirings `R` and `R₂`, and a submodule `p` of `R₂` and `M₂`, an element `x` of `M` is in the preimage `Submodule.comap f p` if and only if `f x` is in `p`.
|
Submodule.comap_smul
theorem Submodule.comap_smul :
∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [inst : Semifield K] [inst_1 : AddCommMonoid V]
[inst_2 : Module K V] [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂)
(a : K), a ≠ 0 → Submodule.comap (a • f) p = Submodule.comap f p
This theorem states that for any non-zero scalar `a`, the preimage of a submodule `p` under the scalar multiplication map `a • f` is the same as the preimage of the submodule `p` under the original linear map `f`. Here, `K` is a semifield, `V` and `V₂` are additive commutative monoids, and both `V` and `V₂` are modules over `K`. The linear map `f` is from `V` to `V₂`. The scalar multiplication `a • f` means each element of `V` is first multiplied by `a` and then mapped to `V₂` by `f`.
More concisely: For any non-zero scalar `a` in a semifield `K`, the preimage of a submodule `p` under the scalar multiplication map `a • f` equals the preimage of `p` under the linear map `f`.
|
Submodule.map_iSup
theorem Submodule.map_iSup :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂]
[inst_8 : RingHomSurjective σ₁₂] {ι : Sort u_10} (f : F) (p : ι → Submodule R M),
Submodule.map f (⨆ i, p i) = ⨆ i, Submodule.map f (p i)
The `Submodule.map_iSup` theorem states that for given types `R`, `R₂`, `M`, `M₂`, and `F`, together with instances of `Semiring R`, `Semiring R₂`, `AddCommMonoid M`, `AddCommMonoid M₂`, `Module R M`, `Module R₂ M₂`, `FunLike F M M₂`, `SemilinearMapClass F σ₁₂ M M₂`, and `RingHomSurjective σ₁₂`; a ring homomorphism `σ₁₂ : R →+* R₂`; a variable `f` of type `F`; and a family of submodules `p : ι → Submodule R M` indexed by `ι`, the image of the join (`⨆`) of all submodules `p i` under the map `f` is equal to the join of the images of each individual submodule `p i` under the map `f`. In mathematical terms, it asserts that mapping (with `f`) respects the join operation in the lattice of submodules.
More concisely: For a ring homomorphism `σ₁₂` between semirings `R` and `R₂`, and for submodules `p i` of `M` indexed by `ι`, the image of the join (⨆) of `p i` under the semilinear map `f : M → M₂` is equal to the join of the images of each `p i` under `f`.
|
Submodule.map_equiv_eq_comap_symm
theorem Submodule.map_equiv_eq_comap_symm :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂]
(e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M), Submodule.map (↑e) K = Submodule.comap (↑e.symm) K
The theorem `Submodule.map_equiv_eq_comap_symm` states that for any two semi-rings `R` and `R₂`, with associated `AddCommMonoid` structures `M` and `M₂` and also Module structures over `R` and `R₂`, and given two ring homomorphisms `τ₁₂` and `τ₂₁` between these rings that form an inverse pair, then for any linear equivalence `e` between `M` and `M₂` and a submodule `K` of `M`, the image of `K` under the map induced by `e` is equal to the inverse image of `K` under the map induced by the inverse of `e`.
More concisely: For any semi-rings R and R₂, ring homomorphisms τ₁₂ and τ₂₁ forming an inverse pair, Module structures M and M₂ over R and R₂, and linear equivalence e between M and M₂, the image of a submodule K of M under e equals the inverse image of K under e⁻¹.
|
Mathlib.Algebra.Module.Submodule.Map._auxLemma.1
theorem Mathlib.Algebra.Module.Submodule.Map._auxLemma.1 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} [inst_6 : RingHomSurjective σ₁₂] {F : Type u_9} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂},
(x ∈ Submodule.map f p) = ∃ y ∈ p, f y = x
This theorem states that for all types `R`, `R₂`, `M`, `M₂`, and `F`, given the instances of `R` and `R₂` as semirings, `M` and `M₂` as additive commutative monoids, `M` as a module over `R`, `M₂` as a module over `R₂`, a ring homomorphism `σ₁₂` from `R` to `R₂` which is surjective, `F` as a type that behaves like a function from `M` to `M₂`, and `F` as a semilinear map class with respect to `σ₁₂`, `M`, and `M₂`, and given an element `f` of type `F`, a submodule `p` of `M`, and an element `x` of `M₂`, then `x` is in the image of the submodule `p` under the function `f` if and only if there exists an element `y` in `p` such that `f(y) = x`.
In other words, it is characterizing the elements of the image of a submodule under a (semi)linear map in terms of elements of the submodule itself.
More concisely: For a surjective ring homomorphism σ₁₂ between semirings R and R₂, a semilinear map F from an additive commutative monoid M (a module over R) to another additive commutative monoid M₂, and any submodule p of M, an element x in M₂ is in the image of p under F if and only if there exists y in p such that F(y) = x.
|
Submodule.comap_mono
theorem Submodule.comap_mono :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {f : F}
{q q' : Submodule R₂ M₂}, q ≤ q' → Submodule.comap f q ≤ Submodule.comap f q'
The theorem `Submodule.comap_mono` states that for any semirings `R` and `R₂`, additive 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` that acts like a function from `M` to `M₂`, and a semilinear map from `M` to `M₂` over `R` and `R₂` via `σ₁₂` and `f`, if a submodule `q` of the module `M₂` over `R₂` is a subset of another submodule `q'`, then the preimage of `q` under `f` is a subset of the preimage of `q'` under `f`. Here, the preimage of a submodule under a function is the set of all elements in the domain that map to elements in the submodule. This theorem demonstrates the "monotonicity" of the `comap` (preimage) operation.
More concisely: If `f` is a semilinear map from an additive commutative `R`-module `M` to an additive commutative `R₂`-module `M₂`, `σ₁₂` is a ring homomorphism from `R` to `R₂`, `q` is a submodule of `M₂`, and `q'` is a submodule of `M₂` containing `q`, then `f⁻¹(q)` is a submodule of `M` and is contained in `f⁻¹(q')`.
|
Submodule.mem_map
theorem Submodule.mem_map :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} [inst_6 : RingHomSurjective σ₁₂] {F : Type u_9} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂},
x ∈ Submodule.map f p ↔ ∃ y ∈ p, f y = x
This theorem, `Submodule.mem_map`, asserts a property about mappings between submodules. Specifically, for all rings `R` and `R₂`, modules `M` and `M₂`, a semiring structure on `R` and `R₂`, an addition commutative monoid structure on `M` and `M₂`, a module structure over `R` on `M` and over `R₂` on `M₂`, a ring homomorphism `σ₁₂`, a function `f` of type `F` that behaves like a function from `M` to `M₂` (as defined by the `FunLike` class), and a semilinear map structure on `f` in accordance with `σ₁₂`, the theorem states that an element `x` in the module `M₂` is in the image of a submodule `p` under the map `f` if and only if there exists an element `y` in `p` such that `f y = x`. This defines the membership of the image of a submodule under a function in terms of preimages under that function.
More concisely: For submodules `p` of modules `M` and `M₂`, a ring homomorphism `σ₁₂` between rings `R` and `R₂`, a semilinear map `f` from `M` to `M₂` in accordance with `σ₁₂`, and any `x` in `M₂`, `x` is in the image of `p` under `f` if and only if there exists `y` in `p` such that `f(y) = x`.
|
Mathlib.Algebra.Module.Submodule.Map._auxLemma.4
theorem Mathlib.Algebra.Module.Submodule.Map._auxLemma.4 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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₂} {x : M} {F : Type u_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂] {f : F}
{p : Submodule R₂ M₂}, (x ∈ Submodule.comap f p) = (f x ∈ p)
This theorem, `Mathlib.Algebra.Module.Submodule.Map._auxLemma.4`, states that for two semirings `R` and `R₂`, two additive commutative monoids `M` and `M₂`, which are also modules over `R` and `R₂` respectively, and a function `f` of type `F` that is a semilinear map between `M` and `M₂` with respect to a ring homomorphism `σ₁₂` from `R` to `R₂`, then for any element `x` from `M` and a submodule `p` of `M₂` over `R₂`, `x` is in the preimage of `p` under `f` if and only if the image of `x` under `f` is in `p`. This is essentially a characterization of the preimage of a set under a function in terms of the elements of the set and the function.
More concisely: For semirings R and R₂, modules M and M₂ over them, a ring homomorphism σ₁₂ from R to R₂, and a semilinear map f of type F from M to M₂, if x is an element of M and p is a submodule of M₂, then x is in the preimage of p under f if and only if the image of x under f is in p.
|
Submodule.comap_map_eq_of_injective
theorem Submodule.comap_map_eq_of_injective :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {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_9} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F σ₁₂ M M₂]
[inst_8 : RingHomSurjective σ₁₂] {f : F},
Function.Injective ⇑f → ∀ (p : Submodule R M), Submodule.comap f (Submodule.map f p) = p
The theorem `Submodule.comap_map_eq_of_injective` states that for any two types `R` and `R₂` that form semirings, any two types `M` and `M₂` that form additive commutative monoids and are modules over `R` and `R₂` respectively, a ring homomorphism `σ₁₂` from `R` to `R₂` that is surjective, a type `F` that is a function-like from `M` to `M₂`, and a semilinear map from `F` to `σ₁₂` in the context of `M` and `M₂`. Given any function `f` of type `F` that is injective and any submodule `p` of `M`, the submodule obtained by first mapping `p` using `f` and then performing the comap operation of `f` on the result equals `p`.
In even more layman's terms, if you have an injective function and you apply it to a submodule, then 'undo' the function using a comap operation, you get your original submodule back. This is a kind of 'inverse operation' property for injective functions and submodules.
More concisely: For any injective semilinear map `F` from an additive commutative monoid `M` (a `R`-module) to an additive commutative monoid `M₂` (an `R₂`-module), and any surjective ring homomorphism `σ₁₂` from `R` to `R₂`, if `p` is a submodule of `M`, then `(map F '' p) = comap F '' p`.
|