Documentation

Mathlib.LinearAlgebra.Dimension.LinearMap

The rank of a linear map #

Main Definition #

@[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') :

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

Equations
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') :
    f.rank 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₁) :
    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] :
    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'') :
    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'') :

    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'₁) :
    (f ∘ₗ g).rank g.rank
    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'₁) :
    (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 : V →ₗ[K] V') (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') :
    (∑ ds, f d).rank ds, (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 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 f.rank ∃ (s : Finset V), s.card = n LinearIndependent K fun (x : s) => f x