# Commit2021-05-10 07:36ef90a7ab

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 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

#### Estimated changes

deleted theorem constr_basis
deleted theorem constr_eq
deleted theorem constr_neg
deleted theorem constr_range
deleted theorem constr_self
deleted theorem constr_smul
deleted theorem constr_sub
deleted theorem constr_zero
deleted theorem exists_is_basis
deleted theorem exists_subset_is_basis
deleted theorem exists_sum_is_basis
deleted theorem is_basis.comp
deleted def is_basis.constr
deleted theorem is_basis.constr_apply
deleted def is_basis.equiv_fun
deleted theorem is_basis.equiv_fun_apply
deleted theorem is_basis.equiv_fun_self
deleted theorem is_basis.equiv_fun_total
deleted theorem is_basis.ext
deleted theorem is_basis.ext_elem
deleted theorem is_basis.injective
deleted theorem is_basis.mem_span
deleted theorem is_basis.range
deleted theorem is_basis.range_repr
deleted theorem is_basis.range_repr_self
deleted def is_basis.repr
deleted theorem is_basis.repr_apply_eq
deleted theorem is_basis.repr_eq_iff
deleted theorem is_basis.repr_eq_single
deleted theorem is_basis.repr_eq_zero
deleted theorem is_basis.repr_ker
deleted theorem is_basis.repr_range
deleted theorem is_basis.repr_self_apply
deleted theorem is_basis.repr_total
deleted theorem is_basis.smul_eq_zero
deleted theorem is_basis.total_comp_repr
deleted theorem is_basis.total_repr
deleted def is_basis
deleted theorem is_basis_empty
deleted theorem is_basis_inl_union_inr
deleted theorem is_basis_singleton_iff
deleted theorem is_basis_singleton_one
deleted theorem is_basis_span
deleted theorem exists_is_basis_fintype
deleted theorem is_basis.le_span
deleted theorem is_basis.mk_eq_dim''
deleted theorem is_basis.mk_eq_dim
deleted theorem is_basis.mk_range_eq_dim
deleted theorem is_basis_of_dim_eq_zero'
deleted theorem is_basis_of_dim_eq_zero
modified theorem mk_eq_mk_of_basis'
modified theorem mk_eq_mk_of_basis
modified theorem {m}
deleted theorem dual_pair.decomposition
deleted theorem dual_pair.eq_dual
deleted theorem dual_pair.is_basis
deleted def is_basis.coord_fun
deleted def is_basis.dual_basis
deleted theorem is_basis.dual_basis_apply
deleted theorem is_basis.dual_basis_repr
deleted theorem is_basis.dual_dim_eq
deleted def is_basis.to_dual
deleted theorem is_basis.to_dual_apply
deleted theorem is_basis.to_dual_eq_repr
deleted theorem is_basis.to_dual_inj
deleted theorem is_basis.to_dual_ker
deleted theorem is_basis.to_dual_range
deleted theorem is_basis.to_dual_to_dual
deleted theorem is_basis.total_dual_basis
modified theorem finrank_eq_one_iff
deleted theorem is_basis_of_finrank_zero'
deleted theorem is_basis_of_finrank_zero
deleted theorem singleton_is_basis
deleted def is_basis.det
deleted theorem is_basis.det_apply
deleted theorem is_basis.det_self
modified theorem is_basis.iff_det
deleted theorem is_basis.to_lin_to_matrix
deleted def is_basis.to_matrix
deleted theorem is_basis.to_matrix_apply
deleted theorem is_basis.to_matrix_self
deleted theorem is_basis.to_matrix_update
modified theorem linear_equiv.is_unit_det
modified theorem linear_map.to_matrix_id
modified theorem linear_map.to_matrix_one
modified def linear_map.trace
modified def linear_map.trace_aux
modified theorem linear_map.trace_aux_def
deleted theorem linear_map.trace_aux_eq'
modified theorem linear_map.trace_aux_eq
modified theorem linear_map.trace_mul_comm
modified theorem matrix.to_lin_alg_equiv_one
modified theorem matrix.to_lin_one