refactor(Tensors): remove pre-Lorentz Contr/Co reps in favour of ContrMod.rep/CoMod.rep#1336
Conversation
…rMod.rep/CoMod.rep Inline the vestigial `Contr`/`Co` Rep objects (which were just `Rep.of ContrMod.rep`/`Rep.of CoMod.rep`) per the maintainer TODO in RealTensor/Vector/Pre/Basic.lean. Group actions `(Contr d).ρ`/`(Co d).ρ` become `ContrMod.rep`/`CoMod.rep`; monoidal carriers `(X ⊗ Y).V` become module tensors `XMod d ⊗[ℝ] YMod d`; coerced type positions become `ContrMod d`/`CoMod d`. Deletes the dead defs, the TODO, and the duplicate `TopologicalSpace (Contr d)` instance (`ContrMod d` already carries it). All replacements are defeq-preserving; build unchanged at 9113 jobs.
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Great! Approved! Many thanks
jstoobysmith
added
the
ready-to-merge
3 participants
Towards #1048.
Implements what's flagged in
RealTensor/Vector/Pre/Basic.lean:removes the vestigial
Contr/Corepresentation aliases and replaces every call site withContrMod.rep/CoMod.repdirectly, sinceContr dwasRep.of ContrMod.rep(defeq-preserving throughout).dropped a duplicate
TopologicalSpace (Contr d)instance that was a verbatim copy of the existing one onContrMod d.Contr.toCo/Co.toContr(the intertwining maps) are untouched they were already stated againstContrMod.rep/CoMod.rep, not the aliases, so the names survive independently.One note: the issue text also mentions replacing with
Vector/CoVector. Should those be different, higher-level abstractions (Lorentz.Vector d := Fin 1 ⊕ Fin d → ℝ, a plain function type) fromContrMod.rep/CoMod.rep(Representationobjects), or is it meant to be an equivalence or a renaming of the same thing? Migrating thePre/machinery onto that carrier could be a separate, larger refactor after this. This PR follows what's already flagged in the file, but for now it is the narrower scope not a full closure yet.