LinearMap.lift_rank_comp_le
theorem LinearMap.lift_rank_comp_le :
∀ {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [inst : Ring K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] [inst_5 : AddCommGroup V'']
[inst_6 : Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V''),
Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ min (Cardinal.lift.{v', v''} f.rank) (Cardinal.lift.{v'', v'} g.rank)
The theorem `LinearMap.lift_rank_comp_le` states that for all types `K`, `V`, `V'`, and `V''`, assuming `K` is a ring, `V`, `V'`, and `V''` are additive commutative groups, and `V`, `V'`, and `V''` are `K`-modules, for any two linear maps `g : V →ₗ[K] V'` and `f : V' →ₗ[K] V''`, the rank of the composition of `f` and `g` is less than or equal to the minimum of the ranks of `f` and `g`. Here, `Cardinal.lift.{v', v''} (f ∘ₗ g).rank` represents the rank of the composition of `f` and `g`, `Cardinal.lift.{v', v''} f.rank` is the rank of `f`, and `Cardinal.lift.{v'', v'} g.rank` is the rank of `g`. The rank is lifted to the maximum of the corresponding universes of `V'` and `V''`.
More concisely: For any ring K and additive commutative groups/K-modules V, V', and V'', the rank of the composition of linear maps g : V --> V' and f : V' --> V'' is less than or equal to the minimum rank of g and f.
|
LinearMap.rank_comp_le
theorem LinearMap.rank_comp_le :
∀ {K : Type u} {V : Type v} {V' V'₁ : Type v'} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : AddCommGroup V'] [inst_4 : Module K V'] [inst_5 : AddCommGroup V'₁] [inst_6 : Module K V'₁]
(g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁), (f ∘ₗ g).rank ≤ min f.rank g.rank
This theorem states that for any two linear maps, `f` and `g`, defined over a ring `K` and vector spaces `V`, `V'`, and `V'₁`, the rank of the composition of `f` and `g` (i.e., `f ∘ₗ g`) is less than or equal to the minimum of the ranks of `f` and `g`. This is a fundamental property of linear maps in linear algebra. Note that there is a universe-polymorphic version of this theorem named `lift_rank_comp_le`.
More concisely: The rank of the composition of linear maps `f` and `g` over rings `K` and vector spaces `V`, `V'`, and `V'₁` is less than or equal to the minimum of the ranks of `f` and `g`.
|
LinearMap.lift_rank_comp_le_right
theorem LinearMap.lift_rank_comp_le_right :
∀ {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [inst : Ring K] [inst_1 : AddCommGroup V]
[inst_2 : Module K V] [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] [inst_5 : AddCommGroup V'']
[inst_6 : Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V''),
Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ Cardinal.lift.{v'', v'} g.rank
The theorem `LinearMap.lift_rank_comp_le_right` states that: For any ring `K` and `K`-modules `V`, `V'`, and `V''`, given two linear maps `g : V →ₗ[K] V'` and `f : V' →ₗ[K] V''`, the lift (to the maximum of the universes of `V'` and `V''`) of the rank of the composition of the two maps (i.e., `f ∘ₗ g`) is less than or equal to the lift (to the maximum of the universes of `V''` and `V'`) of the rank of the linear map `g`. In mathematical terms, if we denote the rank of a linear map using the function `rank(.)`, this theorem can be expressed as: $\forall f,g: \text{rank}(f \circ g) \leq \text{rank}(g)$. This result is related to the dimension theory of vector spaces and the properties of linear transformations.
More concisely: The rank of the composition of two linear maps is less than or equal to the rank of the second map.
|