LinearPMap.sup_h_of_disjoint
theorem LinearPMap.sup_h_of_disjoint :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] (f g : E →ₗ.[R] F),
Disjoint f.domain g.domain → ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
The theorem `LinearPMap.sup_h_of_disjoint` states that for any ring `R` and any two vector spaces `E` and `F` over `R`, given two linear maps `f` and `g` from `E` to `F`, if the domain of `f` is disjoint with the domain of `g`, then for any element `x` in the domain of `f` and any element `y` in the domain of `g`, if `x` and `y` are the same, then the images of `x` under `f` and `y` under `g` are the same. This theorem relates to the infimum (or greatest lower bound) of two elements in a lattice and is a part of the theory of linear partial maps.
More concisely: If two linear maps from one vector space to another have disjoint domains and map the same element to different elements, then they map that element to the same image.
|
LinearPMap.le_of_le_graph
theorem LinearPMap.le_of_le_graph :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F}, f.graph ≤ g.graph → f ≤ g
The theorem `LinearPMap.le_of_le_graph` states that for any ring `R`, and any two linear maps `f` and `g` from a module `E` over `R` to a module `F` over `R` (where `E` and `F` are also additive commutative groups), if the graph of `f` is a sub-module of (or equal to) the graph of `g`, then `f` is less than or equal to `g`. The 'graph' of a linear map here refers to the set of tuples `(x, f(x))` for all `x` in the domain of `f`.
More concisely: If `f` and `g` are linear maps from module `E` to module `F` over ring `R`, and the graph of `f` is contained in the graph of `g`, then `f ≤ g`.
|
LinearPMap.le_sSup
theorem LinearPMap.le_sSup :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (fun x x_1 => x ≤ x_1) c)
{f : E →ₗ.[R] F}, f ∈ c → f ≤ LinearPMap.sSup c hc
The theorem `LinearPMap.le_sSup` states that for any ring `R` and modules `E` and `F` over the ring `R`, given a set `c` of linear mappings from `E` to `F`, if `c` is directed with respect to the "less than or equal to" relation (meaning for any two mappings in `c`, there is another mapping in `c` that is greater than or equal to both), then any specific mapping `f` in `c` is less than or equal to the supremum of the set `c`, where the supremum is defined by `LinearPMap.sSup`.
More concisely: For any ring `R` and modules `E` and `F` over `R`, if `c` is a directed set of linear mappings from `E` to `F`, then for all `f` in `c`, we have `f ≤ LinearPMap.sSup c`.
|
LinearPMap.neg_graph
theorem LinearPMap.neg_graph :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
(-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
This theorem states that for any given ring `R`, and any modules `E` and `F` over `R` with the addition operation being a commutative group in `E` and `F`, if `f` is a linear map from `E` to `F`, then the graph of the negation of `f` is equal to the image of the graph of `f` under the map induced by the identity map on `E` and the negation of the identity map on `F`. In mathematical terms, if $f : E \to F$ is a linear map, then the graph of $-f$ is the image of the graph of $f$ under the map $(\text{id}, -\text{id}) : E \times F \to E \times F$.
More concisely: For any linear map $f$ between modules $E$ and $F$ over a ring $R$ with commutative addition, the graph of the negation of $f$ is equal to the image of the graph of $f$ under the map $(id, -id): E \times F \to E \times F$.
|
LinearPMap.smul_graph
theorem LinearPMap.smul_graph :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] {M : Type u_5} [inst_5 : Monoid M] [inst_6 : DistribMulAction M F]
[inst_7 : SMulCommClass R M F] (f : E →ₗ.[R] F) (z : M),
(z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
The theorem `LinearPMap.smul_graph` states that for any ring `R`, additively commutative group `E` and `F` modules over `R`, monoid `M` and an distributive multiplication action of `M` on `F` that also commutes with the scalar multiplication of `R` on `F`, for any linear map `f` from `E` to `F` and any element `z` in `M`, the graph of the scaled linear map `z • f` is equal to the submodule obtained by mapping the graph of `f` via the product of the identity map and the scaled identity map `z • LinearMap.id`. In simpler terms, the theorem relates the graph of a scaled linear map to the graph of the original map transformed by an operation involving the scaling factor.
More concisely: Given a ring `R`, additively commutative groups `E` and `F`, `R`-modules `E` and `F`, a monoid `M` with distributive multiaction on `F` commuting with scalar multiplication, a linear map `f : E → F`, and an element `z ∈ M`, the graphs of `z • f` and `f` are equal as submodules of `E × F` under the product of the identity maps on `E` and `F` with `z • idₐF` and `idₐE` respectively.
|
LinearPMap.map_zero
theorem LinearPMap.map_zero :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F), ↑f 0 = 0
This theorem states that for any ring `R`, and any two modules `E` and `F` over `R`, if we have a linear map `f` from `E` to `F`, then the image of the zero vector in `E` under `f` is the zero vector in `F`. This property is a characteristic of linear maps in mathematics, where the map of zero always yields zero.
More concisely: For any ring `R`, and modules `E` and `F` over `R`, if `f` is a linear map from `E` to `F`, then `f(0_E) = 0_F`.
|
LinearPMap.graph_fst_eq_zero_snd
theorem LinearPMap.graph_fst_eq_zero_snd :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x : E} {x' : F},
(x, x') ∈ f.graph → x = 0 → x' = 0
The theorem states that, given a function `f` that is a linear map from a module `E` over a ring `R` to another module `F` over the same ring `R`, if a pair `(x, x')` is in the graph of `f` and `x` equals to zero, then `x'` must also equal to zero. In other words, if the input of `f` is zero (i.e., `f 0`), the output must also be zero. This is essentially saying that the linear map `f` preserves the zero element, a key characteristic of linear maps.
More concisely: If `f` is a linear map from module `E` to module `F` over ring `R`, then `f (0_E) = 0_F`.
|
LinearPMap.mem_graph
theorem LinearPMap.mem_graph :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) (x : ↥f.domain), (↑x, ↑f x) ∈ f.graph
This theorem asserts that for any linear map `f` from a module `E` over a ring `R` to a module `F` over the same ring `R`, and for any element `x` in the domain of `f`, the tuple consisting of `x` and its image under `f` (`f x`) is a member of the graph of `f`. Here, the graph of a function is the set of all pairs `(x, y)`, where `y` is the image of `x` under the function.
More concisely: For any linear map `f` from module `E` to module `F` over ring `R`, and for all `x` in `E`, the tuple `(x, f x)` belongs to the graph of `f`.
|
LinearPMap.mem_inverse_graph_snd_eq_zero
theorem LinearPMap.mem_inverse_graph_snd_eq_zero :
∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
[inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F},
LinearMap.ker f.toFun = ⊥ → ∀ x ∈ Submodule.map (LinearEquiv.prodComm R E F) f.graph, x.1 = 0 → x.2 = 0
This theorem states that for any ring `R`, and any two modules `E` and `F` over this ring (where `E` and `F` are both additive commutative groups), given a linear mapping `f` from `E` to `F` such that the kernel of `f` is trivial (i.e. the kernel only contains the zero element), for any element `x` in the image of the product commutative linear equivalence of `f`'s graph, if the first component of `x` is zero, then its second component must also be zero. In other words, this theorem says that the graph of the inverse of a linear mapping with trivial kernel generates a partial linear map whose second component is zero whenever the first component is zero.
More concisely: If `f` is a linear map between additive commutative groups `E` and `F` over a ring `R` with trivial kernel, then the second component of every element in the graph of `f`'s inverse is zero whenever the first component is zero.
|