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

      Equations
        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.

          Equations
            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.

              Equations
                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.

                  Equations
                    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.

                      Equations
                        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.

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