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.

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