Documentation

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Finite dimensional vector spaces #

This file contains some further development of finite dimensional vector spaces, their dimensions, and linear maps on such spaces.

Definitions are in Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean and results that require fewer imports are in Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean.

theorem Submodule.finrank_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Submodule K V} (h : s ) :

The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.

See also Submodule.length_lt.

theorem Submodule.finrank_sup_add_finrank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Submodule K V) [FiniteDimensional K s] [FiniteDimensional K t] :
Module.finrank K (st) + Module.finrank K (st) = Module.finrank K s + Module.finrank K t

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

theorem Submodule.eq_top_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s t : Submodule K V) (hdim : Module.finrank K V Module.finrank K s + Module.finrank K t) (hdisjoint : Disjoint s t) :
st =
noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {p : Subspace K V} {q : Subspace K V₂} (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) :
(V p) ≃ₗ[K] V₂ q

Given isomorphic subspaces p q of vector spaces V and V₁ respectively, p.quotient is isomorphic to q.quotient.

Equations
Instances For
    noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {p q : Subspace K V} (f : (V p) ≃ₗ[K] q) :
    (V q) ≃ₗ[K] p

    Given the subspaces p q, if p.quotient ≃ₗ[K] q, then q.quotient ≃ₗ[K] p

    Equations
    Instances For
      theorem LinearMap.finrank_range_add_finrank_ker {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) :

      rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.

      theorem LinearMap.ker_ne_bot_of_finrank_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (h : Module.finrank K V₂ < Module.finrank K V) :
      noncomputable def LinearMap.linearEquivOfInjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂) (hf : Function.Injective f) (hdim : Module.finrank K V = Module.finrank K V₂) :
      V ≃ₗ[K] V₂

      Given a linear map f between two vector spaces with the same dimension, if ker f = ⊥ then linearEquivOfInjective is the induced isomorphism between the two vector spaces.

      Equations
      Instances For
        @[simp]
        theorem LinearMap.linearEquivOfInjective_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (hf : Function.Injective f) (hdim : Module.finrank K V = Module.finrank K V₂) (x : V) :
        (f.linearEquivOfInjective hf hdim) x = f x
        theorem Submodule.finrank_lt_finrank_of_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Submodule K V} [FiniteDimensional K t] (hst : s < t) :
        theorem LinearIndependent.span_eq_top_of_card_eq_finrank' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Fintype ι] [FiniteDimensional K V] {b : ιV} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) :
        theorem LinearIndependent.span_eq_top_of_card_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ιV} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) :
        noncomputable def basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ιV} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) :
        Basis ι K V

        A linear independent family of finrank K V vectors forms a basis.

        Equations
        Instances For
          @[simp]
          theorem basisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ιV} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) (a✝ : V) :
          @[simp]
          theorem coe_basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ιV} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) :
          noncomputable def basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {ι : Type u_1} [Fintype ι] [Decidable (Nonempty ι)] {b : ιιK} (hb : LinearIndependent K b) :
          Basis ι K (ιK)

          In a vector space ι → K, a linear independent family indexed by ι is a basis.

          Equations
          Instances For
            @[simp]
            theorem coe_basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {ι : Type u_1} [Fintype ι] {b : ιιK} (hb : LinearIndependent K b) :
            noncomputable def finsetBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) :
            Basis { x : V // x s } K V

            A linear independent finset of finrank K V vectors forms a basis.

            Equations
            Instances For
              noncomputable def setBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty s] [Fintype s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) :
              Basis (↑s) K V

              A linear independent set of finrank K V vectors forms a basis.

              Equations
              Instances For

                We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.

                theorem is_simple_module_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Type u_1} [Semiring A] [Module A V] [SMul K A] [IsScalarTower K A V] (h : Module.finrank K V = 1) :

                Any K-algebra module that is 1-dimensional over K is simple.

                theorem Subalgebra.isSimpleOrder_of_finrank {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] (hr : Module.finrank F E = 2) :
                theorem Module.End.ker_pow_eq_ker_pow_finrank_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} {m : } (hm : finrank K V m) :