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.

source
šŸ“ coverage
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 ā‰  āŠ¤) :
Module.finrank K ā†„s < Module.finrank K V

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

See also Submodule.length_lt.

source
šŸ“ coverage
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 ā†„(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

source
šŸ“ coverage
theorem Submodule.finrank_add_le_finrank_add_finrank {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 ā†„(s āŠ” t) ā‰¤ Module.finrank K ā†„s + Module.finrank K ā†„t
source
šŸ“ coverage
theorem Submodule.finrank_add_finrank_le_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s t : Submodule K V} (hdisjoint : Disjoint s t) :
Module.finrank K ā†„s + Module.finrank K ā†„t ā‰¤ Module.finrank K V
source
šŸ“ coverage
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) :
s āŠ” t = āŠ¤
source
šŸ“ coverage
theorem Submodule.isCompl_iff_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) :
IsCompl s t ā†” Disjoint s t
source
šŸ“ coverage
theorem Submodule.sup_span_singleton_eq_top_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Module.Finite K V] {W : Submodule K V} {v : V} (hv : v āˆ‰ W) :
W āŠ” K āˆ™ v = āŠ¤ ā†” Module.finrank K (V ā§ø W) = 1
source
šŸ”ø coverage
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.

Instances For
    source
    šŸ”ø coverage
    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

    Instances For
      source
      šŸ“ coverage
      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ā‚‚) :
      Module.finrank K ā†„f.range + Module.finrank K ā†„f.ker = Module.finrank 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.

      source
      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) :
      f.ker ā‰  āŠ„
      source
      šŸ“ coverage
      theorem LinearMap.injective_iff_surjective_of_finrank_eq_finrank {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ā‚‚] (H : Module.finrank K V = Module.finrank K Vā‚‚) {f : V ā†’ā‚—[K] Vā‚‚} :
      Function.Injective ā‡‘f ā†” Function.Surjective ā‡‘f
      source
      šŸ“ coverage
      theorem LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank {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ā‚‚] (H : Module.finrank K V = Module.finrank K Vā‚‚) {f : V ā†’ā‚—[K] Vā‚‚} :
      f.ker = āŠ„ ā†” f.range = āŠ¤
      source
      šŸ”ø coverage
      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.

      Instances For
        source
        šŸ“ coverage
        @[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
        source
        šŸ“ coverage
        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) :
        Module.finrank K ā†„s < Module.finrank K ā†„t
        source
        šŸ“ coverage
        theorem Submodule.finrank_strictMono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] :
        StrictMono fun (s : Submodule K V) => Module.finrank K ā†„s
        source
        šŸ“ coverage
        theorem Submodule.finrank_add_eq_of_isCompl {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) :
        Module.finrank K ā†„U + Module.finrank K ā†„W = Module.finrank K V
        source
        šŸ“ coverage
        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) :
        Submodule.span K (Set.range b) = āŠ¤
        source
        šŸ“ coverage
        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) :
        Submodule.span K (Set.range b) = āŠ¤
        source
        šŸ”ø coverage
        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) :
        Module.Basis Ī¹ K V

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

        Instances For
          source
          šŸ“ coverage
          @[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āœ)
          source
          šŸ“ coverage
          @[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) :
          ā‡‘(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b
          source
          šŸ”ø coverage
          noncomputable def basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {Ī¹ : Type u_1} [Fintype Ī¹] [Decidable (Nonempty Ī¹)] {b : Ī¹ ā†’ Ī¹ ā†’ K} (hb : LinearIndependent K b) :
          Module.Basis Ī¹ K (Ī¹ ā†’ K)

          In a vector space Ī¹ ā†’ K, a linear independent family indexed by Ī¹ is a basis.

          Instances For
            source
            šŸ“ coverage
            @[simp]
            theorem coe_basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {Ī¹ : Type u_1} [Fintype Ī¹] {b : Ī¹ ā†’ Ī¹ ā†’ K} (hb : LinearIndependent K b) :
            ā‡‘(basisOfPiSpaceOfLinearIndependent hb) = b
            source
            šŸ”ø coverage
            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) :
            Module.Basis (ā†„s) K V

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

            Instances For
              source
              šŸ“ coverage
              @[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āœ)
              source
              šŸ“ coverage
              @[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
              source
              šŸ”ø coverage
              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) :
              Module.Basis (ā†‘s) K V

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

              Instances For
                source
                šŸ“ coverage
                @[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āœ)
                source
                šŸ“ coverage
                @[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.

                source
                šŸ“ coverage
                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) :
                IsSimpleOrder (Submodule A V)

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

                source
                šŸ“ coverage
                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) :
                IsSimpleOrder (Subalgebra F E)
                source
                šŸ“ coverage
                theorem Module.End.exists_ker_pow_eq_ker_pow_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) :
                āˆƒ k ā‰¤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
                source
                šŸ“ coverage
                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) :
                LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
                source
                šŸ“ coverage
                theorem Module.End.ker_pow_le_ker_pow_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (m : ā„•) :
                LinearMap.ker (f ^ m) ā‰¤ LinearMap.ker (f ^ finrank K V)