feat(algebra/*): morphisms from closures are equal if they agree on generators

src/algebra/star/subalgebra.lean

@@ -394,13 +394,15 @@ le_antisymm (subalgebra.star_closure_le_iff.2 $ subset_adjoin R (S : set A))
 
 /-- If some predicate holds for all `x ∈ (s : set A)` and this predicate is closed under the
 `algebra_map`, addition, multiplication and star operations, then it holds for `a ∈ adjoin R s`. -/
+@[elab_as_eliminator]
 lemma adjoin_induction {s : set A} {p : A → Prop} {a : A} (h : a ∈ adjoin R s)
   (Hs : ∀ (x : A), x ∈ s → p x) (Halg : ∀ (r : R), p (algebra_map R A r))
   (Hadd : ∀ (x y : A), p x → p y → p (x + y)) (Hmul : ∀ (x y : A), p x → p y → p (x * y))
   (Hstar : ∀ (x : A), p x → p (star x)) : p a :=
 algebra.adjoin_induction h (λ x hx, hx.elim (λ hx, Hs x hx) (λ hx, star_star x ▸ Hstar _ (Hs _ hx)))
   Halg Hadd Hmul
 
+@[elab_as_eliminator]
 lemma adjoin_induction₂ {s : set A} {p : A → A → Prop} {a b : A} (ha : a ∈ adjoin R s)
   (hb : b ∈ adjoin R s) (Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y)
   (Halg : ∀ (r₁ r₂ : R), p (algebra_map R A r₁) (algebra_map R A r₂))
@@ -425,6 +427,7 @@ begin
 end
 
 /-- The difference with `star_subalgebra.adjoin_induction` is that this acts on the subtype. -/
+@[elab_as_eliminator]
 lemma adjoin_induction' {s : set A} {p : adjoin R s → Prop} (a : adjoin R s)
   (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_adjoin R s h⟩)
   (Halg : ∀ r, p (algebra_map R _ r)) (Hadd : ∀ x y, p x → p y → p (x + y))
@@ -610,18 +613,34 @@ lemma map_adjoin [star_module R B] (f : A →⋆ₐ[R] B) (s : set A) :
 galois_connection.l_comm_of_u_comm set.image_preimage (gc_map_comap f) star_subalgebra.gc
   star_subalgebra.gc (λ _, rfl)
 
-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 :=
 begin
-  refine fun_like.ext f g (λ a, adjoin_induction' a (λ x hx, _) (λ r, _) (λ x y hx hy, _)
-    (λ x y hx hy, _) (λ x hx, _)),
-  { exact h ⟨x, subset_adjoin R s hx⟩ hx },
-  { simp only [alg_hom_class.commutes] },
-  { rw [map_add, map_add, hx, hy] },
-  { rw [map_mul, map_mul, hx, hy] },
-  { rw [map_star, map_star, hx] },
+  refine fun_like.ext _ _ (λ x, _),
+  refine adjoin_induction' x _ _ _ _ _,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intro r,
+    exact (alg_hom_class.commutes f _).trans (alg_hom_class.commutes g _).symm },
+  { intros x y hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros x y hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+  { intros x hfg,
+    exact (map_star f _).trans ((congr_arg star hfg).trans (map_star g _).symm) },
 end
 
+/-- Two star algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext] lemma ext_adjoin {s : set A} ⦃f g : adjoin R s →⋆ₐ[R] B⦄
+  (h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g :=
+star_alg_hom_class.ext_adjoin h
+
 lemma ext_adjoin_singleton {a : A} [star_alg_hom_class F R (adjoin R ({a} : set A)) B] {f g : F}
   (h : f ⟨a, self_mem_adjoin_singleton R a⟩ = g ⟨a, self_mem_adjoin_singleton R a⟩) : f = g :=
 ext_adjoin $ λ x hx, (show x = ⟨a, self_mem_adjoin_singleton R a⟩,

src/group_theory/subgroup/basic.lean

@@ -787,6 +787,27 @@ begin
     (λ x ⟨hx', hx⟩, ⟨_, Hinv _ _ hx⟩),
 end
 
+/-- Two group morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive group morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.monoid_hom.ext_closure {s : set G} ⦃f g : closure s →* G'⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_one.trans g.map_one.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+  { intros x hx hfg,
+    exact (map_inv f _).trans ((congr_arg (has_inv.inv) hfg).trans (map_inv g _).symm) },
+end
+
 /-- An induction principle for closure membership for predicates with two arguments. -/
 @[elab_as_eliminator, to_additive "An induction principle for additive closure membership, for
 predicates with two arguments."]

src/group_theory/submonoid/operations.lean

@@ -617,6 +617,25 @@ noncomputable def equiv_map_of_injective
   (f : M →* N) (hf : function.injective f) (x : S) :
   (equiv_map_of_injective S f hf x : N) = f x := rfl
 
+/-- Two monoid morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive monoid morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.monoid_hom.ext_mclosure {s : set M} ⦃f g : closure s →* N⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_one.trans g.map_one.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp, to_additive]
 lemma closure_closure_coe_preimage {s : set M} : closure ((coe : closure s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin

src/group_theory/subsemigroup/basic.lean

@@ -53,7 +53,7 @@ variables {M : Type*} {N : Type*}
 variables {A : Type*}
 
 section non_assoc
-variables [has_mul M] {s : set M}
+variables [has_mul M] [has_mul N] {s : set M}
 variables [has_add A] {t : set A}
 
 /-- `mul_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(*)` -/

src/group_theory/subsemigroup/operations.lean

@@ -462,6 +462,24 @@ noncomputable def equiv_map_of_injective
   (f : M →ₙ* N) (hf : function.injective f) (x : S) :
   (equiv_map_of_injective S f hf x : N) = f x := rfl
 
+/-- Two semigroup morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive semigroup morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.mul_hom.ext_closure {s : set M} ⦃f g : closure s →ₙ* N⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp, to_additive]
 lemma closure_closure_coe_preimage {s : set M} : closure ((coe : closure s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin

src/linear_algebra/span.lean

@@ -138,6 +138,23 @@ begin
     ⟨smul_mem _ _ hx', H2 r _ _ hx⟩)
 end
 
+/-- Two linear maps from a span are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext] lemma _root_.linear_map.ext_span {s : set M} ⦃f g : span R s →ₛₗ[σ₁₂] M₂⦄
+  (h : f ∘ set.inclusion subset_span = g ∘ set.inclusion subset_span) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine span_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_zero.trans g.map_zero.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros a x hx hfg,
+    exact (map_smulₛₗ f _ _).trans ((congr_arg ((•) (σ₁₂ a)) hfg).trans (map_smulₛₗ g _ _).symm) },
+end
+
 @[simp] lemma span_span_coe_preimage : span R ((coe : span R s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
   refine span_induction' (λ x hx, _) _ (λ x y _ _, _) (λ r x _, _) hx,

src/ring_theory/adjoin/basic.lean

@@ -109,6 +109,24 @@ subtype.rec_on x $ λ x hx, begin
     exists.elim hy $ λ hy' hy, ⟨subalgebra.mul_mem _ hx' hy', Hmul _ _ hx hy⟩),
 end
 
+/-- Two algebra morphisms from `algebra.adjoin` are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext] lemma _root_.alg_hom.adjoin_ext {s : set A} ⦃f g : adjoin R s →ₐ[R] B⦄
+  (h : f ∘ set.inclusion subset_adjoin = g ∘ set.inclusion subset_adjoin) : f = g :=
+begin
+  ext x,
+  refine adjoin_induction' _ _ _ _ x,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intro r,
+    exact (f.commutes _).trans (g.commutes _).symm },
+  { intros x y hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros x y hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp] lemma adjoin_adjoin_coe_preimage {s : set A} :
   adjoin R ((coe : adjoin R s → A) ⁻¹' s) = ⊤ :=
 begin