feat(group_theory/subgroup linear_algebra/prod): add ker_prod_map (#7729

)

The kernel of the product of two `group_hom` is the product of the kernels (and similarly for monoids).

src/group_theory/subgroup.lean

@@ -1308,6 +1308,20 @@ begin
   { exact λ h, le_bot_iff.mp (λ x hx, h (hx.trans f.map_one.symm)) },
 end
 
+@[to_additive]
+lemma prod_map_comap_prod {G' : Type*} {N' : Type*} [group G'] [group N']
+  (f : G →* N) (g : G' →* N') (S : subgroup N) (S' : subgroup N') :
+  (S.prod S').comap (prod_map f g) = (S.comap f).prod (S'.comap g) :=
+set_like.coe_injective $ set.preimage_prod_map_prod f g _ _
+
+@[to_additive]
+lemma ker_prod_map {G' : Type*} {N' : Type*} [group G'] [group N'] (f : G →* N) (g : G' →* N') :
+  (prod_map f g).ker = f.ker.prod g.ker :=
+begin
+  dsimp only [ker],
+  rw [←prod_map_comap_prod, bot_prod_bot],
+end
+
 /-- The subgroup of elements `x : G` such that `f x = g x` -/
 @[to_additive "The additive subgroup of elements `x : G` such that `f x = g x`"]
 def eq_locus (f g : G →* N) : subgroup G :=

src/linear_algebra/prod.lean

@@ -179,6 +179,18 @@ def prod_map (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : (M × M₂) →
 @[simp] theorem prod_map_apply (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x) :
   f.prod_map g x = (f x.1, g x.2) := rfl
 
+lemma prod_map_comap_prod (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : submodule R M₂)
+  (S' : submodule R M₄) :
+  (submodule.prod S S').comap (linear_map.prod_map f g) = (S.comap f).prod (S'.comap g) :=
+set_like.coe_injective $ set.preimage_prod_map_prod f g _ _
+
+lemma ker_prod_map (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
+  (linear_map.prod_map f g).ker = submodule.prod f.ker g.ker :=
+begin
+  dsimp only [ker],
+  rw [←prod_map_comap_prod, submodule.prod_bot],
+end
+
 end linear_map
 
 end prod