[Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras #3531

adamtopaz · 2020-07-23T20:37:30Z

This PR constructs the tensor algebra of a module over a commutative ring.

The main components are:

The construction of the tensor algebra: tensor_algebra R M for a module M over a commutative ring R.
The linear map univ R M from M to tensor_algebra R M.
Given a linear map ffrom Mto an R-algebra A, the lift of f to tensor_algebra R M is denoted lift R M f.
A theorem univ_comp_lift asserting that the composition of univ R M with lift R M fis f.
A theorem lift_unique asserting the uniqueness of lift R M fwith respect to property 4.

Note: This PR only does the bare minimum!

src/linear_algebra/tensor_algebra.lean

jcommelin

Nice work!

src/linear_algebra/tensor_algebra.lean

PatrickMassot · 2020-07-24T16:07:23Z

src/linear_algebra/tensor_algebra.lean

+  pre.has_coe_module pre.has_coe_ring pre.has_mul pre.has_add pre.has_zero
+  pre.has_one pre.has_scalar pre.has_neg
+
+instance : ring (tensor_algebra R M) :=


This proof and the following one really seem to call for a small tactic, something like the pi_instance tactic.

src/linear_algebra/tensor_algebra.lean

eric-wieser · 2020-07-24T16:31:22Z

Now that this is written in terms of [semiring R] and [semimodule M], is it still possible to show [ring (tensor_algebra R M)] if I have [ring R] [module M]?

adamtopaz · 2020-07-24T16:38:05Z

Now that this is written in terms of [semiring R] and [semimodule M], is it still possible to show [ring (tensor_algebra R M)] if I have [ring R] [module M]?

This is a more general question: if you have semiring which is an algebra over a ring, then it is also a ring.
Neg is defined as multiplication by -1 from the base ring, and distributivity should give you all the other lemmas.

But this proof probably doesn't belong in this PR.

Also, changed function ccomp in theorems to a comp of lin maps.

eric-wieser · 2020-07-24T20:43:49Z

But this proof probably doesn't belong in this PR.

My fear is that such a proof might require an entirely different construction, perhaps as bad as having two entirely separate quot definitions

src/linear_algebra/tensor_algebra.lean

semorrison · 2020-07-25T05:06:10Z

But this proof probably doesn't belong in this PR.

My fear is that such a proof might require an entirely different construction, perhaps as bad as having two entirely separate quot definitions

I'm pretty confident this won't be the case. Given a semiring which is an algebra over a ring, it's straightforward to construct a ring instance.

semorrison · 2020-07-25T05:08:44Z

Besides some minor suggestions on doc-strings, let's hit merge!

semorrison · 2020-07-25T05:08:50Z

bors d+

bors · 2020-07-25T05:08:51Z

✌️ adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

src/linear_algebra/tensor_algebra.lean

semorrison · 2020-07-25T13:01:02Z

Oops, removing that, another maintainer suggested we look more at this one.

bors d-

eric-wieser · 2020-07-28T14:45:51Z

src/linear_algebra/tensor_algebra.lean

+begin
+  refine ⟨λ hyp, _, λ hyp, by simp [hyp]⟩,
+  ext,
+  rcases quot.exists_rep x with ⟨x,rfl⟩,


Suggested change

rcases quot.exists_rep x with ⟨x,rfl⟩,

rcases x,

eric-wieser · 2020-07-28T15:07:13Z

src/linear_algebra/tensor_algebra.lean

+theorem lift_unique {A : Type u₃} [semiring A] [algebra R A] (f : M →ₗ[R] A)
+  (g : tensor_algebra R M →ₐ[R] A) : g.to_linear_map.comp (ι R M) = f ↔ g = lift R M f :=
+begin
+  refine ⟨λ hyp, _, λ hyp, by simp [hyp]⟩,


Clearer without simp, maybe?

Suggested change

refine ⟨λ hyp, _, λ hyp, by simp [hyp]⟩,

refine ⟨λ hyp, _, λ hyp, by {rw hyp, exact ι_comp_lift f}⟩,

eric-wieser · 2020-07-28T15:20:42Z

src/linear_algebra/tensor_algebra.lean

+
+@[simp]
+theorem ι_comp_lift {A : Type u₃} [semiring A] [algebra R A] (f : M →ₗ[R] A) :
+  (lift R M f).to_linear_map.comp (ι R M) = f := by {ext, refl}


Is this similar theorem also useful?

@[simp] theorem lift_comp_ι {A : Type u₃} [semiring A] [algebra R A] (g : tensor_algebra R M →ₐ[R] A) : lift R M (g.to_linear_map.comp (ι R M)) = g := begin symmetry, ext, rcases x, induction x, case pre.of: x { refl }, case pre.of_scalar: x { exact alg_hom.commutes g x }, case pre.add: a b ha hb { change g (quot.mk _ _ + quot.mk _ _) = _, rw alg_hom.map_add, rw [ha, hb], refl }, case pre.mul: a b ha hb { change g (quot.mk _ _ * quot.mk _ _) = _, rw alg_hom.map_mul, rw [ha, hb], refl }, end

With it, you can implement lift_unique as ⟨λ hyp, by simp [←hyp], λ hyp, by simp [hyp]⟩

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

adamtopaz · 2020-07-28T21:39:19Z

Here is a summary of the changes.

I removed the universe variables. As I mentioned in my response to the comment regarding this, the original proofs in lift broke, but after some small changes there, everything now works with Type*.
I added implementation details in the documentation at the top of the file.
I implemented the various changes that @semorrison suggested.
I added the theorem that @eric-wieser suggested, except I proved it using the lift_unique theorem that was already there.
Various other minor changes to the documentation and/or spacing.

Thanks @eric-wieser and @semorrison for the suggestions!

I want to reiterate that neither I nor @eric-wieser marked the conversations about the universe variables and pre as resolved. Since it was another maintainer that did this, I had the impression that the changes I made actually resolved these issues. You can take a look at the history and see that I only ever marked a conversation as resolved when I explicitly made the change that a maintainer has asked for.

I understand (and agree!) that this is a large project with a lot of moving pieces, and that style, formatting, and documentation is important. If there are some other issues, then please let me know what they are and I would be happy to change them. Other than that, I'll honestly say that I was a bit discouraged by the subtly hostile comments about "bad habits."

PatrickMassot · 2020-07-28T22:13:15Z

I'm really sorry that you felt that my comment was "subtly hostile". This was not my intention at all. I don't understand why people marked these conversation as resolved, and I admit it didn't come to my mind that other maintainers could have done that. But all maintainers are under pressure from the huge flow of PRs. We are very happy to see all those contributions, but it's not always easy.

I'm a bit worried that changing the universes annotations required changes to the proofs. I think it's a very bad omen. We really need to understand what happened. The first step is to have a look at all the universe levels inferred by Lean before and after this change.

adamtopaz · 2020-07-28T22:44:18Z

Thanks @PatrickMassot -- no harm, no foul.

Concerning universes -- I just checked. The universe annotations work out to be the same. The three types R, M and A which appear in the file can be in arbitrary (and unrelated) universes. The only thing that changed in the proof is this:

Before:

repeat { set G := lift_fun R M f,
      change G _ + G _ = G _ + G _,
      rw h_ih, },
repeat { set G := lift_fun R M f,
      change G _ * G _ = G _ * G _,
      rw h_ih, },

After:

repeat { change lift_fun R M f _ + lift_fun R M f _ = _,
      rw h_ih,
      refl, },
repeat { change lift_fun R M f _ * lift_fun R M f _ = _,
      rw h_ih,
      refl, },

These seem to be equivalent to me! And certainly the second proof works even with complete universe annotations (I checked).
Finally, I should mention that the proof didn't really break down, it's just that some goals were not closed as part of the repeat. Long story short: I don't think there is any issue in using Type* everywhere.

PatrickMassot · 2020-07-28T22:51:25Z

Ok, thanks for checking this. I'll let Scott check whether he's happy and merge.

adamtopaz · 2020-07-29T14:48:14Z

You need a comm_ring instance for R.

This is a restriction coming from the algebra typeclass

eric-wieser · 2020-07-29T14:52:34Z

I'm being stupid, I misread comm_ring as semiring. Sorry for the noise.

semorrison · 2020-08-02T10:37:30Z

bors merge

This PR constructs the tensor algebra of a module over a commutative ring. The main components are: 1. The construction of the tensor algebra: `tensor_algebra R M` for a module `M` over a commutative ring `R`. 2. The linear map `univ R M` from `M` to `tensor_algebra R M`. 3. Given a linear map `f`from `M`to an `R`-algebra `A`, the lift of `f` to `tensor_algebra R M` is denoted `lift R M f`. 4. A theorem `univ_comp_lift` asserting that the composition of `univ R M` with `lift R M f`is `f`. 5. A theorem `lift_unique` asserting the uniqueness of `lift R M f`with respect to property 4. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr>

bors · 2020-08-02T13:13:15Z

Pull request successfully merged into master.

Build succeeded:

adamtopaz added 4 commits July 23, 2020 12:09

Add defn of tensor algebra + univ prop.

7280fd3

Some linting

6aeeff9

Add minor documentation.

651ab29

Add header

82f50f8

adamtopaz added the awaiting-review The author would like community review of the PR label Jul 23, 2020

eric-wieser reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Show resolved Hide resolved

eric-wieser reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Show resolved Hide resolved

Simplify construction by changing defn of pre

166b73f

jcommelin reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

Generalize to semirings

ac04f59

PatrickMassot reviewed Jul 24, 2020

View reviewed changes

ChrisHughes24 reviewed Jul 24, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

adamtopaz added 2 commits July 24, 2020 10:43

Added hom_ext

b541c09

Also, changed function ccomp in theorems to a comp of lin maps.

Add docstrings

94effa1

semorrison reviewed Jul 25, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

semorrison reviewed Jul 25, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

semorrison added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 25, 2020

eric-wieser reviewed Jul 25, 2020

View reviewed changes

src/linear_algebra/tensor_algebra.lean Outdated Show resolved Hide resolved

semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 28, 2020

eric-wieser reviewed Jul 28, 2020

View reviewed changes

adamtopaz and others added 6 commits July 28, 2020 10:21

Cleanup; add lift_comp_\iota

7c5a393

Remove universe variables.

6ed4dc3

Add implementation details

f7b2cf9

Small change

90a4d61

Clean up documentation.

6ac38f9

Update src/data/quot.lean

a182d9f

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

robertylewis added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 29, 2020

robertylewis requested a review from semorrison July 29, 2020 10:33

This comment has been minimized.

Sign in to view

ChrisHughes24 assigned semorrison Aug 1, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 2, 2020

bors bot changed the title ~~feat(linear_algebra/tensor_algebra): Tensor algebras~~ [Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras Aug 2, 2020

bors bot closed this Aug 2, 2020

bors bot deleted the tensor_algebra branch August 2, 2020 13:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras #3531

[Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras #3531

adamtopaz commented Jul 23, 2020 •

edited by bryangingechen

Loading

jcommelin left a comment

PatrickMassot Jul 24, 2020

eric-wieser commented Jul 24, 2020 •

edited

Loading

adamtopaz commented Jul 24, 2020

eric-wieser commented Jul 24, 2020

semorrison commented Jul 25, 2020

semorrison commented Jul 25, 2020

semorrison commented Jul 25, 2020

bors bot commented Jul 25, 2020

semorrison commented Jul 25, 2020

eric-wieser Jul 28, 2020

eric-wieser Jul 28, 2020

eric-wieser Jul 28, 2020 •

edited

Loading

adamtopaz commented Jul 28, 2020

PatrickMassot commented Jul 28, 2020

adamtopaz commented Jul 28, 2020 •

edited

Loading

PatrickMassot commented Jul 28, 2020

This comment has been minimized.

adamtopaz commented Jul 29, 2020 •

edited

Loading

eric-wieser commented Jul 29, 2020

semorrison commented Aug 2, 2020

bors bot commented Aug 2, 2020

	refine ⟨λ hyp, _, λ hyp, by simp [hyp]⟩,
	refine ⟨λ hyp, _, λ hyp, by {rw hyp, exact ι_comp_lift f}⟩,

[Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras #3531

[Merged by Bors] - feat(linear_algebra/tensor_algebra): Tensor algebras #3531

Conversation

adamtopaz commented Jul 23, 2020 • edited by bryangingechen Loading

jcommelin left a comment

Choose a reason for hiding this comment

PatrickMassot Jul 24, 2020

Choose a reason for hiding this comment

eric-wieser commented Jul 24, 2020 • edited Loading

adamtopaz commented Jul 24, 2020

eric-wieser commented Jul 24, 2020

semorrison commented Jul 25, 2020

semorrison commented Jul 25, 2020

semorrison commented Jul 25, 2020

bors bot commented Jul 25, 2020

semorrison commented Jul 25, 2020

eric-wieser Jul 28, 2020

Choose a reason for hiding this comment

eric-wieser Jul 28, 2020

Choose a reason for hiding this comment

eric-wieser Jul 28, 2020 • edited Loading

Choose a reason for hiding this comment

adamtopaz commented Jul 28, 2020

PatrickMassot commented Jul 28, 2020

adamtopaz commented Jul 28, 2020 • edited Loading

PatrickMassot commented Jul 28, 2020

This comment has been minimized.

adamtopaz commented Jul 29, 2020 • edited Loading

eric-wieser commented Jul 29, 2020

semorrison commented Aug 2, 2020

bors bot commented Aug 2, 2020

adamtopaz commented Jul 23, 2020 •

edited by bryangingechen

Loading

eric-wieser commented Jul 24, 2020 •

edited

Loading

eric-wieser Jul 28, 2020 •

edited

Loading

adamtopaz commented Jul 28, 2020 •

edited

Loading

adamtopaz commented Jul 29, 2020 •

edited

Loading