@[inline, reducible]
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')
:
rank f is the rank of a LinearMap f, defined as the dimension of f.range.
Equations
- LinearMap.rank f = Module.rank K ↥(LinearMap.range f)
Instances For
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')
:
LinearMap.rank f ≤ Module.rank K V'
theorem
LinearMap.rank_le_domain
{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₁)
:
LinearMap.rank f ≤ 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]
:
LinearMap.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'')
:
LinearMap.rank (f ∘ₗ g) ≤ LinearMap.rank f
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''} (LinearMap.rank (f ∘ₗ g)) ≤ Cardinal.lift.{v'', v'} (LinearMap.rank g)
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''} (LinearMap.rank (f ∘ₗ g)) ≤ min (Cardinal.lift.{v', v''} (LinearMap.rank f)) (Cardinal.lift.{v'', v'} (LinearMap.rank g))
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' : 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'₁)
:
LinearMap.rank (f ∘ₗ g) ≤ LinearMap.rank g
theorem
LinearMap.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'₁)
:
LinearMap.rank (f ∘ₗ g) ≤ min (LinearMap.rank f) (LinearMap.rank g)
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 : V →ₗ[K] V')
(g : V →ₗ[K] V')
:
LinearMap.rank (f + g) ≤ LinearMap.rank f + LinearMap.rank g
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')
:
LinearMap.rank (Finset.sum s fun (d : η) => f d) ≤ Finset.sum s fun (d : η) => LinearMap.rank (f d)
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 ≤ LinearMap.rank f ↔ ∃ (s : Set V),
Cardinal.lift.{v', v} (Cardinal.mk ↑s) = Cardinal.lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x
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 ≤ LinearMap.rank f ↔ ∃ (s : Finset V), s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x