Documentation

Mathlib.LinearAlgebra.Dimension.Constructions

Rank of various constructions #

Main statements #

For free modules, we have

Lemmas for ranks of submodules and subalgebras are also provided. We have finrank variants for most lemmas as well.

theorem LinearIndependent.sum_elim_of_quotient {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {M' : Submodule R M} {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁M'} (hf : LinearIndependent R f) (g : ι₂M) (hg : LinearIndependent R (Submodule.Quotient.mk g)) :
LinearIndependent R (Sum.elim (fun (x : ι₁) => (f x)) g)
theorem LinearIndependent.union_of_quotient {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {M' : Submodule R M} {s : Set M} (hs : s M') (hs' : LinearIndependent (ι := s) R Subtype.val) {t : Set M} (ht : LinearIndependent (ι := t) R (Submodule.Quotient.mk Subtype.val)) :
LinearIndependent (ι := (s t)) R Subtype.val
theorem rank_quotient_add_rank_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] (M' : Submodule R M) :
theorem rank_quotient_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) :
theorem rank_quotient_eq_of_le_torsion {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {M' : Submodule R M} (hN : M' Submodule.torsion R M) :
@[simp]
@[simp]
theorem finrank_ulift {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :
theorem rank_add_rank_le_rank_prod (R : Type u) (M : Type v) {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [Nontrivial R] :
Module.rank R M + Module.rank R M₁ Module.rank R (M × M₁)
@[simp]

If M and M' are free, then the rank of M × M' is (Module.rank R M).lift + (Module.rank R M').lift.

theorem rank_prod' {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [StrongRankCondition R] [Module.Free R M] [Module.Free R M₁] :
Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

If M and M' are free (and lie in the same universe), the rank of M × M' is (Module.rank R M) + (Module.rank R M').

@[simp]
theorem Module.finrank_prod {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] [StrongRankCondition R] [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] :

The finrank of M × M' is (finrank R M) + (finrank R M').

theorem rank_finsupp' (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Free R M] (ι : Type v) :

The rank of (ι →₀ R) is (#ι).lift.

theorem rank_finsupp_self' (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type u} :

If R and ι lie in the same universe, the rank of (ι →₀ R) is # ι.

@[simp]
theorem rank_directSum (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} (M : ιType w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] :
Module.rank R (DirectSum ι fun (i : ι) => M i) = Cardinal.sum fun (i : ι) => Module.rank R (M i)

The rank of the direct sum is the sum of the ranks.

@[simp]

If m and n are finite, the rank of m × n matrices over a module M is (#m).lift * (#n).lift * rank R M.

@[simp]

If m and n are finite and lie in the same universe, the rank of m × n matrices over a module M is (#m * #n).lift * rank R M.

If m and n are finite, the rank of m × n matrices is (#m).lift * (#n).lift.

If m and n are finite and lie in the same universe, the rank of m × n matrices is (#n * #m).lift.

theorem rank_matrix'' (R : Type u) [Ring R] [StrongRankCondition R] (m : Type u) (n : Type u) [Finite m] [Finite n] :

If m and n are finite and lie in the same universe as R, the rank of m × n matrices is # m * # n.

@[simp]
theorem Module.finrank_finsupp (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Free R M] {ι : Type v} [Fintype ι] :
@[simp]

The finrank of (ι →₀ R) is Fintype.card ι.

@[simp]
theorem Module.finrank_directSum (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] (M : ιType w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] :
Module.finrank R (DirectSum ι fun (i : ι) => M i) = i : ι, Module.finrank R (M i)

The finrank of the direct sum is the sum of the finranks.

theorem Module.finrank_matrix (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Free R M] (m : Type u_2) (n : Type u_3) [Fintype m] [Fintype n] :

If m and n are Fintype, the finrank of m × n matrices over a module M is (Fintype.card m) * (Fintype.card n) * finrank R M.

@[simp]
theorem rank_pi {R : Type u} {η : Type u₁'} {φ : ηType u_1} [Ring R] [StrongRankCondition R] [(i : η) → AddCommGroup (φ i)] [(i : η) → Module R (φ i)] [∀ (i : η), Module.Free R (φ i)] [Finite η] :
Module.rank R ((i : η) → φ i) = Cardinal.sum fun (i : η) => Module.rank R (φ i)

The rank of a finite product of free modules is the sum of the ranks.

theorem Module.finrank_pi (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] :
Module.finrank R (ιR) = Fintype.card ι

The finrank of (ι → R) is Fintype.card ι.

theorem Module.finrank_pi_fintype (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] {M : ιType w} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] :
Module.finrank R ((i : ι) → M i) = i : ι, Module.finrank R (M i)

The finrank of a finite product is the sum of the finranks.

theorem rank_fun {R : Type u} [Ring R] [StrongRankCondition R] {M : Type u} {η : Type u} [Fintype η] [AddCommGroup M] [Module R M] [Module.Free R M] :
Module.rank R (ηM) = (Fintype.card η) * Module.rank R M
theorem rank_fun_eq_lift_mul {R : Type u} {M : Type v} {η : Type u₁'} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Free R M] [Fintype η] :
theorem rank_fun' {R : Type u} {η : Type u₁'} [Ring R] [StrongRankCondition R] [Fintype η] :
Module.rank R (ηR) = (Fintype.card η)
theorem rank_fin_fun {R : Type u} [Ring R] [StrongRankCondition R] (n : ) :
Module.rank R (Fin nR) = n
@[simp]
theorem Module.finrank_fintype_fun_eq_card (R : Type u) {η : Type u₁'} [Ring R] [StrongRankCondition R] [Fintype η] :
Module.finrank R (ηR) = Fintype.card η

The vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.

theorem Module.finrank_fin_fun (R : Type u) [Ring R] [StrongRankCondition R] {n : } :
Module.finrank R (Fin nR) = n

The vector space of functions on Fin n has finrank equal to n.

def finDimVectorspaceEquiv {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Free R M] (n : ) (hn : Module.rank R M = n) :
M ≃ₗ[R] Fin nR

An n-dimensional R-vector space is equivalent to Fin n → R.

Equations
Instances For
    @[simp]

    The S-rank of M ⊗[R] M' is (Module.rank S M).lift * (Module.rank R M').lift.

    theorem rank_tensorProduct' {R : Type u} {S : Type u} {M : Type v} {M₁ : Type v} [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [StrongRankCondition R] [StrongRankCondition S] [Module S M] [Module S M₁] [Module.Free S M₁] [Algebra S R] [IsScalarTower S R M] [Module.Free R M] :

    If M and M' lie in the same universe, the S-rank of M ⊗[R] M' is (Module.rank S M) * (Module.rank R M').

    @[simp]
    theorem Module.finrank_tensorProduct {R : Type u} {S : Type u} {M : Type v} {M' : Type v'} [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M'] [Module R M] [StrongRankCondition R] [StrongRankCondition S] [Module S M] [Module S M'] [Module.Free S M'] [Algebra S R] [IsScalarTower S R M] [Module.Free R M] :

    The S-finrank of M ⊗[R] M' is (finrank S M) * (finrank R M').

    theorem Submodule.lt_of_le_of_finrank_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} (le : s t) (lt : Module.finrank R s < Module.finrank R t) :
    s < t
    theorem Submodule.lt_top_of_finrank_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} (lt : Module.finrank R s < Module.finrank R M) :
    s <

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

    The dimension of a quotient is bounded by the dimension of the ambient space.

    theorem Submodule.finrank_map_le {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [StrongRankCondition R] [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] :

    Pushforwards of finite submodules have a smaller finrank.

    theorem Submodule.finrank_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Submodule R M} {t : Submodule R M} [Module.Finite R t] (hst : s t) :
    @[deprecated Submodule.finrank_mono]
    theorem Submodule.finrank_le_finrank_of_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Submodule R M} {t : Submodule R M} [Module.Finite R t] (hst : s t) :

    Alias of Submodule.finrank_mono.

    theorem rank_span_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] (s : Set M) :
    theorem rank_span_finset_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] (s : Finset M) :
    Module.rank R (Submodule.span R s) s.card
    noncomputable def Set.finrank (R : Type u) {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (s : Set M) :

    The rank of a set of vectors as a natural number.

    Equations
    Instances For
      theorem finrank_span_le_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] (s : Set M) [Fintype s] :
      Module.finrank R (Submodule.span R s) s.toFinset.card
      theorem finrank_span_finset_le_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] (s : Finset M) :
      Set.finrank R s s.card
      theorem finrank_range_le_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_2} [Fintype ι] (b : ιM) :
      theorem finrank_span_eq_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Nontrivial R] {ι : Type u_2} [Fintype ι] {b : ιM} (hb : LinearIndependent R b) :
      theorem finrank_span_set_eq_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Set M} [Fintype s] (hs : LinearIndependent R Subtype.val) :
      Module.finrank R (Submodule.span R s) = s.toFinset.card
      theorem finrank_span_finset_eq_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Finset M} (hs : LinearIndependent R Subtype.val) :
      Module.finrank R (Submodule.span R s) = s.card
      theorem span_lt_of_subset_of_card_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Set M} [Fintype s] {t : Submodule R M} (subset : s t) (card_lt : s.toFinset.card < Module.finrank R t) :
      theorem span_lt_top_of_card_lt_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Set M} [Fintype s] (card_lt : s.toFinset.card < Module.finrank R M) :
      theorem finrank_le_of_span_eq_top {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_2} [Fintype ι] {v : ιM} (hv : Submodule.span R (Set.range v) = ) :
      @[simp]
      theorem Subalgebra.rank_toSubmodule {F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] (S : Subalgebra F E) :
      Module.rank F (Subalgebra.toSubmodule S) = Module.rank F S
      @[simp]
      theorem Subalgebra.finrank_toSubmodule {F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] (S : Subalgebra F E) :
      Module.finrank F (Subalgebra.toSubmodule S) = Module.finrank F S
      theorem Subalgebra.rank_top {F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] :
      @[simp]
      theorem Subalgebra.rank_bot {F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] [StrongRankCondition F] [NoZeroSMulDivisors F E] [Nontrivial E] :
      @[simp]