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
refactor(algebra/monoid_algebra): remove simp from of_apply #13791
Conversation
@@ -1542,11 +1542,11 @@ lemma lift_unique' (F : add_monoid_algebra k G →ₐ[k] A) : | |||
/-- Decomposition of a `k`-algebra homomorphism from `monoid_algebra k G` by | |||
its values on `F (single a 1)`. -/ | |||
lemma lift_unique (F : add_monoid_algebra k G →ₐ[k] A) (f : monoid_algebra k G) : | |||
F f = f.sum (λ a b, b • F (single a 1)) := | |||
by conv_lhs { rw lift_unique' F, simp [lift_apply] } | |||
F f = f.sum (λ a b, b • F (of k G a)) := |
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.
This isn't type correct any more, it needs to be either
F f = f.sum (λ a b, b • F (of k G a)) := | |
F f = f.sum (λ a b, b • F (of k G (multiplicative.of_add a))) := |
or
F f = f.sum (λ a b, b • F (of k G a)) := | |
F f = f.sum (λ a b, b • F (of' k G a)) := |
|
||
lemma alg_hom_ext_iff {φ₁ φ₂ : add_monoid_algebra k G →ₐ[k] A} : | ||
(∀ x, φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 1)) ↔ φ₁ = φ₂ := | ||
(∀ x, φ₁ (of k G x) = φ₂ (of k G x)) ↔ φ₁ = φ₂ := |
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.
This feel slike it will be irritating, because it introduces x : multiplicative G
instead of x : G
like it used to. Changing from of
to of'
would fix this.
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.
If you remove these simp
s, then we should:
- add back
[simp]
to the lemmas aboutof
that were previously rejected by the linter - copy the
simp
lemmas below aboutsingle
into versions aboutof
Maybe the second one can wait till a follow-up PR, but I think we should do the first change in this PR.
I agree, but I may not get to this soon, so I'll leave this PR as |
I felt that this was unhelpfully "breaking the API" by dropping us down to stuff about
finsupp
. On the other hand, the line between monoid_algebra and finsupp remains very murky, so it's not clear this is really an improvement.I'm proposing just this change for now as it would have been helpful for me in other recent work.