Documentation

Mathlib.LinearAlgebra.Dimension.Free

Rank of free modules #

Main result #

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

The universe polymorphic version of rank_mul_rank below.

theorem rank_mul_rank (F : Type u) (K : Type v) [Ring F] [Ring K] [Module F K] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] (A : Type v) [AddCommGroup A] [Module K A] [Module F A] [IsScalarTower F K A] [Module.Free K A] :

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

This is a simpler version of lift_rank_mul_lift_rank with K and A in the same universe.

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

The rank of a free module M over R is the cardinality of ChooseBasisIndex R M.

The finrank of a free module M over R is the cardinality of ChooseBasisIndex R M.

The rank of a free module M over an infinite scalar ring R is the cardinality of M whenever #R < #M.

Two vector spaces are isomorphic if they have the same dimension.

theorem nonempty_linearEquiv_of_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] (cond : Module.rank R M = Module.rank R M₁) :
Nonempty (M ≃ₗ[R] M₁)

Two vector spaces are isomorphic if they have the same dimension.

Two vector spaces are isomorphic if they have the same dimension.

Equations
Instances For
    def LinearEquiv.ofRankEq {R : Type u} (M : Type v) (M₁ : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] (cond : Module.rank R M = Module.rank R M₁) :
    M ≃ₗ[R] M₁

    Two vector spaces are isomorphic if they have the same dimension.

    Equations
    Instances For

      Two vector spaces are isomorphic if and only if they have the same dimension.

      theorem LinearEquiv.nonempty_equiv_iff_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] :

      Two vector spaces are isomorphic if and only if they have the same dimension.

      Two finite and free modules are isomorphic if they have the same (finite) rank.

      Two finite and free modules are isomorphic if and only if they have the same (finite) rank.

      noncomputable def LinearEquiv.ofFinrankEq {R : Type u} (M : Type v) (M' : Type v') [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] (cond : Module.finrank R M = Module.finrank R M') :
      M ≃ₗ[R] M'

      Two finite and free modules are isomorphic if they have the same (finite) rank.

      Equations
      Instances For

        See rank_lt_aleph0 for the inverse direction without Module.Free R M.

        theorem Module.finite_of_finrank_eq_succ {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {n : } (hn : Module.finrank R M = n.succ) :
        theorem Module.finite_iff_of_rank_eq_nsmul {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {W : Type v} [AddCommGroup W] [Module R W] [Module.Free R W] {n : } (hn : n 0) (hVW : Module.rank R M = n Module.rank R W) :
        noncomputable def Module.finBasis (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] :

        A finite rank free module has a basis indexed by Fin (finrank R M).

        Equations
        Instances For
          noncomputable def Module.finBasisOfFinrankEq (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {n : } (hn : Module.finrank R M = n) :
          Basis (Fin n) R M

          A rank n free module has a basis indexed by Fin n.

          Equations
          Instances For
            noncomputable def Module.basisUnique {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] (ι : Type u_1) [Unique ι] (h : Module.finrank R M = 1) :
            Basis ι R M

            A free module with rank 1 has a basis with one element.

            Equations
            Instances For
              @[simp]
              theorem Module.basisUnique_repr_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {ι : Type u_1} [Unique ι] {h : Module.finrank R M = 1} {v : M} {i : ι} :
              ((Module.basisUnique ι h).repr v) i = 0 v = 0