[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

smorel394 · 2024-01-13T09:26:28Z

This does a few things:

Define the algebra morphism TrivSqZeroExt.map f between trivial square-zero extensions induced by a linear mapf, and establish some of its basic properties (functoriality, composition with the basic maps to/from TrivSqZeroExt). Note that we only consider the case of a commutative base ring, because the case of a general base ring requires morphisms of bimodules, which we do not have.
Define the algebra morphism ExteriorAlgebra.map f between exterior algebras induced by a linear map f. This is a straightforward application of the similar construction for Clifford algebras, but I think it is still useful to have. Basic properties of this construction are proved: functoriality, composition with ExteriorAlgebra.ι, ExteriorAlgebra.ιInv (this part uses the first point) and ExteriorAlgebra.ιMulti. Then exactness properties of the construction is studied:
- If the linear map is surjective, then the map on exterior algebras is also surjective. This actually holds for Clifford algebras, so I added a lemma called CliffordAlgebra.map_surjective in LinearAlgebra/CliffordAlgebra/Basic.lean. For exterior algebras, the converse holds and is also proved.
- If the linear map has a retraction, then the map on exterior algebras is injective. So if the base ring is a field, the map on exterior algebras is injective if the linear map is injective.
Establish some properties of ExteriorAlgebra.ιMulti:
- ExteriorAlgebra.ιMulti_range: The range of ιMulti R n is contained in the nth exterior power (define here as LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n).
- ExteriorAlgebra.ιMulti_span_fixedDegree: This range spans the nth exterior power.
- ExteriorAlgebra.ιMulti_span: The union over all n of the range of ιMulti R n spans the whole exterior algebra (this is in LinearAlgebra/ExteriorAlgebra/Grading.lean because the proof uses the graded module structure, but it might be possible to do something simpler).
Construct ExteriorAlgebra.ιMulti_family: This takes a natural number n and a family of vectors v indexed by a linearly ordered type I, and it returns the family of n-fold products of the v i in the exterior algebra, indexed by the set of finsets of I of cardinality n. (The point, to be proved in another PR, is that when v is a basis, then ExteriorAlgebra.ιMulti_family R n v is a basis of the nth exterior power.)

eric-wieser · 2024-02-09T15:34:57Z

Sorry, I think I missed this one. Can you resolve the merge conflicts? Are all the changes in the conflicting file already merged?

smorel394 · 2024-02-15T13:54:23Z

Sorry, missed your comment (busy week). I'm thinking of just doing a fresh branch and fresh PR at this point, so the conflicts will be easier to solve.

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…hlib4 into ExteriorAlgebra

eric-wieser

This is looking pretty good now! I suspect this is similar to what I was thinking of when I added MultilinearMap.range, but I don't think that definition is of any use for this PR.

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Its easy enough to prove these by simp, then the bunled versions are trivial. The bundled version of one result can be promoted from a RingHom to an AlgHom.

eric-wieser

maintainer merge

I pushed some more small cleanups, and fixed a porting note that was causing you to need erw. This now looks great! Can you check the commit message reflects what we've ended up at?

eric-wieser · 2024-02-16T15:44:37Z

Mathlib/Algebra/TrivSqZeroExt.lean

+/-- Functoriality of `TrivSqZeroExt` when the ring is commutative: a linear map
+`f : M →ₗ[R'] N` induces a morphism of `R'`-algebras from `TrivSqZeroExt R' M` to
+`TrivSqZeroExt R' N`.
+
+Note that we cannot neatly state the non-commutative case, as we do not have morphisms of bimodules.
+-/
+def map (f : M →ₗ[R'] N) : TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N :=
+  liftEquivOfComm ⟨inrHom R' N ∘ₗ f, fun _ _ => inr_mul_inr _ _ _⟩


Please mention this in the commit message

I updated the commit message.

github-actions · 2024-02-16T15:56:29Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

github-actions · 2024-02-16T15:56:29Z

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

mattrobball · 2024-02-16T15:59:44Z

!bench

mattrobball · 2024-02-16T16:01:12Z

Thanks! Functoriality is wonderful.

Assuming the profiling comes back ok, I will merge.

leanprover-bot · 2024-02-16T16:22:29Z

Here are the benchmark results for commit 4fc8304.
There were significant changes against commit d43978d:

  Benchmark                                      Metric         Change
  ====================================================================
- ~Mathlib.Algebra.TrivSqZeroExt                 instructions    43.0%
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic   instructions    46.7%

mattrobball · 2024-02-16T16:51:12Z

+100 lines or so for +50% in instructions isn't great. These mainly all come from typeclass search. But the problems surfaced are not particular to this file and need to be fixed more generally.

bors merge

mathlib-bors · 2024-02-16T16:51:56Z

Canceled.

eric-wieser · 2024-02-16T16:52:19Z

@mattrobball, I tried making some simps unfold less, lets see if it helps.

eric-wieser · 2024-02-16T16:52:24Z

!bench

leanprover-bot · 2024-02-16T17:23:08Z

Here are the benchmark results for commit beb41cd.
There were significant changes against commit d43978d:

  Benchmark                                      Metric         Change
  ====================================================================
- ~Mathlib.Algebra.TrivSqZeroExt                 instructions    42.6%
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic   instructions    46.7%

eric-wieser · 2024-02-16T17:31:27Z

Well, I guess .4% is better than nothing!

bors merge

…of the exterior algebra and some lemmas about generation (#9718) This does a few things: - Define the algebra morphism `TrivSqZeroExt.map f` between trivial square-zero extensions induced by a linear map`f`, and establish some of its basic properties (functoriality, composition with the basic maps to/from `TrivSqZeroExt`). Note that we only consider the case of a commutative base ring, because the case of a general base ring requires morphisms of bimodules, which we do not have. - Define the algebra morphism `ExteriorAlgebra.map f` between exterior algebras induced by a linear map `f`. This is a straightforward application of the similar construction for Clifford algebras, but I think it is still useful to have. Basic properties of this construction are proved: functoriality, composition with `ExteriorAlgebra.ι`, `ExteriorAlgebra.ιInv` (this part uses the first point) and `ExteriorAlgebra.ιMulti`. Then exactness properties of the construction is studied: - If the linear map is surjective, then the map on exterior algebras is also surjective. This actually holds for Clifford algebras, so I added a lemma called `CliffordAlgebra.map_surjective` in `LinearAlgebra/CliffordAlgebra/Basic.lean`. For exterior algebras, the converse holds and is also proved. - If the linear map has a retraction, then the map on exterior algebras is injective. So if the base ring is a field, the map on exterior algebras is injective if the linear map is injective. - Establish some properties of `ExteriorAlgebra.ιMulti`: - `ExteriorAlgebra.ιMulti_range`: The range of `ιMulti R n` is contained in the `n`th exterior power (define here as `LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n`). - `ExteriorAlgebra.ιMulti_span_fixedDegree`: This range spans the `n`th exterior power. - `ExteriorAlgebra.ιMulti_span`: The union over all `n` of the range of `ιMulti R n` spans the whole exterior algebra (this is in `LinearAlgebra/ExteriorAlgebra/Grading.lean` because the proof uses the graded module structure, but it might be possible to do something simpler). - Construct `ExteriorAlgebra.ιMulti_family`: This takes a natural number `n` and a family of vectors `v` indexed by a linearly ordered type `I`, and it returns the family of `n`-fold products of the `v i` in the exterior algebra, indexed by the set of finsets of `I` of cardinality `n`. (The point, to be proved in another PR, is that when `v` is a basis, then `ExteriorAlgebra.ιMulti_family R n v` is a basis of the `n`th exterior power.) Co-authored-by: morel <smorel@math.princeton.edu> Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

mattrobball · 2024-02-16T17:32:22Z

Overall instructions were up by 4B though

mathlib-bors · 2024-02-16T18:01:33Z

Pull request successfully merged into master.

Build succeeded:

smorel394 · 2024-02-16T21:06:55Z

Great, now I can PR the exterior power stuff (after I have checked that it still builds).

smorel394 · 2024-02-17T08:46:00Z

Here it is: #10654

…of the exterior algebra and some lemmas about generation (#9718) This does a few things: - Define the algebra morphism `TrivSqZeroExt.map f` between trivial square-zero extensions induced by a linear map`f`, and establish some of its basic properties (functoriality, composition with the basic maps to/from `TrivSqZeroExt`). Note that we only consider the case of a commutative base ring, because the case of a general base ring requires morphisms of bimodules, which we do not have. - Define the algebra morphism `ExteriorAlgebra.map f` between exterior algebras induced by a linear map `f`. This is a straightforward application of the similar construction for Clifford algebras, but I think it is still useful to have. Basic properties of this construction are proved: functoriality, composition with `ExteriorAlgebra.ι`, `ExteriorAlgebra.ιInv` (this part uses the first point) and `ExteriorAlgebra.ιMulti`. Then exactness properties of the construction is studied: - If the linear map is surjective, then the map on exterior algebras is also surjective. This actually holds for Clifford algebras, so I added a lemma called `CliffordAlgebra.map_surjective` in `LinearAlgebra/CliffordAlgebra/Basic.lean`. For exterior algebras, the converse holds and is also proved. - If the linear map has a retraction, then the map on exterior algebras is injective. So if the base ring is a field, the map on exterior algebras is injective if the linear map is injective. - Establish some properties of `ExteriorAlgebra.ιMulti`: - `ExteriorAlgebra.ιMulti_range`: The range of `ιMulti R n` is contained in the `n`th exterior power (define here as `LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n`). - `ExteriorAlgebra.ιMulti_span_fixedDegree`: This range spans the `n`th exterior power. - `ExteriorAlgebra.ιMulti_span`: The union over all `n` of the range of `ιMulti R n` spans the whole exterior algebra (this is in `LinearAlgebra/ExteriorAlgebra/Grading.lean` because the proof uses the graded module structure, but it might be possible to do something simpler). - Construct `ExteriorAlgebra.ιMulti_family`: This takes a natural number `n` and a family of vectors `v` indexed by a linearly ordered type `I`, and it returns the family of `n`-fold products of the `v i` in the exterior algebra, indexed by the set of finsets of `I` of cardinality `n`. (The point, to be proved in another PR, is that when `v` is a basis, then `ExteriorAlgebra.ιMulti_family R n v` is a basis of the `n`th exterior power.) Co-authored-by: morel <smorel@math.princeton.edu> Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

morel added 10 commits January 11, 2024 22:42

removing normed spaces

2790785

some progress

c5a4c44

decidable instances

bd9e708

remove decidable instances

06240d6

indentation

620c031

shorten proof

7eb00fa

small fix

566c8a4

exterior algebra lemmas

fa3dfdc

indentation

d081935

delete useless statement

68141b2

smorel394 added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Jan 13, 2024

morel added 2 commits January 14, 2024 13:09

Merge remote-tracking branch 'origin/master' into ExteriorAlgebra

21b12c8

cleaning

a72e054

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jan 20, 2024

eric-wieser self-assigned this Feb 9, 2024

Merge remote-tracking branch 'origin/master' into ExteriorAlgebra

8c7591e

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 15, 2024

eric-wieser reviewed Feb 15, 2024

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 15, 2024

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 15, 2024

View reviewed changes

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean Outdated Show resolved Hide resolved

smorel394 and others added 6 commits February 15, 2024 16:56

Update Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

9397ae9

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

erase import

bd9273a

Merge branch 'ExteriorAlgebra' of github.com:leanprover-community/mat…

2c9cfe4

…hlib4 into ExteriorAlgebra

use induction in surjectivity proof

294f935

tiny golf

38c9e7f

small golfs and style fixes

93a5e32

eric-wieser reviewed Feb 15, 2024

View reviewed changes

eric-wieser added 4 commits February 16, 2024 15:43

golf, rename, and reorder some lemmas

ae197dc

Its easy enough to prove these by simp, then the bunled versions are trivial. The bundled version of one result can be promoted from a RingHom to an AlgHom.

add simp

76bbe11

fix for renamed lemma

006afb6

final golfs

4fc8304

eric-wieser approved these changes Feb 16, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Feb 16, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Feb 16, 2024

don't unfold things so much in proofs

beb41cd

mathlib-bors bot closed this Feb 16, 2024

mathlib-bors bot deleted the ExteriorAlgebra branch February 16, 2024 18:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

smorel394 commented Jan 13, 2024 •

edited

eric-wieser commented Feb 9, 2024

smorel394 commented Feb 15, 2024

eric-wieser left a comment

eric-wieser left a comment

eric-wieser Feb 16, 2024

smorel394 Feb 16, 2024

github-actions bot commented Feb 16, 2024

github-actions bot commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mattrobball commented Feb 16, 2024

leanprover-bot commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mathlib-bors bot commented Feb 16, 2024

eric-wieser commented Feb 16, 2024 •

edited

eric-wieser commented Feb 16, 2024

leanprover-bot commented Feb 16, 2024

eric-wieser commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mathlib-bors bot commented Feb 16, 2024

smorel394 commented Feb 16, 2024

smorel394 commented Feb 17, 2024

[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

Conversation

smorel394 commented Jan 13, 2024 • edited

eric-wieser commented Feb 9, 2024

smorel394 commented Feb 15, 2024

eric-wieser left a comment

Choose a reason for hiding this comment

eric-wieser left a comment

Choose a reason for hiding this comment

eric-wieser Feb 16, 2024

Choose a reason for hiding this comment

smorel394 Feb 16, 2024

Choose a reason for hiding this comment

github-actions bot commented Feb 16, 2024

github-actions bot commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mattrobball commented Feb 16, 2024

leanprover-bot commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mathlib-bors bot commented Feb 16, 2024

eric-wieser commented Feb 16, 2024 • edited

eric-wieser commented Feb 16, 2024

leanprover-bot commented Feb 16, 2024

eric-wieser commented Feb 16, 2024

mattrobball commented Feb 16, 2024

mathlib-bors bot commented Feb 16, 2024

smorel394 commented Feb 16, 2024

smorel394 commented Feb 17, 2024

smorel394 commented Jan 13, 2024 •

edited

eric-wieser commented Feb 16, 2024 •

edited