[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

jsm28 · 2021-12-12T13:30:44Z

Add lemmas that composing an alternating map with a linear equiv using
comp_linear_map, or composing a basis with a linear equiv using
basis.map, produces the same orientation if and only if the
determinant of that linear equiv is positive.

depends on: [Merged by Bors] - feat(linear_algebra/orientation): add orientation.map #10815

…terminant Add lemmas that composing an alternating map with a linear equiv using `comp_linear_map`, or composing a basis with a linear equiv using `basis.map`, produces the same orientation if and only if the determinant of that linear equiv is positive.

eric-wieser

If you added the following instance:

/-- If two vectors are on the same ray then both scaled by the same action are also on the same
ray. -/
lemma same_ray.smul {S : Type*} [has_scalar S M] [smul_comm_class R S M]
  {v₁ v₂ : M} (s : S) (h : same_ray R v₁ v₂) :
  same_ray R (s • v₁) (s • v₂) :=
let ⟨r₁, r₂, hr₁, hr₂, h⟩ := h in
⟨r₁, r₂, hr₁, hr₂, by rw [smul_comm r₁ s v₁, smul_comm r₂ s v₂, h]⟩

/-- Any invertible action preserves the non-zeroness of rays. This is primarily of interest when
`G = units R` -/
instance {G} [group G] [nontrivial R] [distrib_mul_action G M] [smul_comm_class R G M] :
  mul_action G (module.ray R M) :=
{ smul := λ r, quotient.map
    (subtype.map ((•) r) $ λ a, (smul_ne_zero_iff_ne _).2) (λ a b, same_ray.smul _),
  mul_smul := λ a b, quotient.ind $ begin
    refine (λ m, congr_arg quotient.mk (subtype.ext _)),
    exact mul_smul a b _,
  end,
  one_smul := quotient.ind $ begin
    refine (λ m, congr_arg quotient.mk (subtype.ext _)),
    exact one_smul _ _,
  end }

@[simp] lemma smul_ray_of_ne_zero {G} [group G] [nontrivial R]
  [distrib_mul_action G M] [smul_comm_class R G M] (g : G) (v : M) (hv) :
  g • ray_of_ne_zero R v hv = ray_of_ne_zero R (g • v) ((smul_ne_zero_iff_ne _).2 hv) := rfl

and

-- do we have this?
def linear_equiv.det : (M ≃ₗ[R] M) →* units R :=
(units.map (linear_map.det : (M →ₗ[R] M) →* R)).comp
  (linear_map.general_linear_group.general_linear_equiv R M).symm.to_monoid_hom

then you would be able to state

/-- Composing a basis with a linear equiv scales the orientation by the determinant. -/
lemma orientation_comp_linear_equiv_eq_iff_det_pos (e : basis ι R M) (f : M ≃ₗ[R] M) :
  (e.map f).orientation = linear_equiv.det f • e.orientation :=
begin

which is likely a more useful statement as it's an equality.

jsm28 · 2021-12-12T16:14:41Z

I can see that action might be useful, and don't know what linear_equiv.det might be useful for without seeing a full proposal with doc string and API, but don't see that statement as more useful because linear_equiv.det f • e.orientation doesn't seem a particularly useful expression. I envisage using these lemmas in very concrete use cases such as "construct a basis with this orientation by modifying one that has the wrong orientation", where I definitely want "equals this orientation" or "equals the negation of this orientation".

So I can see I should probably add eq_neg_iff_det_neg variants of both my lemmas, but everything involving linear_equiv.det seems essentially orthogonal to what I want from this PR.

eric-wieser · 2021-12-12T16:19:20Z

but everything involving linear_equiv.det seems essentially orthogonal to what I want from this PR.

How about I PR those suggestions in a separate PR, and then we come back to this one to see if they end up helping?

jsm28 · 2021-12-12T16:53:06Z

Yes, that seems appropriate.

I should also add: I wondered if my result for alternating maps could be deduced from that for bases (which has more general type class assumptions) in a way that makes the proof shorter, but while they are certainly related results, it seemed rather awkward to actually rewrite one into the other.

eric-wieser · 2021-12-12T17:02:39Z

Alright, I've made #10738. Your

(e.map f).orientation = e.orientation ↔ 0 < (f : M →ₗ[R] M).det

Would follow from

(e.map f).orientation = linear_equiv.det f • e.orientation (would be in this PR)
units_smul_eq_self_iff : u • v = v ↔ (0 : R) < u (with u = linear_equiv.det f)
(linear_equiv.det f : R) = linear_map.det f (true by rfl)

eric-wieser · 2021-12-12T17:21:12Z

Interestingly, with that PR, f • e.orientation = linear_equiv.det f • e.orientation is also true!

…omp_linear_equiv

src/linear_algebra/orientation.lean

eric-wieser · 2021-12-13T10:31:43Z

Here's the smul statement using the lemmas in #10751.

lemma orientation_comp_linear_equiv_eq (e : basis ι R M) (f : M ≃ₗ[R] M) :
  (e.map f).orientation = linear_equiv.det f.symm • e.orientation :=
begin
  simp_rw [basis.orientation, smul_ray_of_ne_zero, ray_eq_iff],
  rw [(e.map f).det.eq_smul_basis_det e, e.det_map, ←linear_equiv.coe_coe, e.det_comp f.symm e,
      e.det_self, mul_one, units.smul_def, linear_equiv.coe_det],
  exact reflexive_same_ray R _ _,
end

…omp_linear_equiv

jsm28 · 2021-12-13T20:00:20Z

Feel free to push such smul statements to this branch.

…omp_linear_equiv

eric-wieser · 2021-12-15T11:29:27Z

src/linear_algebra/orientation.lean

+/-- Composing a basis with a linear equiv gives the same orientation if and only if the
+determinant is positive. -/
+lemma orientation_comp_linear_equiv_eq_iff_det_pos (e : basis ι R M) (f : M ≃ₗ[R] M) :
+  (e.map f).orientation = e.orientation ↔ 0 < (f : M →ₗ[R] M).det :=
+by rw [orientation_map, units_inv_smul, units_smul_eq_self_iff, linear_equiv.coe_det]
+
+/-- Composing a basis with a linear equiv gives the negation of that orientation if and only if
+the determinant is negative. -/
+lemma orientation_comp_linear_equiv_eq_neg_iff_det_neg (e : basis ι R M) (f : M ≃ₗ[R] M) :
+  (e.map f).orientation = -e.orientation ↔ (f : M →ₗ[R] M).det < 0 :=
+by rw [orientation_map, units_inv_smul, units_smul_eq_neg_iff, linear_equiv.coe_det]


@jsm28, do you think this lemma is still useful, now that it's just four rewrites?

I'm not entirely sure what version or versions will end up being most useful when I start working with concrete manipulations of bases to get them into the desired orientation (but also, different versions may end up being useful for different purposes).

Let's keep them then.

src/linear_algebra/orientation.lean

jsm28 · 2021-12-15T14:55:46Z

src/linear_algebra/orientation.lean

+-- TODO: does this generalize to an arbitrary orientation, not just `e.orientation`?
+lemma map_orientation_eq_det_inv_smul [nontrivial R] [is_domain R] (e : basis ι R M)
+  (f : M ≃ₗ[R] M) : orientation.map ι f e.orientation = (f.det)⁻¹ • e.orientation :=


This seems extremely closely related to what I have as orientation_comp_linear_equiv_eq_iff_det_pos, so I expect you'll want to refactor that in some way.

I'm out of time for today, but I agree; those lemmas at the bottom of the file should probably be expressed in terms of the orientation.map I added.

Well, they should be proved in terms of lemmas for orientation.map, I suppose, and start with one stated in terms of the units action before deducing the ones about positive and negative determinants, but statements for alternating maps still make sense in their own right. All these groups of lemmas are proving related results about different APIs: what (basis.map, orientation.map, alternating_map.comp_linear_map) do to an orientation, in terms of the determinant of the linear_equiv involved.

I've now refactored so this is proved for an arbitrary orientation and the lemmas at the bottom of the file (special cases when the dimension is used to deduce the existence of a basis, essentially) are restated in terms of orientation.map and deduced from this one.

eric-wieser · 2021-12-15T15:03:54Z

src/linear_algebra/orientation.lean

+/-- An equivalence between modules implies an equivalence between orientations. -/
+def orientation.map [nontrivial R] (e : M ≃ₗ[R] N) : orientation R M ι ≃ orientation R N ι :=
+module.ray.map
+  { to_fun := λ f, f.comp_linear_map e.symm,
+    inv_fun := λ g, g.comp_linear_map e,
+    map_add' := λ _ _, rfl,
+    map_smul' := λ _ _, rfl,
+    left_inv := λ f, alternating_map.ext $ λ v, f.congr_arg $ funext $ λ i, e.symm_apply_apply _,
+    right_inv := λ f, alternating_map.ext $ λ v, f.congr_arg $ funext $ λ i, e.apply_symm_apply _ }
+
+@[simp] lemma orientation.map_apply [nontrivial R] (e : M ≃ₗ[R] N) (v : alternating_map R M R ι)
+  (hv : v ≠ 0) :
+  orientation.map ι e (ray_of_ne_zero _ v hv) = ray_of_ne_zero _ (v.comp_linear_map e.symm)
+      (mt (v.comp_linear_equiv_eq_zero_iff e.symm).mp hv) := rfl
+
+@[simp] lemma orientation.map_refl [nontrivial R] :
+  (orientation.map ι $ linear_equiv.refl R M) = equiv.refl _ :=
+equiv.ext $ module.ray.ind R $ λ _ _, begin
+  dsimp,
+  simp_rw alternating_map.comp_linear_map_id,
+end
+
+@[simp] lemma orientation.map_symm [nontrivial R] (e : M ≃ₗ[R] N) :
+  (orientation.map ι e).symm = orientation.map ι e.symm := rfl


I extracted this to #10815. I expect we probably want to extra alternating_map.dom_lcongr from that too, but gitpod has given up on me so I can't try that.

…omp_linear_equiv

github-actions · 2021-12-18T18:21:50Z

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

~~[Merged by Bors] - feat(linear_algebra/orientation): add orientation.map #10815~~

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

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

eric-wieser · 2021-12-18T20:09:58Z

src/linear_algebra/orientation.lean

+lemma orientation_comp_linear_equiv_eq_iff_det_pos (f : alternating_map R M R ι) (hf : f ≠ 0)
+  (g : M ≃ₗ[R] M) (h : fintype.card ι = finrank R M) :
+  ray_of_ne_zero R (f.comp_linear_map ↑g)
+                   ((not_iff_not.2 (f.comp_linear_equiv_eq_zero_iff g)).2 hf)


The LHS here is ~~defeq~~ equal to (ray_of_ne_zero R f hf).map g.symm via orientation.map_apply and linear_equiv.symm_symm

At which point both sides only refer to f via ray_of_ne_zero R f hf, so you can generalize to f : orientation R M ι

eric-wieser · 2021-12-18T21:59:51Z

src/linear_algebra/orientation.lean

+
+/-- The value of `orientation.map` when the index type has cardinality equal to the finite
+dimension, in terms of `f.det`. -/
+lemma map_eq_det_inv_smul (x : orientation R M ι) (f : M ≃ₗ[R] M)


This lemma doesn't need a linear order, does it?

We don't have a type class for non-linearly ordered fields, however. If enough of linear_algebra.finite_dimensional gets generalized to module.free, that should enable more general type class requirements here.

eric-wieser · 2021-12-18T22:05:12Z

This looks great to me now, thanks - just worth double checking that the typeclasses aren't stronger than the proofs actually use

jcommelin

bors d+

src/linear_algebra/orientation.lean

bors · 2021-12-23T14:06:28Z

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

Co-authored-by: Johan Commelin <johan@commelin.net>

jsm28 · 2021-12-23T16:02:03Z

bors r+

…terminant (#10737) Add lemmas that composing an alternating map with a linear equiv using `comp_linear_map`, or composing a basis with a linear equiv using `basis.map`, produces the same orientation if and only if the determinant of that linear equiv is positive. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2021-12-23T18:27:29Z

Pull request successfully merged into master.

Build succeeded:

jsm28 added the awaiting-review The author would like community review of the PR label Dec 12, 2021

eric-wieser reviewed Dec 12, 2021

View reviewed changes

jsm28 added 3 commits December 12, 2021 17:30

Add eq_neg_iff_det_neg lemmas.

7c54504

Fix long line, unneeded type class assumption.

7a54af4

Merge remote-tracking branch 'origin/master' into jsm28/orientation_c…

2720c9f

…omp_linear_equiv

eric-wieser reviewed Dec 13, 2021

View reviewed changes

src/linear_algebra/orientation.lean Show resolved Hide resolved

jsm28 added 2 commits December 13, 2021 13:39

Merge remote-tracking branch 'origin/master' into jsm28/orientation_c…

137932d

…omp_linear_equiv

Merge remote-tracking branch 'origin/master' into jsm28/orientation_c…

092ce81

…omp_linear_equiv

jcommelin requested a review from eric-wieser December 14, 2021 07:29

jsm28 and others added 2 commits December 14, 2021 12:24

Merge remote-tracking branch 'origin/master' into jsm28/orientation_c…

3ee3b0d

…omp_linear_equiv

chore(*): generalize lemmas

afb759f

eric-wieser reviewed Dec 15, 2021

View reviewed changes

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

eric-wieser added 3 commits December 15, 2021 14:07

fix namespacing

c8bb6b3

generalize lemma argument

2d01e46

finish

ccc8ae5

jsm28 commented Dec 15, 2021

View reviewed changes

eric-wieser reviewed Dec 15, 2021

View reviewed changes

Fix linter failure.

c04fb5e

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 Dec 15, 2021

Merge remote-tracking branch 'origin/master' into jsm28/orientation_c…

999c853

…omp_linear_equiv

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 Dec 18, 2021

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 18, 2021

eric-wieser reviewed Dec 18, 2021

View reviewed changes

Refactor in terms of orientation.map.

71302b9

eric-wieser reviewed Dec 18, 2021

View reviewed changes

jcommelin reviewed Dec 23, 2021

View reviewed changes

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

github-actions bot 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 Dec 23, 2021

Update src/linear_algebra/orientation.lean

9063051

Co-authored-by: Johan Commelin <johan@commelin.net>

bors bot changed the title ~~feat(linear_algebra/orientation): composing with linear equivs and determinant~~ [Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant Dec 23, 2021

bors bot closed this Dec 23, 2021

bors bot deleted the jsm28/orientation_comp_linear_equiv branch December 23, 2021 18:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

jsm28 commented Dec 12, 2021 •

edited by github-actions bot

Loading

eric-wieser left a comment •

edited

Loading

jsm28 commented Dec 12, 2021

eric-wieser commented Dec 12, 2021

jsm28 commented Dec 12, 2021

eric-wieser commented Dec 12, 2021 •

edited

Loading

eric-wieser commented Dec 12, 2021 •

edited

Loading

eric-wieser commented Dec 13, 2021 •

edited

Loading

jsm28 commented Dec 13, 2021

eric-wieser Dec 15, 2021

jsm28 Dec 15, 2021

eric-wieser Dec 15, 2021

jsm28 Dec 15, 2021

eric-wieser Dec 15, 2021

jsm28 Dec 15, 2021

jsm28 Dec 18, 2021

eric-wieser Dec 15, 2021

github-actions bot commented Dec 18, 2021

eric-wieser Dec 18, 2021 •

edited

Loading

eric-wieser Dec 18, 2021

eric-wieser Dec 18, 2021

jsm28 Dec 18, 2021

eric-wieser commented Dec 18, 2021

jcommelin left a comment

bors bot commented Dec 23, 2021

jsm28 commented Dec 23, 2021

bors bot commented Dec 23, 2021

[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

Conversation

jsm28 commented Dec 12, 2021 • edited by github-actions bot Loading

eric-wieser left a comment • edited Loading

Choose a reason for hiding this comment

jsm28 commented Dec 12, 2021

eric-wieser commented Dec 12, 2021

jsm28 commented Dec 12, 2021

eric-wieser commented Dec 12, 2021 • edited Loading

eric-wieser commented Dec 12, 2021 • edited Loading

eric-wieser commented Dec 13, 2021 • edited Loading

jsm28 commented Dec 13, 2021

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot commented Dec 18, 2021

eric-wieser Dec 18, 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

eric-wieser commented Dec 18, 2021

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Dec 23, 2021

jsm28 commented Dec 23, 2021

bors bot commented Dec 23, 2021

jsm28 commented Dec 12, 2021 •

edited by github-actions bot

Loading

eric-wieser left a comment •

edited

Loading

eric-wieser commented Dec 12, 2021 •

edited

Loading

eric-wieser commented Dec 12, 2021 •

edited

Loading

eric-wieser commented Dec 13, 2021 •

edited

Loading

eric-wieser Dec 18, 2021 •

edited

Loading