Documentation

Mathlib.LinearAlgebra.FiniteDimensional

Finite dimensional vector spaces #

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

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

In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding quotient add up to the dimension of the space.

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.

theorem Submodule.finrank_sup_add_finrank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) [FiniteDimensional K s] [FiniteDimensional K t] :
Module.finrank K (s t) + Module.finrank K (s t) = 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 : Submodule K V) (t : Submodule K V) (hdim : Module.finrank K s + Module.finrank K t = Module.finrank K V) (hdisjoint : Disjoint s t) :
s t =
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 : Subspace K V} {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

      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 : Submodule K V} {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) :
        @[deprecated LinearIndependent.span_eq_top_of_card_eq_finrank]
        theorem span_eq_top_of_linearIndependent_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) :

        Alias of LinearIndependent.span_eq_top_of_card_eq_finrank.

        @[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), (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ) a)
        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 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) :
          @[simp]
          theorem finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply {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) :
          ∀ (a : V), (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ) a)
          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
            @[simp]
            theorem coe_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) :
            (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val
            @[simp]
            theorem setBasisOfLinearIndependentOfCardEqFinrank_repr_apply {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) :
            ∀ (a : V), (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ) a)
            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
              @[simp]
              theorem coe_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) :
              (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val

              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) :