feat(data/zmod/basic): morphisms to zmod are surjective (deps: #3888) (…

…#3889)

... and determined by their kernel

src/data/zmod/basic.lean

@@ -7,6 +7,7 @@ Author: Chris Hughes
 import data.int.modeq
 import algebra.char_p
 import data.nat.totient
+import ring_theory.ideal.operations
 
 /-!
 # Integers mod `n`
@@ -772,3 +773,17 @@ end
 instance zmod.subsingleton_ring_hom {n : ℕ} {R : Type*} [semiring R] :
   subsingleton ((zmod n) →+* R) :=
 ⟨ring_hom.ext_zmod⟩
+
+lemma zmod.ring_hom_surjective {R : Type*} [comm_ring R] {n : ℕ} (f : R →+* (zmod n)) :
+  function.surjective f :=
+begin
+  intros k,
+  rcases zmod.int_cast_surjective k with ⟨n, rfl⟩,
+  refine ⟨n, f.map_int_cast n⟩
+end
+
+lemma zmod.ring_hom_eq_of_ker_eq {R : Type*} [comm_ring R] {n : ℕ} (f g : R →+* (zmod n))
+  (h : f.ker = g.ker) : f = g :=
+by rw [← f.lift_of_surjective_comp (zmod.ring_hom_surjective f) g (le_of_eq h),
+      ring_hom.ext_zmod (f.lift_of_surjective _ _ _) (ring_hom.id _),
+      ring_hom.id_comp]

src/group_theory/sylow.lean

@@ -214,7 +214,7 @@ have hm' : p ∣ card (quotient (subgroup.comap ((normalizer H).subtype : normal
   nat.dvd_of_mod_eq_zero
     (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),
 let ⟨x, hx⟩ := @exists_prime_order_of_dvd_card _ (quotient_group.group _) _ _ hp hm' in
-have hxcard : ∀ {f : fintype (gpowers x)}, card (gpowers x) = p,
+have hxcard : ∀ {f : fintype (subgroup.gpowers x)}, card (subgroup.gpowers x) = p,
   from λ f, by rw [← hx, order_eq_card_gpowers]; congr,
 have fintype (subgroup.comap (quotient_group.mk' (comap H.normalizer.subtype H)) (gpowers x)),
   by apply_instance,
@@ -224,7 +224,7 @@ have hequiv : H ≃ (subgroup.comap ((normalizer H).subtype : normalizer H →*
 -- begin proof of ∃ H : subgroup G, fintype.card H = p ^ n
 ⟨subgroup.map ((normalizer H).subtype) (subgroup.comap (quotient_group.mk' _) (gpowers x)),
 begin
-  show card ↥(map H.normalizer.subtype (comap (mk' (comap H.normalizer.subtype H)) (gpowers x))) =
+  show card ↥(map H.normalizer.subtype (comap (mk' (comap H.normalizer.subtype H)) (subgroup.gpowers x))) =
     p ^ (n + 1),
   suffices : card ↥(subtype.val '' ((subgroup.comap (mk' (comap H.normalizer.subtype H))
     (gpowers x)) : set (↥(H.normalizer)))) = p^(n+1),