New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(linear_algebra/multilinear): Add dom_dom_congr #5136
Conversation
src/data/equiv/basic.lean
Outdated
{ simp only [h, dif_pos], | ||
have A : e.symm ⟨i, h⟩ = j ↔ i = e j, | ||
by { rw equiv.symm_apply_eq, exact subtype.ext_iff_val }, | ||
by_cases h' : i = e j, | ||
{ rw [A.2 h', h'], simp }, | ||
{ have : ¬ e.symm ⟨i, h⟩ = j, by simpa [← A] using h', | ||
simp [h, h', this] } }, | ||
{ rw dif_pos h, | ||
rw [function.update_apply_equiv_apply, equiv.symm_symm, function.comp], | ||
rw [function.update_apply, function.update_apply], | ||
rw dif_pos h, | ||
have h_coe : (⟨i, h⟩ : s) = e j ↔ i = e j := subtype.ext_iff.trans (by rw subtype.coe_mk), | ||
simp_rw h_coe, | ||
congr, }, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Happy to revert these, but I figured there was value to showing the reader that this is an extension of the update_apply_equiv_apply
case.
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
(m : multilinear_map R (λ i : ι, M₂) M₃) (σ : equiv.perm ι) : | ||
multilinear_map R (λ i : ι, M₂) M₃ := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In hindsight, this should have had signature
(m : multilinear_map R (λ i : ι, M₂) M₃) (σ : equiv.perm ι) : | |
multilinear_map R (λ i : ι, M₂) M₃ := | |
(m : multilinear_map R (λ i : ι1, M₂) M₃) (σ : ι1 ≃ ι2) : | |
multilinear_map R (λ i : ι2, M₂) M₃ := |
I'll make a follow-up PR to generalize this, since I don't want to have to build all the way from function.basic
again! Let's let bors finish merging this one.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this should perhaps be something like:
@[simps apply]
private def dom_dom_congr_aux {M₂ M₃ : Type*} {ι₁ ι₂ : Type*} [decidable_eq ι₁] [decidable_eq ι₂]
[add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M₂] [semimodule R M₃]
(σ : ι₁ ≃ ι₂) (m : multilinear_map R (λ i : ι₁, M₂) M₃) : multilinear_map R (λ i : ι₂, M₂) M₃ :=
{ to_fun := λ v, m (λ i, v (σ i)),
map_add' := λ v i a b, by { simp_rw function.update_apply_equiv_apply v, rw m.map_add, },
map_smul' := λ v i a b, by { simp_rw function.update_apply_equiv_apply v, rw m.map_smul, }, }
/-- Transfer the equivalence between argument indices to an equivalence between maps
The naming is derived from `finsupp.dom_congr`, noting that here the permutation applies to the
domain of the domain. -/
@[simps apply symm_apply]
def dom_dom_congr {M₂ M₃ : Type*} {ι₁ ι₂ : Type*} [decidable_eq ι₁] [decidable_eq ι₂]
[add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M₂] [semimodule R M₃]
(σ : ι₁ ≃ ι₂) :
multilinear_map R (λ i : ι₁, M₂) M₃ ≃+ multilinear_map R (λ i : ι₂, M₂) M₃ :=
{ to_fun := dom_dom_congr_aux σ,
inv_fun := dom_dom_congr_aux σ.symm,
left_inv := λ m, by {ext, simp},
right_inv := λ m, by {ext, simp},
map_add' := λ a b, by {ext, simp} }
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/If.20.60f.60.20is.20a.20multilinear.20map.20then.20.60.CE.BB.20v.2C.20f.20%28v.20.E2.88.98.20.CF.83%29.60.20is.20too/near/217986991