Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace #10372

Closed
wants to merge 43 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace #10372

wants to merge 43 commits into from

Conversation

antoinelab01
Copy link
Collaborator

Open in Gitpod

@antoinelab01 antoinelab01 added the awaiting-review The author would like community review of the PR label Nov 17, 2021
@antoinelab01 @ocfnash
Update src/linear_algebra/tensor_product_basis.lean
8451a8b 
Co-authored-by: Oliver Nash <github@olivernash.org>
eric-wieser
eric-wieser reviewed Nov 19, 2021
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using the explicit right inverse, I think you should refactor this to:

  • def dual_tensor_hom_equiv_of_basis which requires only a comm_ring, and an explicit basis
  • A proof that dual_tensor_hom_equiv_of_basis b1 = dual_tensor_hom_equiv_of_basis b2 (trivially follows from linear_equiv.ext)
  • def dual_tensor_hom_equiv := dual_tensor_hom_equiv_of_basis (fin_basis R M) which requires a field

@eric-wieser eric-wieser 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 Nov 19, 2021
riccardobrasca
riccardobrasca approved these changes Apr 14, 2022
View reviewed changes
src/data/matrix/basis.lean Outdated
variable [fintype n]

lemma trace_zero (h : j ≠ i) : trace n α α (std_basis_matrix i j c) = 0 := by simp [h]

lemma trace_same : trace n α α (std_basis_matrix i i c) = c := by simp
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the proof is simp, do you really need it? What happens if you remove it?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At any rate this lemma should include std_basis_matrix in its name

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, I don't really need it.

@riccardobrasca
Copy link
Member

Thanks!

bors d+

@bors
Copy link

bors bot commented Apr 19, 2022

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

@github-actions 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 Apr 19, 2022
eric-wieser
eric-wieser reviewed Apr 19, 2022
View reviewed changes
src/data/finsupp/basic.lean Outdated
Comment on lines 1292 to 1298
@[simp] lemma fintype_sum_single [add_comm_monoid M] [fintype α] (i : α) (m : M) :
∑ (j : α), (single i m) j = m :=
by simp [single]

@[simp] lemma fintype_sum_single' [add_comm_monoid M] [fintype α] (i : α) (m : M) :
∑ (j : α), (single j m) i = m :=
by simp [single]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think these should instead be called sum_univ_single, since syntactically this is finset.univ.sum _ not fintype.sum _.

antoinelab01 and others added 4 commits April 19, 2022 14:11
@antoinelab01 @eric-wieser
Update src/linear_algebra/contraction.lean
ef1e848 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@antoinelab01 @eric-wieser
Update src/linear_algebra/trace.lean
63cc7a6 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@antoinelab01 @eric-wieser
Update src/linear_algebra/trace.lean
86cadfc 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@antoinelab01
changed name to sum_univ_single
7e6ea37
@antoinelab01
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 19, 2022
@antoinelab01 @ocfnash
feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basi…
046daa1 
…s-free characterization of the trace (#10372)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
@bors
Copy link

bors bot commented Apr 19, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Apr 19, 2022
@antoinelab01 @ocfnash
feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basi…
b40293f 
…s-free characterization of the trace (#10372)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
@bors
Copy link

bors bot commented Apr 19, 2022

Build failed:

@ocfnash
Copy link
Collaborator

ocfnash commented Apr 20, 2022

@antoinelab01 I merged master because this was failing to build for bors. Do you think you can fix this?

@ocfnash
Copy link
Collaborator

ocfnash commented Apr 20, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 20, 2022
bors bot pushed a commit that referenced this pull request Apr 20, 2022
@antoinelab01 @ocfnash
feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basi…
b0805a5 
…s-free characterization of the trace (#10372)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
@bors
Copy link

bors bot commented Apr 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace [Merged by Bors] - feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace Apr 20, 2022
@bors bors bot closed this Apr 20, 2022
@bors bors bot deleted the trace branch April 20, 2022 18:42
Julian added a commit that referenced this pull request Apr 21, 2022
@Julian
Merge remote-tracking branch 'origin/master' into torsion-free-groups
eb3119e 
* origin/master: (394 commits)
  feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422)
  feat(order/basic): Simple shortcut lemmas (#13421)
  chore(number_theory/dioph): Cleanup (#13403)
  feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)
  feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398)
  feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)
  feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)
  feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)
  feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)
  feat(set_theory/cofinality): Basic fundamental sequences (#13326)
  feat(special_functions/pow): continuity of real to complex power (#13244)
  feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172)
  feat(category_theory/path_category): canonical quotient of a path category (#13159)
  refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)
  feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)
  fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507)
  feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)
  chore(algebra/group/type_tags): missing simp lemmas (#13553)
  feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427)
  refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)
  chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533)
  feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)
  chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)
  feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)
  refactor(analysis/calculus/cont_diff): reorder the file (#13468)
  move(set_theory/*): Organize in folders (#13530)
  chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)
  feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)
  feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546)
  feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526)
  feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)
  feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)
  feat(order/filter/basic): allow functions between different types in lemmas about [co]map by a constant function (#13542)
  feat(data/finset/basic): simp `to_finset_eq_empty` (#13531)
  feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458)
  chore(model_theory/encoding): Improve the encoding of terms  (#13532)
  feat(topology/separation): Finite sets in T2 spaces (#12845)
  feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)
  chore(algebra/big_operators/fin): golf finset.prod_range (#13535)
  chore(analysis/normed_space/star): make an argument explicit (#13523)
  feat(*): `op_op_op_comm` lemmas (#13528)
  chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)
  chore(*/matrix): order `m` and `n` alphabetically (#13510)
  feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516)
  feat(analysis): lemmas about nnnorm and nndist (#13498)
  feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513)
  feat(category_theory/limits): add characteristic predicate for zero objects (#13511)
  feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)
  fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)
  feat(order/cover): define `wcovby` (#13424)
  ...
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@ericrbg ericrbg ericrbg left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@ocfnash ocfnash ocfnash left review comments

@jcommelin jcommelin jcommelin left review comments

@Vierkantor Vierkantor Vierkantor left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
9 participants
@antoinelab01 @riccardobrasca @ocfnash @eric-wieser @Vierkantor @jcommelin @j-loreaux @ericrbg @leanprover-community-bot-assistant