The standard basis

This file defines the standard basis Pi.basis (s : ∀ j, Basis (ι j) R (M j)), which is the Σ j, ι j-indexed basis of Π j, M j. The basis vectors are given by Pi.basis s ⟨j, i⟩ j' = Pi.single j' (s j) i = if j = j' then s i else 0.

The standard basis on R^η, i.e. η → R is called Pi.basisFun.

To give a concrete example, Pi.single (i : Fin 3) (1 : R) gives the ith unit basis vector in R³, and Pi.basisFun R (Fin 3) proves this is a basis over Fin 3 → R.

Main definitions

• Pi.basis s: given a basis s i for each M i, the standard basis on Π i, M i
• Pi.basisFun R η: the standard basis on R^η, i.e. η → R, given by Pi.basisFun R η i j = Pi.single i 1 j = if i = j then 1 else 0.
• Matrix.stdBasis R n m: the standard basis on Matrix n m R, given by Matrix.stdBasis R n m (i, j) i' j' = if (i, j) = (i', j') then 1 else 0.

theorem Pi.linearIndependent_single {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Ring R] [(i : η) → AddCommGroup (Ms i)] [(i : η) → Module R (Ms i)] [DecidableEq η] (v : (j : η) → ιs j → Ms j) (hs : ∀ (i : η), LinearIndependent R (v i)) : LinearIndependent R fun (ji : (j : η) × ιs j) => single ji.fst (v ji.fst ji.snd)

theorem Pi.linearIndependent_single_one (ι : Type u_5) (R : Type u_6) [Ring R] [DecidableEq ι] : LinearIndependent R fun (i : ι) => single i 1

theorem Pi.linearIndependent_single_of_ne_zero {ι : Type u_5} {R : Type u_6} {M : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [DecidableEq ι] {v : ι → M} (hv : ∀ (i : ι), v i ≠ 0) : LinearIndependent R fun (i : ι) => single i (v i)

@[deprecated Pi.linearIndependent_single_of_ne_zero (since := "2025-04-14")]

theorem Pi.linearIndependent_single_ne_zero {ι : Type u_5} {R : Type u_6} [Ring R] [NoZeroDivisors R] [DecidableEq ι] {v : ι → R} (hv : ∀ (i : ι), v i ≠ 0) : LinearIndependent R fun (i : ι) => single i (v i)

noncomputable def Pi.basis {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] (s : (j : η) → Basis (ιs j) R (Ms j)) : Basis ((j : η) × ιs j) R ((j : η) → Ms j)

Pi.basis (s : ∀ j, Basis (ιs j) R (Ms j)) is the Σ j, ιs j-indexed basis on Π j, Ms j given by s j on each component.

For the standard basis over R on the finite-dimensional space η → R see Pi.basisFun.

Equations

• Pi.basis s = { repr := (LinearEquiv.piCongrRight fun (j : η) => (s j).repr) ≪≫ₗ (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm }

@[simp]

theorem Pi.basis_repr_single {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] [DecidableEq η] (s : (j : η) → Basis (ιs j) R (Ms j)) (j : η) (i : ιs j) : (Pi.basis s).repr (single j ((s j) i)) = Finsupp.single ⟨j, i⟩ 1

@[simp]

theorem Pi.basis_apply {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] [DecidableEq η] (s : (j : η) → Basis (ιs j) R (Ms j)) (ji : (j : η) × ιs j) : (Pi.basis s) ji = single ji.fst ((s ji.fst) ji.snd)

@[simp]

theorem Pi.basis_repr {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] (s : (j : η) → Basis (ιs j) R (Ms j)) (x : (j : η) → Ms j) (ji : (j : η) × ιs j) : ((Pi.basis s).repr x) ji = ((s ji.fst).repr (x ji.fst)) ji.snd

noncomputable def Pi.basisFun (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] : Basis η R (η → R)

The basis on η → R where the ith basis vector is Function.update 0 i 1.

Equations

• Pi.basisFun R η = Basis.ofEquivFun (LinearEquiv.refl R (η → R))

@[simp]

theorem Pi.basisFun_apply (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] [DecidableEq η] (i : η) : (basisFun R η) i = single i 1

@[simp]

theorem Pi.basisFun_repr (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] (x : η → R) (i : η) : ((basisFun R η).repr x) i = x i

@[simp]

theorem Pi.basisFun_equivFun (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] : (basisFun R η).equivFun = LinearEquiv.refl R (η → R)

theorem AlgHom.eq_piEvalAlgHom {k : Type u_1} {G : Type u_2} [CommSemiring k] [NoZeroDivisors k] [Nontrivial k] [Finite G] (φ : (G → k) →ₐ[k] k) : ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) => k) s

Let k be an integral domain and G an arbitrary finite set. Then any algebra morphism φ : (G → k) →ₐ[k] k is an evaluation map.

@[deprecated AlgHom.eq_piEvalAlgHom (since := "2025-04-15")]

theorem eval_of_algHom {k : Type u_1} {G : Type u_2} [CommSemiring k] [NoZeroDivisors k] [Nontrivial k] [Finite G] (φ : (G → k) →ₐ[k] k) : ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) => k) s

Alias of AlgHom.eq_piEvalAlgHom.

---

Let k be an integral domain and G an arbitrary finite set. Then any algebra morphism φ : (G → k) →ₐ[k] k is an evaluation map.

noncomputable def Module.piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] : (ι → M) ≃ₗ[R] (ι → R) →ₗ[R] M

The natural linear equivalence: Mⁱ ≃ Hom(Rⁱ, M) for an R-module M.

Equations

• Module.piEquiv ι R M = (Pi.basisFun R ι).constr R

theorem Module.piEquiv_apply_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Fintype ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) : ((piEquiv ι R M) v) w = ∑ i : ι, w i • v i

@[simp]

theorem Module.range_piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : LinearMap.range ((piEquiv ι R M) v) = Submodule.span R (Set.range v)

@[simp]

theorem Module.surjective_piEquiv_apply_iff (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : Function.Surjective ⇑((piEquiv ι R M) v) ↔ Submodule.span R (Set.range v) = ⊤

instance Module.Free.pi {ι : Type u_1} (R : Type u_2) [Semiring R] (M : ι → Type u_4) [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Free R (M i)] : Free R ((i : ι) → M i)

The product of finitely many free modules is free.

instance Module.Free.function (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [Free R M] : Free R (ι → M)

The product of finitely many free modules is free (non-dependent version to help with typeclass search).