[Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod #5269

eric-wieser · 2020-12-07T17:29:44Z

This implements a variant of the multiplication defined in the second half of Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier):

Before this gets merged I'll want to squash the commits to remove @zhangir-azerbayev from the history, as none of the code changed in this PR is theirs.

Resolved Dependencies

depends on: [Merged by Bors] - chore(group_theory/perm, linear_algebra/alternating): add some helper lemmas for gh-5269 #6186

eric-wieser · 2020-12-12T12:16:41Z

src/group_theory/perm/shuffle.lean

@@ -0,0 +1,80 @@
+import group_theory.perm.sign


This file is junk, I'll delete it when I next push.

… lemmas for gh-5269 (#6186)

github-actions · 2021-02-12T01:07:22Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - feat(linear_algebra/alternating): Add alternatization of multilinear_map #5187~~
~~[Merged by Bors] - chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas #5260~~
~~[Merged by Bors] - feat(group_theory/perm/sign): Add sign_sum_congr #5266~~
~~[Merged by Bors] - chore(linear_algebra/multilinear): Add linear_map.comp_multilinear_map_dom_dom_congr #5270~~
~~[Merged by Bors] - feat(group_theory/perm/subgroup): Add some simple subgroups of permutations #5279~~
~~[Merged by Bors] - fix(group_theory): Remove a duplicate fintype instance on quotient_group.quotient #5368~~
~~fix(group_theory/group_action/defs): Make smul_comm_class.symm an instance #5365~~
~~[Merged by Bors] - chore(linear_algebra/{multilinear,alternating}): Generalize smul and neg instance #5364~~
~~[Merged by Bors] - chore(data/quot): Add missing simp lemmas #5372~~
~~[Merged by Bors] - chore(group_theory/group_action/basic): Add a simp lemma about smul on quotient groups #5374~~
~~[Merged by Bors] - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs #5301~~
~~[Merged by Bors] - chore(algebra/module/basic): add subsingleton (semimodule ℕ M) #5396~~
~~[Merged by Bors] - feat(linear_algebra/tensor_product): Inherit smul through is_scalar_tower #5317~~
~~[Merged by Bors] - feat(linear_algebra/tensor_product,algebra/module/linear_map): Made tmul_smul and map_smul_of_tower work for int over semirings #5430~~
~~[Merged by Bors] - fix(algebra/module/basic): Do not attach the ℕ and ℤ is_scalar_tower and smul_comm_class instances to a specific definition of smul #5509~~
~~[Merged by Bors] - chore(group_theory/perm, linear_algebra/alternating): add some helper lemmas for gh-5269 #6186~~

💡 To add or remove a dependency please update this issue/PR description.

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

eric-wieser · 2021-02-26T12:44:53Z

src/linear_algebra/alternating.lean

+    with_cases {
+      cases hi : σ⁻¹ i;
+        cases hj : σ⁻¹ j;
+        rw perm.inv_eq_iff_eq at hi hj;
+        propagate_tags' { substs hi hj, }, },
+    case [sum.inl sum.inr : i' j', sum.inr sum.inl : i' j'] {


@gebner, this is where I needed propagate_tags from leanprover-community/lean#540. Can you think of a better solution? Should substs just call propagate_tags itself?

Good lord! I think propagate_tags is the least of this proof's problems. Is there any way it can be split up into more manageable and maybe even independently useful chunks?

But yes, substs should call propagate_tags itself.

Sorry for the first impressions. I don't find it particularly readable when every line is either all_goals or work_on_goal. While I value avoiding duplication, I think it would be better to refactor all_goals { a }, work_on_goal 0 { b }, work_on_goal 1 { b' }, all_goals { c } into { a, b, c }, { a, b', c } here.

I would also introduce a definition for the summand of dom_coprod_fun. This is an unwieldy expression, and you can probably extract two of the big blocks in the proof here.

I would also introduce a definition for the summand of dom_coprod_fun. This is an unwieldy expression, and you can probably extract two of the big blocks in the proof here.

I've done this as dom_coprod.summand and eliminated dom_coprod_fun - good idea.

gebner · 2021-02-26T13:13:49Z

src/linear_algebra/alternating.lean

+  {R : Type*} {M N₁ N₂ : Type*}
+  [comm_semiring R]
+  [add_comm_group N₁] [semimodule R N₁]
+  [add_comm_group N₂] [semimodule R N₂]
+  [add_comm_monoid M] [semimodule R M]


I would use variables for this.

I didn't do this because there is already a global R variable in the file with an associated semiring. It's frustrating that def ... {R : Type*} can shadow variables, but section variables {R : Type*} def ... can't.

I guess I'll just introduce an R' and use that instead...

src/linear_algebra/alternating.lean

jcommelin

Thanks 🎉

bors d+

src/linear_algebra/alternating.lean

bors · 2021-03-13T17:43:22Z

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

bryangingechen · 2021-03-13T17:53:40Z

Do you think it's worth citing the reference in the PR comment (and adding it to references.bib)?

eric-wieser · 2021-03-13T18:06:15Z

docs/references.bib

@@ -281,6 +281,13 @@ @InProceedings{   fuerer-lochbihler-schneider-traytel2020
  bibsource     = {dblp computer science bibliography, https://dblp.org}
 }

+@Inproceedings{   Gallier2011Notes,


This was what "semantic scholar" suggested, but I have no idea what the right choice is.

LGTM as far as doc-gen is concerned.

src/linear_algebra/alternating.lean

eric-wieser · 2021-03-13T18:09:50Z

@bryangingechen, does the way I've included the reference look ok to you?

bryangingechen · 2021-03-13T19:10:10Z

docs/references.bib

@@ -281,6 +281,13 @@ @InProceedings{   fuerer-lochbihler-schneider-traytel2020
  bibsource     = {dblp computer science bibliography, https://dblp.org}
 }

+@Inproceedings{   Gallier2011Notes,


LGTM as far as doc-gen is concerned.

docs/references.bib

eric-wieser · 2021-03-14T10:35:42Z

bors r+

@zhangir-azerbayev

This implements a variant of the multiplication defined in the second half of [Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier)](https://www.cis.upenn.edu/~cis610/diffgeom-n.pdf): ![image](https://user-images.githubusercontent.com/425260/104042315-3dfe7380-51d2-11eb-9b3a-bbbb52d180f0.png) Despite what the commit generated by bors may claim, none of this is @zhangir-azerbayev's work Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser · 2021-03-14T10:36:38Z

bors r-

Commit has the wrong main author, let me try again

bors · 2021-03-14T10:36:39Z

Canceled.

This implements a variant of the multiplication defined in the second half of [Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier)](https://www.cis.upenn.edu/~cis610/diffgeom-n.pdf): ![image](https://user-images.githubusercontent.com/425260/104042315-3dfe7380-51d2-11eb-9b3a-bbbb52d180f0.png)

eric-wieser · 2021-03-14T10:50:24Z

bors r+

This implements a variant of the multiplication defined in the second half of [Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier)](https://www.cis.upenn.edu/~cis610/diffgeom-n.pdf): ![image](https://user-images.githubusercontent.com/425260/104042315-3dfe7380-51d2-11eb-9b3a-bbbb52d180f0.png)

bors · 2021-03-14T12:22:01Z

Pull request successfully merged into master.

Build succeeded:

… lemmas for gh-5269 (#6186)

This implements a variant of the multiplication defined in the second half of [Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier)](https://www.cis.upenn.edu/~cis610/diffgeom-n.pdf): ![image](https://user-images.githubusercontent.com/425260/104042315-3dfe7380-51d2-11eb-9b3a-bbbb52d180f0.png)

eric-wieser added the WIP Work in progress label Dec 7, 2020

eric-wieser mentioned this pull request Dec 10, 2020

[Merged by Bors] - feat(group_theory/perm/subgroup): Add some simple subgroups of permutations #5279

Closed

1 task

eric-wieser commented Dec 12, 2020

View reviewed changes

eric-wieser mentioned this pull request Dec 14, 2020

[Merged by Bors] - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs #5301

Closed

2 tasks

eric-wieser added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Dec 17, 2020

eric-wieser force-pushed the eric-wieser/alternating_map_product branch from fe37f4b to 4902e95 Compare December 17, 2020 23:11

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. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Dec 18, 2020

github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Jan 3, 2021

eric-wieser force-pushed the eric-wieser/alternating_map_product branch from fe04aaf to 1740bb0 Compare January 4, 2021 11:17

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 11, 2021

bryangingechen mentioned this pull request Feb 11, 2021

[Merged by Bors] - chore(group_theory/perm, linear_algebra/alternating): add some helper lemmas for gh-5269 #6186

Closed

bors bot pushed a commit that referenced this pull request Feb 11, 2021

chore(group_theory/perm, linear_algebra/alternating): add some helper…

64914d3

… lemmas for gh-5269 (#6186)

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 12, 2021

eric-wieser commented Feb 26, 2021

View reviewed changes

gebner reviewed Feb 26, 2021

View reviewed changes

eric-wieser mentioned this pull request Mar 8, 2021

[Merged by Bors] - feat(linear_algebra/determinant): determinant of a block triangular matrix #6050

Closed

1 task

jcommelin approved these changes Mar 13, 2021

View reviewed changes

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

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

eric-wieser commented Mar 13, 2021

View reviewed changes

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

bryangingechen reviewed Mar 13, 2021

View reviewed changes

eric-wieser force-pushed the eric-wieser/alternating_map_product branch from 71d61e3 to 6d7c47b Compare March 14, 2021 10:49

bors bot changed the title ~~feat(linear_algebra/alternating): Add dom_coprod~~ [Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod Mar 14, 2021

bors bot closed this Mar 14, 2021

bors bot deleted the eric-wieser/alternating_map_product branch March 14, 2021 12:22

b-mehta pushed a commit that referenced this pull request Apr 2, 2021

chore(group_theory/perm, linear_algebra/alternating): add some helper…

01fb1e1

… lemmas for gh-5269 (#6186)

YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 17, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod #5269

[Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod #5269

eric-wieser commented Dec 7, 2020 •

edited

Loading

eric-wieser Dec 12, 2020

github-actions bot commented Feb 12, 2021

eric-wieser Feb 26, 2021 •

edited

Loading

gebner Feb 26, 2021

gebner Feb 26, 2021

eric-wieser Feb 26, 2021

gebner Feb 26, 2021

eric-wieser Feb 26, 2021

jcommelin left a comment

bors bot commented Mar 13, 2021

bryangingechen commented Mar 13, 2021

eric-wieser Mar 13, 2021

bryangingechen Mar 13, 2021

eric-wieser commented Mar 13, 2021

bryangingechen Mar 13, 2021

eric-wieser commented Mar 14, 2021

eric-wieser commented Mar 14, 2021

bors bot commented Mar 14, 2021

eric-wieser commented Mar 14, 2021

bors bot commented Mar 14, 2021

[Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod #5269

[Merged by Bors] - feat(linear_algebra/alternating): Add dom_coprod #5269

Conversation

eric-wieser commented Dec 7, 2020 • edited Loading

Choose a reason for hiding this comment

github-actions bot commented Feb 12, 2021

eric-wieser Feb 26, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Mar 13, 2021

bryangingechen commented Mar 13, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Mar 13, 2021

Choose a reason for hiding this comment

eric-wieser commented Mar 14, 2021

eric-wieser commented Mar 14, 2021

bors bot commented Mar 14, 2021

eric-wieser commented Mar 14, 2021

bors bot commented Mar 14, 2021

eric-wieser commented Dec 7, 2020 •

edited

Loading

eric-wieser Feb 26, 2021 •

edited

Loading