The rank of a linear map

Main Definition

• LinearMap.rank: The rank of a linear map.

@[reducible, inline]

abbrev LinearMap.rank {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f : V →ₗ[K] V') : Cardinal.{v'}

rank f is the rank of a LinearMap f, defined as the dimension of f.range.

theorem LinearMap.rank_le_range {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f : V →ₗ[K] V') : f.rank ≤ Module.rank K V'

theorem LinearMap.rank_le_domain {K : Type u} {V V₁ : Type v} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) : f.rank ≤ Module.rank K V

@[simp]

theorem LinearMap.rank_zero {K : Type u} {V : Type v} {V' : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [Nontrivial K] : rank 0 = 0

theorem LinearMap.rank_comp_le_left {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : (f ∘ₗ g).rank ≤ f.rank

theorem LinearMap.lift_rank_comp_le_right {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ Cardinal.lift.{v'', v'} g.rank

theorem LinearMap.lift_rank_comp_le {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V''] [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 rank of the composition of two maps is less than the minimum of their ranks.

theorem LinearMap.rank_comp_le_right {K : Type u} {V : Type v} {V' V'₁ : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : (f ∘ₗ g).rank ≤ g.rank

theorem LinearMap.rank_comp_le {K : Type u} {V : Type v} {V' V'₁ : Type v'} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] [AddCommGroup V'₁] [Module K V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : (f ∘ₗ g).rank ≤ min f.rank g.rank

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 LinearMap.rank_add_le {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] (f g : V →ₗ[K] V') : (f + g).rank ≤ f.rank + g.rank

theorem LinearMap.rank_finset_sum_le {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {η : Type u_1} (s : Finset η) (f : η → V →ₗ[K] V') : (∑ d ∈ s, f d).rank ≤ ∑ d ∈ s, (f d).rank

theorem LinearMap.le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {c : Cardinal.{v'}} {f : V →ₗ[K] V'} : c ≤ f.rank ↔ ∃ (s : Set V), Cardinal.lift.{v', v} (Cardinal.mk ↑s) = Cardinal.lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

theorem LinearMap.le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} {V' : Type v'} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {n : ℕ} {f : V →ₗ[K] V'} : ↑n ≤ f.rank ↔ ∃ (s : Finset V), s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x