Mathlib.LinearAlgebra.Dimension.LinearMap

LinearMap.rank abbrev

(f : V →ₗ[K] V') : Cardinal

Full source

/-- `rank f` is the rank of a `LinearMap` `f`, defined as the dimension of `f.range`. -/
abbrev rank (f : V →ₗ[K] V') : Cardinal :=
  Module.rank K (LinearMap.range f)

Definition of the Rank of a Linear Map

Informal description

The rank of a linear map $f \colon V \to V'$ between vector spaces over a field $K$ is defined as the dimension of the range of $f$.

LinearMap.rank_le_range theorem

(f : V →ₗ[K] V') : rank f ≤ Module.rank K V'

Full source

theorem rank_le_range (f : V →ₗ[K] V') : rank f ≤ Module.rank K V' :=
  Submodule.rank_le _

Rank of Linear Map is Bounded by Dimension of Codomain

Informal description

For any linear map $f \colon V \to V'$ between vector spaces over a field $K$, the rank of $f$ is less than or equal to the dimension of the codomain $V'$, i.e., $\text{rank}(f) \leq \dim_K V'$.

LinearMap.rank_le_domain theorem

(f : V →ₗ[K] V₁) : rank f ≤ Module.rank K V

Full source

theorem rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ Module.rank K V :=
  rank_range_le _

Rank of a linear map is bounded by the dimension of its domain

Informal description

For any linear map $f \colon V \to V_1$ between vector spaces over a field $K$, the rank of $f$ is less than or equal to the dimension of the domain vector space $V$.

LinearMap.rank_zero theorem

[Nontrivial K] : rank (0 : V →ₗ[K] V') = 0

Full source

@[simp]
theorem rank_zero [Nontrivial K] : rank (0 : V →ₗ[K] V') = 0 := by
  rw [rank, LinearMap.range_zero, rank_bot]

Rank of the Zero Linear Map is Zero

Informal description

For any nontrivial field $K$ and vector spaces $V$ and $V'$ over $K$, the rank of the zero linear map $0 \colon V \to V'$ is equal to $0$.

LinearMap.rank_comp_le_left theorem

(g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f

Full source

theorem rank_comp_le_left (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f := by
  refine Submodule.rank_mono ?_
  rw [LinearMap.range_comp]
  exact LinearMap.map_le_range

Rank of Composition is Bounded by Left Factor: $\text{rank}(f \circ g) \leq \text{rank}(f)$

Informal description

For any linear maps $g \colon V \to V'$ and $f \colon V' \to V''$ between vector spaces over a field $K$, the rank of the composition $f \circ g$ is less than or equal to the rank of $f$.

LinearMap.lift_rank_comp_le_right theorem

(g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : Cardinal.lift.{v'} (rank (f.comp g)) ≤ Cardinal.lift.{v''} (rank g)

Full source

theorem lift_rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
    Cardinal.lift.{v'} (rank (f.comp g)) ≤ Cardinal.lift.{v''} (rank g) := by
  rw [rank, rank, LinearMap.range_comp]; exact lift_rank_map_le _ _

Rank Inequality for Composition of Linear Maps: $\text{rank}(f \circ g) \leq \text{rank}(g)$

Informal description

Let $K$ be a field, and let $V$, $V'$, $V''$ be vector spaces over $K$. For any linear maps $g \colon V \to V'$ and $f \colon V' \to V''$, the rank of the composition $f \circ g$ is less than or equal to the rank of $g$, where ranks are compared under appropriate cardinal lifts to handle universe level differences.

LinearMap.lift_rank_comp_le theorem

 (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
  Cardinal.lift.{v'} (rank (f.comp g)) ≤ min (Cardinal.lift.{v'} (rank f)) (Cardinal.lift.{v''} (rank g))

Full source

/-- The rank of the composition of two maps is less than the minimum of their ranks. -/
theorem lift_rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
    Cardinal.lift.{v'} (rank (f.comp g)) ≤
      min (Cardinal.lift.{v'} (rank f)) (Cardinal.lift.{v''} (rank g)) :=
  le_min (Cardinal.lift_le.mpr <| rank_comp_le_left _ _) (lift_rank_comp_le_right _ _)

Rank Inequality for Composition: $\text{rank}(f \circ g) \leq \min(\text{rank}(f), \text{rank}(g))$

Informal description

Let $K$ be a field, and let $V$, $V'$, $V''$ be vector spaces over $K$. For any linear maps $g \colon V \to V'$ and $f \colon V' \to V''$, the rank of the composition $f \circ g$ satisfies \[ \text{rank}(f \circ g) \leq \min(\text{rank}(f), \text{rank}(g)), \] where the ranks are compared under appropriate cardinal lifts to handle universe level differences.

LinearMap.rank_comp_le_right theorem

(g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g

Full source

theorem rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g := by
  simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f

Rank Inequality for Composition of Linear Maps: $\text{rank}(f \circ g) \leq \text{rank}(g)$

Informal description

Let $K$ be a field, and let $V$, $V'$, $V'_1$ be vector spaces over $K$. For any linear maps $g \colon V \to V'$ and $f \colon V' \to V'_1$, the rank of the composition $f \circ g$ is less than or equal to the rank of $g$.

LinearMap.rank_comp_le theorem

(g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ min (rank f) (rank g)

Full source

/-- The rank of the composition of two maps is less than the minimum of their ranks.

See `lift_rank_comp_le` for the universe-polymorphic version. -/
theorem rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
    rank (f.comp g) ≤ min (rank f) (rank g) := by
  simpa only [Cardinal.lift_id] using lift_rank_comp_le g f

Rank Inequality for Composition of Linear Maps: $\text{rank}(f \circ g) \leq \min(\text{rank}(f), \text{rank}(g))$

Informal description

Let $K$ be a field, and let $V$, $V'$, $V'_1$ be vector spaces over $K$. For any linear maps $g \colon V \to V'$ and $f \colon V' \to V'_1$, the rank of the composition $f \circ g$ satisfies \[ \text{rank}(f \circ g) \leq \min(\text{rank}(f), \text{rank}(g)). \]

LinearMap.rank_add_le theorem

(f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g

Full source

theorem rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
  calc
    rank (f + g) ≤ Module.rank K (LinearMap.rangeLinearMap.range f ⊔ LinearMap.range g : Submodule K V') := by
      refine Submodule.rank_mono ?_
      exact LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun x =>
        show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩
    _ ≤ rank f + rank g := Submodule.rank_add_le_rank_add_rank _ _

Subadditivity of Rank for Sum of Linear Maps: $\text{rank}(f + g) \leq \text{rank}(f) + \text{rank}(g)$

Informal description

For any two linear maps $f, g \colon V \to V'$ between vector spaces over a field $K$, the rank of their sum satisfies the inequality \[ \text{rank}(f + g) \leq \text{rank}(f) + \text{rank}(g). \]

LinearMap.rank_finset_sum_le theorem

{η} (s : Finset η) (f : η → V →ₗ[K] V') : rank (∑ d ∈ s, f d) ≤ ∑ d ∈ s, rank (f d)

Full source

theorem rank_finset_sum_le {η} (s : Finset η) (f : η → V →ₗ[K] V') :
    rank (∑ d ∈ s, f d) ≤ ∑ d ∈ s, rank (f d) :=
  @Finset.sum_hom_rel _ _ _ _ _ (fun a b => rank a ≤ b) f (fun d => rank (f d)) s
    (le_of_eq rank_zero) fun _ _ _ h => le_trans (rank_add_le _ _) (add_le_add_left h _)

Subadditivity of Rank for Finite Sums of Linear Maps: $\text{rank}(\sum f_d) \leq \sum \text{rank}(f_d)$

Informal description

For any finite set $\eta$ and any family of linear maps $\{f_d \colon V \to V'\}_{d \in \eta}$ between vector spaces over a field $K$, the rank of the sum of the maps satisfies the inequality \[ \text{rank}\left(\sum_{d \in s} f_d\right) \leq \sum_{d \in s} \text{rank}(f_d), \] where $s$ is any finite subset of $\eta$.

LinearMap.le_rank_iff_exists_linearIndependent theorem

 {c : Cardinal} {f : V →ₗ[K] V'} :
  c ≤ rank f ↔ ∃ s : Set V, Cardinal.lift.{v'} #s = Cardinal.lift.{v} c ∧ LinearIndepOn K f s

Full source

theorem le_rank_iff_exists_linearIndependent {c : Cardinal} {f : V →ₗ[K] V'} :
    c ≤ rank f ↔ ∃ s : Set V,
    Cardinal.lift.{v'} #s = Cardinal.lift.{v} c ∧ LinearIndepOn K f s := by
  rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
  have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
  refine ⟨fun h => ?_, ?_⟩
  · rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩
    refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩
    replace fg : ∀ x, f (g x) = x := by
      intro x
      convert congr_arg Subtype.val (fg x)
    replace si : LinearIndepOn K (fun x => f (g x)) s := by
      simpa only [fg] using si.map' _ (ker_subtype _)
    exact si.image_of_comp
  · rintro ⟨s, hsc, si⟩
    have : LinearIndepOn K f.rangeRestrict s :=
      LinearIndependent.of_comp (LinearMap.range f).subtype (by convert si)
    convert this.id_image.cardinal_le_rank
    rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]
    exact injOn_iff_injective.2 this.injective

Cardinality Bound for Linear Independence in the Range of a Linear Map

Informal description

Let $f \colon V \to V'$ be a linear map between vector spaces over a field $K$, and let $c$ be a cardinal number. Then $c \leq \text{rank}(f)$ if and only if there exists a subset $S \subseteq V$ with cardinality $c$ such that the family $\{f(x) \mid x \in S\}$ is linearly independent in $V'$.

LinearMap.le_rank_iff_exists_linearIndependent_finset theorem

 {n : ℕ} {f : V →ₗ[K] V'} : ↑n ≤ rank f ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K fun x : (s : Set V) => f x

Full source

theorem le_rank_iff_exists_linearIndependent_finset {n : ℕ} {f : V →ₗ[K] V'} :
    ↑n ≤ rank f ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K fun x : (s : Set V) => f x := by
  simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
    Cardinal.mk_set_eq_nat_iff_finset]
  constructor
  · rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
    exact ⟨t, rfl, si⟩
  · rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Finite Linear Independence Criterion for Rank of Linear Map

Informal description

For a linear map $f \colon V \to V'$ between vector spaces over a field $K$ and a natural number $n$, the inequality $n \leq \text{rank}(f)$ holds if and only if there exists a finite subset $s \subseteq V$ with $|s| = n$ such that the family $\{f(x) \mid x \in s\}$ is linearly independent in $V'$.

Main Definition