-
Notifications
You must be signed in to change notification settings - Fork 298
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
feat(algebra/*): morphisms from closures are equal if they agree on generators #18836
base: master
Are you sure you want to change the base?
Conversation
lemma ext_adjoin {s : set A} [star_alg_hom_class F R (adjoin R s) B] {f g : F} | ||
(h : ∀ x : adjoin R s, (x : A) ∈ s → f x = g x) : f = g := | ||
/-- Two star algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the | ||
generators -/ | ||
lemma _root_.star_alg_hom_class.ext_adjoin | ||
{s : set A} [star_alg_hom_class F R (adjoin R s) B] ⦃f g : F⦄ | ||
(h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g := |
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.
@j-loreaux, do you have thoughts on which phrasing is more useful of:
f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)
∀ x : adjoin R s, (x : A) ∈ s → f x = g x
∀ (x : A) (hx : x ∈ s), f ⟨x, subset_adjoin _ _ hx⟩ = g ⟨x, subset_adjoin _ _ hx⟩
In theory the first one lets you chain further ext lemmas, but in practice I don't think any exist.
generators. | ||
|
||
See note [partially-applied ext lemmas]. -/ | ||
@[ext] lemma ext_adjoin {s : set A} ⦃f g : adjoin R s →⋆ₐ[R] B⦄ |
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.
Unfortunately the existing lemma couldn't be tagged ext
This adds this statement for:
subsemigroup
,add_subsemigroup
submonoid
,add_submonoid
submodule
subalgebra
star_subalgebra
I don't add it for
subsemiring
orsubring
as these are missing theinduction'
lemma used to prove it.