feat(RepresentationTheory): add smooth representations (draft)#41520
feat(RepresentationTheory): add smooth representations (draft)#41520JX-Mo wants to merge 35 commits into
Conversation
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
1. Delete the last lemma and relevant imports. 2. Fix naming conventions. 3. Delete the long list in docstring.
Make {n : \Nat} implicit in le_stabilizer_sum
Style improvements.
Simplify proofs related to stabilizers using simp +contextual.
Use the latest lemma `inv_apply_eq_iff` to shorten the proof of stabilizer_conj
Add a lemma for Subrepresentation recording the inherited group action.
Add the definition of the quotient representation associated to a subrepresentation in Representation.Subrepresentation
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Rename using `toRepresentation_apply_mk` and `quotient_apply_mk` Remove @[simp] above quotient_apply_mk
…l groups Introduces the concept of smooth representations for topological groups. Prove closure properties such as subrepresentations, quotient representations, direct sums, and tensor products being smooth. Construct smoothHom and smoothDual.
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 16e3848858Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5003 | 3 | exposed public sections |
Current commit 16e3848858
Reference commit e2361c1beb
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Define dual functor and dual representation in Smooth category.
add docstring for SmRep.of
1 participant
This draft PR introduces basic set up for smooth representations of a topological group. Hopefully it will serve as preliminary content for those who are interested in formalizing representation theory for p-adic reductive groups in the future. Concretely, we introduce the following in the files:
ihomanddualis compatible withsmootHomandcontragredient.LLM use: ChatGPT5.5 pointed out instead of manually proving the counit naturality of tensorHomAdjunction in the author's raw approach,
Adjunction.restrictFullSubcategorycan be used to construct the adjuntion.