[Merged by Bors] - refactor(*): bundle `is_basis` #7496

Vierkantor · 2021-05-04T16:18:10Z

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:

I'm still reviewing for style and updating docstrings, but the API and code itself are more or less definitive now.

src/linear_algebra/affine_space/independent.lean

src/linear_algebra/basis.lean

src/linear_algebra/finite_dimensional.lean

src/ring_theory/adjoin_root.lean

Vierkantor · 2021-05-06T11:39:06Z

Those were all the changes I wanted to make, so the refactor is now officially not a WIP anymore!

github-actions · 2021-05-07T05:36:41Z

⏳ Alright! Looks like we need to wait for some dependencies:

~~[Merged by Bors] - feat(linear_algebra/finsupp): linear equivalence between α × β →₀ M and α →₀ β →₀ M #7472~~
~~[Merged by Bors] - feat(data/finsupp): prove f.curry x y = f (x, y) #7475~~
~~[Merged by Bors] - feat(algebra/module): S-linear equivs are also R-linear equivs #7476~~
~~[Merged by Bors] - feat(data/equiv,linear_algebra): Pi_congr_right for mul_equiv and linear_equiv #7489~~
~~[Merged by Bors] - feat(data/finsupp,linear_algebra): finsupp.split is an equivalence #7490~~
~~[Merged by Bors] - feat(algebra/module): linear_equiv.refl.symm = refl #7493~~
feat(algebra/module): scalar multiplication on the right is injective #7548
[Merged by Bors] - feat(linear_algebra/finsupp): adjust apply lemma for finsupp.dom_lcongr #7549

💡 Don't worry, I will continue watching the list above and keep this comment updated. To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

src/linear_algebra/basis.lean

jcommelin · 2021-05-10T06:05:34Z

Thanks for this major refactor! There are still some open comments on some of the PRs that this depends on. I'm going to merge this now. And then those issues in the other PRs can be fixed afterwards. (Might be some merge conflicts, but they will be less problematic than letting this PR rot.)

bors merge

bors · 2021-05-10T06:05:36Z

👎 Rejected by label

jcommelin · 2021-05-10T06:05:52Z

bors merge

@digama0

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

bors · 2021-05-10T12:34:53Z

Pull request successfully merged into master.

Build succeeded:

…ngr` (#7549) This is a split-off dependency from #7496. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Vierkantor added the WIP Work in progress label May 4, 2021

github-actions bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label. labels May 4, 2021

Vierkantor force-pushed the bundled-basis branch from 161d7b1 to 704c96d Compare May 6, 2021 09:46