# Commit 2021-05-10 07:36 ef90a7ab

View on Github →refactor(*): bundle `is_basis`

(#7496)
This PR replaces the definition of a basis used in mathlib and fixes the usages throughout.
Rationale: Previously, `is_basis`

was a predicate on a family of vectors, saying this family is linear independent and spans the whole space. We encountered many small annoyances when working with these unbundled definitions, for example complicated `is_basis`

arguments being hidden in the goal view or slow elaboration when mapping a basis to a slightly different set of basis vectors. The idea to turn `basis`

into a bundled structure originated in the discussion on #4949. @digama0 suggested on Zulip to identify these "bundled bases" with their map `repr : M ≃ₗ[R] (ι →₀ R)`

that sends a vector to its coordinates. (In fact, that specific map used to be only a `linear_map`

rather than an equiv.)
Overview of the changes:

- The
`is_basis`

predicate has been replaced with the`basis`

structure. - Parameters of the form
`{b : ι → M} (hb : is_basis R b)`

become a single parameter`(b : basis ι R M)`

. - Constructing a basis from a linear independent family spanning the whole space is now spelled
`basis.mk hli hspan`

, instead of`and.intro hli hspan`

. - You can also use
`basis.of_repr`

to construct a basis from an equivalence`e : M ≃ₗ[R] (ι →₀ R)`

. If`ι`

is a`fintype`

, you can use`basis.of_equiv_fun (e : M ≃ₗ[R] (ι → R))`

instead, saving you from having to work with`finsupp`

s. - Most declaration names that used to contain
`is_basis`

are now spelled with`basis`

, e.g.`pi.is_basis_fun`

is now`pi.basis_fun`

. - Theorems of the form
`exists_is_basis K V : ∃ (s : set V) (b : s -> V), is_basis K b`

and`finite_dimensional.exists_is_basis_finset K V : [finite_dimensional K V] -> ∃ (s : finset V) (b : s -> V), is_basis K b`

have been replaced with (noncomputable) defs such as`basis.of_vector_space K V : basis (basis.of_vector_space_index K V) K V`

and`finite_dimensional.finset_basis : basis (finite_dimensional.finset_basis_index K V) K V`

; the indexing sets being a separate definition means we can declare a`fintype (basis.of_vector_space_index K V)`

instance on finite dimensional spaces, rather than having to use`cases exists_is_basis_fintype K V with ...`

each time. - Definitions of a
`basis`

are now, wherever practical, accompanied by`simp`

lemmas giving the values of`coe_fn`

and`repr`

for that basis. - Some auxiliary results like
`pi.is_basis_fun₀`

have been removed since they are no longer needed. Basic API overview:

`basis ι R M`

is the type of`ι`

-indexed`R`

-bases for a module`M`

, represented by a linear equiv`M ≃ₗ[R] ι →₀ R`

.- the basis vectors of a basis
`b`

are given by`b i`

for`i : ι`

`basis.repr`

is the isomorphism sending`x : M`

to its coordinates`basis.repr b x : ι →₀ R`

. The inverse of`b.repr`

is`finsupp.total _ _ _ b`

. The converse, turning this isomorphism into a basis, is called`basis.of_repr`

.- If
`ι`

is finite, there is a variant of`repr`

called`basis.equiv_fun b : M ≃ₗ[R] ι → R`

. The converse, turning this isomorphism into a basis, is called`basis.of_equiv_fun`

. `basis.constr hv f`

constructs a linear map`M₁ →ₗ[R] M₂`

given the values`f : ι → M₂`

at the basis elements`⇑b : ι → M₁`

.`basis.mk`

: a linear independent set of vectors spanning the whole module determines a basis (the converse consists of`basis.linear_independent`

and`basis.span_eq`

`basis.ext`

states that two linear maps are equal if they coincide on a basis; similar results are available for linear equivs (if they coincide on the basis vectors), elements (if their coordinates coincide) and the functions`b.repr`

and`⇑b`

.`basis.of_vector_space`

states that every vector space has a basis.`basis.reindex`

uses an equiv to map a basis to a different indexing set,`basis.map`

uses a linear equiv to map a basis to a different module Zulip discussions:- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Bundled.20basis
- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234949