Commit 2021-05-10 07:36 ef90a7ab

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 finsupps.
• 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