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

added theorem basis.apply_eq_iff
added theorem basis.coe_extend
added theorem basis.coe_mk
added theorem basis.coe_of_equiv_fun
added theorem basis.coe_of_repr
added theorem basis.coe_reindex
added theorem basis.coe_reindex_repr
added theorem basis.coe_repr_symm
added def basis.constr
added theorem basis.constr_apply
added theorem basis.constr_basis
added theorem basis.constr_def
added theorem basis.constr_eq
added theorem basis.constr_range
added theorem basis.constr_self
added def basis.coord
added theorem basis.empty_unique
added theorem basis.eq_of_apply_eq
added def basis.equiv'
added theorem basis.equiv'_apply
added theorem basis.equiv_apply
added def basis.equiv_fun
added theorem basis.equiv_fun_apply
added theorem basis.equiv_fun_self
added theorem basis.equiv_refl
added theorem basis.equiv_symm
added theorem basis.equiv_trans
added theorem basis.exists_basis
added theorem basis.ext'
added theorem basis.ext
added theorem basis.ext_elem
added theorem basis.map_apply
added theorem basis.mk_apply
added theorem basis.mk_repr
added theorem basis.prod_apply
added theorem basis.prod_repr_inl
added theorem basis.prod_repr_inr
added theorem basis.range_extend
added theorem basis.range_reindex'
added theorem basis.range_reindex
added def basis.reindex
added theorem basis.reindex_apply
added theorem basis.reindex_repr
added theorem basis.repr_apply_eq
added theorem basis.repr_eq_iff'
added theorem basis.repr_eq_iff
added theorem basis.repr_range
added theorem basis.repr_self
added theorem basis.repr_self_apply
added theorem basis.repr_symm_apply
added theorem basis.repr_symm_single
added theorem basis.repr_total
added theorem basis.singleton_apply
added theorem basis.singleton_repr
added theorem basis.subset_extend
added theorem basis.sum_equiv_fun
added theorem basis.sum_repr
added theorem basis.total_repr
added structure basis
deleted theorem constr_add
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
added theorem basis.coe_dual_basis
added theorem basis.coe_to_dual_self
added def basis.dual_basis
added theorem basis.dual_basis_apply
added theorem basis.dual_basis_repr
added theorem basis.dual_dim_eq
added def basis.to_dual
added theorem basis.to_dual_apply
added theorem basis.to_dual_eq_repr
added theorem basis.to_dual_inj
added theorem basis.to_dual_ker
added theorem basis.to_dual_range
added theorem basis.to_dual_to_dual
added theorem basis.total_coord
added theorem basis.total_dual_basis
added def dual_pair.basis
added theorem dual_pair.coe_basis
deleted theorem dual_pair.decomposition
deleted theorem dual_pair.eq_dual
deleted theorem dual_pair.is_basis
added theorem dual_pair.lc_coeffs
added theorem dual_pair.lc_def
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
added def basis.det
added theorem basis.det_apply
added theorem basis.det_self
added theorem basis.to_lin_to_matrix
added def basis.to_matrix
added theorem basis.to_matrix_apply
added theorem basis.to_matrix_self
added theorem basis.to_matrix_update
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
added theorem pi.basis_apply
added theorem pi.basis_fun_apply
added theorem pi.basis_fun_repr
added theorem pi.basis_repr
deleted theorem pi.is_basis_fun
deleted theorem pi.is_basis_fun_repr
deleted theorem pi.is_basis_fun₀
deleted theorem pi.is_basis_std_basis
added theorem basis.smul_apply
added theorem basis.smul_repr
added theorem basis.smul_repr_mk
deleted theorem is_basis.smul
deleted theorem is_basis.smul_repr
deleted theorem is_basis.smul_repr_mk