feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641)

This allows `ext` to see through quotients by subobjects of a type `A`, and apply ext lemmas specific to `A`.

Author: eric-wieser

src/algebra/category/Group/colimits.lean

@@ -313,10 +313,9 @@ noncomputable def cokernel_iso_quotient {G H : AddCommGroup} (f : G ⟶ H) :
     ext1, simp only [coequalizer_as_cokernel, category.comp_id, cokernel.π_desc_assoc], ext1, refl,
   end,
   inv_hom_id' := begin
-    ext1, induction x,
-    { simp only [colimit.ι_desc_apply, id_apply, lift_quot_mk,
-                 cofork.of_π_ι_app, comp_apply], refl },
-    { refl }
+    ext x : 2,
+    simp only [colimit.ι_desc_apply, id_apply, lift_mk, mk'_apply,
+               cofork.of_π_ι_app, comp_apply, add_monoid_hom.comp_apply],
   end, }
 
 end AddCommGroup

src/algebra/lie/basic.lean

@@ -461,6 +461,8 @@ coe_injective $ funext h
 lemma ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m :=
 ⟨by { rintro rfl m, refl, }, ext⟩
 
+lemma congr_fun {f g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) : f x = g x := h ▸ rfl
+
 @[simp] lemma mk_coe (f : M →ₗ⁅R,L⁆ N) (h₁ h₂ h₃) :
   (⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) = f :=
 by { ext, refl, }

src/algebra/lie/quotient.lean

@@ -59,9 +59,9 @@ variables (N)
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`. -/
 def action_as_endo_map : L →ₗ⁅R⁆ module.End R N.quotient :=
-{ map_lie' := λ x y, by { ext n, apply quotient.induction_on' n, intros m,
-                         change mk ⁅⁅x, y⁆, m⁆ = mk (⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆),
-                         congr, apply lie_lie, },
+{ map_lie' := λ x y, by { ext m,
+                          change mk ⁅⁅x, y⁆, m⁆ = mk (⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆),
+                          congr, apply lie_lie, },
   ..linear_map.comp (submodule.mapq_linear (N : submodule R M) ↑N) lie_submodule_invariant }
 
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is
@@ -127,6 +127,20 @@ instance lie_quotient_lie_algebra : lie_algebra R (quotient I) :=
                             rw ←submodule.quotient.mk_smul, },
                    apply congr_arg, apply lie_smul, } }
 
+/-- `lie_submodule.quotient.mk` as a `lie_module_hom`. -/
+@[simps]
+def mk' : M →ₗ⁅R,L⁆ quotient N :=
+{ to_fun := mk, map_lie' := λ r m, rfl, ..N.to_submodule.mkq}
+
+/-- Two `lie_module_hom`s from a quotient lie module are equal if their compositions with
+`lie_submodule.quotient.mk'` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma lie_module_hom_ext ⦃f g : quotient N →ₗ⁅R,L⁆ M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) :
+  f = g :=
+lie_module_hom.ext $ λ x, quotient.induction_on' x $ lie_module_hom.congr_fun h
+
 end quotient
 
 end lie_submodule

src/algebra/ring_quot.lean

@@ -261,7 +261,7 @@ The ring equivalence between `ring_quot r` and `(ideal.of_rel r).quotient`
 def ring_quot_equiv_ideal_quotient (r : B → B → Prop) :
   ring_quot r ≃+* (ideal.of_rel r).quotient :=
 ring_equiv.of_hom_inv (ring_quot_to_ideal_quotient r) (ideal_quotient_to_ring_quot r)
-  (by { ext, simp, }) (by { ext ⟨x⟩, simp, })
+  (by { ext, refl, }) (by { ext, refl, })
 
 end comm_ring
 

src/group_theory/quotient_group.lean

@@ -84,6 +84,19 @@ lemma coe_mk' : (mk' N : G → quotient N) = coe := rfl
 @[to_additive, simp]
 lemma mk'_apply (x : G) : mk' N x = x := rfl
 
+/-- Two `monoid_hom`s from a quotient group are equal if their compositions with
+`quotient_group.mk'` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[to_additive /-" Two `add_monoid_hom`s from an additive quotient group are equal if their
+compositions with `add_quotient_group.mk'` are equal.
+
+See note [partially-applied ext lemmas]. "-/, ext]
+lemma monoid_hom_ext ⦃f g : quotient N →* H⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
+monoid_hom.ext $ λ x, quotient_group.induction_on x $ (monoid_hom.congr_fun h : _)
+
+attribute [ext] quotient_add_group.add_monoid_hom_ext
+
 @[simp, to_additive quotient_add_group.eq_zero_iff]
 lemma eq_one_iff {N : subgroup G} [nN : N.normal] (x : G) : (x : quotient N) = 1 ↔ x ∈ N :=
 begin
@@ -285,8 +298,14 @@ def quotient_map_subgroup_of_of_le {A' A B' B : subgroup G}
 map _ _ (subgroup.inclusion h) $
   by simp [subgroup.subgroup_of, subgroup.comap_comap]; exact subgroup.comap_mono h'
 
+@[simp, to_additive]
+lemma quotient_map_subgroup_of_of_le_coe {A' A B' B : subgroup G}
+  [hAN : (A'.subgroup_of A).normal] [hBN : (B'.subgroup_of B).normal]
+  (h' : A' ≤ B') (h : A ≤ B) (x : A) :
+  quotient_map_subgroup_of_of_le h' h x = ↑(subgroup.inclusion h x : B) := rfl
+
 /-- Let `A', A, B', B` be subgroups of `G`.
-If `A' = B'` and `A = B`, then the quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic. 
+If `A' = B'` and `A = B`, then the quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic.
 
 Applying this equiv is nicer than rewriting along the equalities, since the type of
 `(A'.subgroup_of A : subgroup A)` depends on on `A`.
@@ -301,9 +320,10 @@ def equiv_quotient_subgroup_of_of_eq {A' A B' B : subgroup G}
   [hAN : (A'.subgroup_of A).normal] [hBN : (B'.subgroup_of B).normal]
   (h' : A' = B') (h : A = B) :
   quotient (A'.subgroup_of A) ≃* quotient (B'.subgroup_of B) :=
-by apply monoid_hom.to_mul_equiv
-    (quotient_map_subgroup_of_of_le h'.le h.le) (quotient_map_subgroup_of_of_le h'.ge h.ge);
-  { ext ⟨x⟩, simp [quotient_map_subgroup_of_of_le, map, lift, mk', subgroup.inclusion], refl }
+monoid_hom.to_mul_equiv
+  (quotient_map_subgroup_of_of_le h'.le h.le) (quotient_map_subgroup_of_of_le h'.ge h.ge)
+  (by { ext ⟨x, hx⟩, refl })
+  (by { ext ⟨x, hx⟩, refl })
 
 section snd_isomorphism_thm
 
@@ -372,12 +392,11 @@ quotient_group.lift_mk' _ _ x
 "**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃ A / M`."]
 def quotient_quotient_equiv_quotient :
   quotient_group.quotient (M.map (quotient_group.mk' N)) ≃* quotient_group.quotient M :=
-{ to_fun := quotient_quotient_equiv_quotient_aux N M h,
-  inv_fun := quotient_group.map _ _ (quotient_group.mk' N) (subgroup.le_comap_map _ _),
-  left_inv := λ x, quotient_group.induction_on' x $ λ x, quotient_group.induction_on' x $
-    λ x, by simp,
-  right_inv := λ x, quotient_group.induction_on' x $ λ x, by simp,
-  map_mul' := monoid_hom.map_mul _ }
+monoid_hom.to_mul_equiv
+  (quotient_quotient_equiv_quotient_aux N M h)
+  (quotient_group.map _ _ (quotient_group.mk' N) (subgroup.le_comap_map _ _))
+  (by { ext, simp })
+  (by { ext, simp })
 
 end third_iso_thm
 

src/linear_algebra/basic.lean

@@ -1921,6 +1921,14 @@ def mkq : M →ₗ[R] p.quotient :=
 
 @[simp] theorem mkq_apply (x : M) : p.mkq x = quotient.mk x := rfl
 
+/-- Two `linear_map`s from a quotient module are equal if their compositions with
+`submodule.mkq` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma linear_map_qext ⦃f g : p.quotient →ₗ[R] M₂⦄ (h : f.comp p.mkq = g.comp p.mkq) : f = g :=
+linear_map.ext $ λ x, quotient.induction_on' x $ (linear_map.congr_fun h : _)
+
 /-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
 vanishing on `p`, as a linear map. -/
 def liftq (f : M →ₗ[R] M₂) (h : p ≤ f.ker) : p.quotient →ₗ[R] M₂ :=
@@ -2631,8 +2639,8 @@ def compatible_maps : submodule R (M →ₗ[R] M₂) :=
 natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear. -/
 def mapq_linear : compatible_maps p q →ₗ[R] p.quotient →ₗ[R] q.quotient :=
 { to_fun    := λ f, mapq _ _ f.val f.property,
-  map_add'  := λ x y, by { ext m', apply quotient.induction_on' m', intros m, refl, },
-  map_smul' := λ c f, by { ext m', apply quotient.induction_on' m', intros m, refl, } }
+  map_add'  := λ x y, by { ext, refl, },
+  map_smul' := λ c f, by { ext, refl, } }
 
 end submodule
 

src/ring_theory/ideal/basic.lean

@@ -475,6 +475,15 @@ instance (I : ideal α) : comm_ring I.quotient :=
 def mk (I : ideal α) : α →+* I.quotient :=
 ⟨λ a, submodule.quotient.mk a, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩
 
+/- Two `ring_homs`s from the quotient by an ideal are equal if their
+compositions with `ideal.quotient.mk'` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma ring_hom_ext [non_assoc_semiring β] ⦃f g : I.quotient →+* β⦄
+  (h : f.comp (mk I) = g.comp (mk I)) : f = g :=
+ring_hom.ext $ λ x, quotient.induction_on' x $ (ring_hom.congr_fun h : _)
+
 instance : inhabited (quotient I) := ⟨mk I 37⟩
 
 protected theorem eq : mk I x = mk I y ↔ x - y ∈ I := submodule.quotient.eq I