chore(group_theory/subgroup): the range of a monoid/group/ring/module…

… hom from a finite type is finite (#8293)

We have this fact for maps of types, but when changing `is_group_hom` etc from classes to structures one needs it for other bundled maps. The proofs use the power of the `copy` trick.

src/algebra/algebra/subalgebra.lean

@@ -416,6 +416,12 @@ def equalizer (ϕ ψ : A →ₐ[R] B) : subalgebra R A :=
 @[simp] lemma mem_equalizer (ϕ ψ : A →ₐ[R] B) (x : A) :
   x ∈ ϕ.equalizer ψ ↔ ϕ x = ψ x := iff.rfl
 
+/-- The range of a morphism of algebras is a fintype, if the domain is a fintype.
+
+Note that this instance can cause a diamond with `subtype.fintype` if `B` is also a fintype. -/
+instance fintype_range [fintype A] [decidable_eq B] (φ : A →ₐ[R] B) : fintype φ.range :=
+set.fintype_range φ
+
 end alg_hom
 
 namespace alg_equiv

src/field_theory/polynomial_galois_group.lean

@@ -418,8 +418,9 @@ begin
     (show (gal_action_hom p ℂ).range = ⊤, from _)).mpr (subgroup.mem_top x)⟩,
   apply equiv.perm.subgroup_eq_top_of_swap_mem,
   { rwa h1 },
-  { rw [h1, ←h2],
-    exact prime_degree_dvd_card p_irr p_deg },
+  { rw h1,
+    convert prime_degree_dvd_card p_irr p_deg using 1,
+    convert h2.symm },
   { exact ⟨conj, rfl⟩ },
   { rw ← equiv.perm.card_support_eq_two,
     apply nat.add_left_cancel,

src/field_theory/subfield.lean

@@ -300,6 +300,12 @@ by { ext, simp }
 lemma map_field_range : f.field_range.map g = (g.comp f).field_range :=
 by simpa only [field_range_eq_map] using (⊤ : subfield K).map_map g f
 
+/-- The range of a morphism of fields is a fintype, if the domain is a fintype.
+
+Note that this instance can cause a diamond with `subtype.fintype` if `L` is also a fintype.-/
+instance fintype_field_range [fintype K] [decidable_eq L] (f : K →+* L) : fintype f.field_range :=
+set.fintype_range f
+
 end ring_hom
 
 namespace subfield

src/group_theory/subgroup.lean

@@ -1415,6 +1415,32 @@ le_antisymm
     (gclosure_preimage_le _ _))
   ((closure_le _).2 $ set.image_subset _ subset_closure)
 
+-- this instance can't go just after the definition of `mrange` because `fintype` is
+-- not imported at that stage
+
+/-- The range of a finite monoid under a monoid homomorphism is finite.
+Note: this instance can form a diamond with `subtype.fintype` in the
+presence of `fintype N`. -/
+@[to_additive "The range of a finite additive monoid under an additive monoid homomorphism is
+finite.
+
+Note: this instance can form a diamond with `subtype.fintype` or `subgroup.fintype` in the
+presence of `fintype N`."]
+instance fintype_mrange {M N : Type*} [monoid M] [monoid N] [fintype M] [decidable_eq N]
+  (f : M →* N) : fintype (mrange f) :=
+set.fintype_range f
+
+/-- The range of a finite group under a group homomorphism is finite.
+
+Note: this instance can form a diamond with `subtype.fintype` or `subgroup.fintype` in the
+presence of `fintype N`. -/
+@[to_additive "The range of a finite additive group under an additive group homomorphism is finite.
+
+Note: this instance can form a diamond with `subtype.fintype` or `subgroup.fintype` in the
+presence of `fintype N`."]
+instance fintype_range  [fintype G] [decidable_eq N] (f : G →* N) : fintype (range f) :=
+set.fintype_range f
+
 end monoid_hom
 
 namespace subgroup

src/linear_algebra/basic.lean

@@ -1570,6 +1570,12 @@ This is the bundled version of `set.range_factorization`. -/
 @[reducible] def range_restrict (f : M →ₗ[R] M₂) : M →ₗ[R] f.range :=
 f.cod_restrict f.range f.mem_range_self
 
+/-- The range of a linear map is finite if the domain is finite.
+Note: this instance can form a diamond with `subtype.fintype` in the
+  presence of `fintype M₂`. -/
+instance fintype_range [fintype M] [decidable_eq M₂] (f : M →ₗ[R] M₂) : fintype (range f) :=
+set.fintype_range f
+
 section
 variables (R) (M)
 

src/ring_theory/subring.lean

@@ -408,6 +408,12 @@ def cod_restrict' {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S)
   map_mul' := λ x y, subtype.eq $ f.map_mul x y,
   map_one' := subtype.eq f.map_one }
 
+/-- The range of a ring homomorphism is a fintype, if the domain is a fintype.
+Note: this instance can form a diamond with `subtype.fintype` in the
+  presence of `fintype S`. -/
+instance fintype_range [fintype R] [decidable_eq S] (f : R →+* S) : fintype (range f) :=
+set.fintype_range f
+
 end ring_hom
 
 namespace subring

src/ring_theory/subsemiring.lean

@@ -299,6 +299,12 @@ mem_srange.mpr ⟨x, rfl⟩
 lemma map_srange : f.srange.map g = (g.comp f).srange :=
 by simpa only [srange_eq_map] using (⊤ : subsemiring R).map_map g f
 
+/-- The range of a morphism of semirings is a fintype, if the domain is a fintype.
+Note: this instance can form a diamond with `subtype.fintype` in the
+  presence of `fintype S`.-/
+instance fintype_srange [fintype R] [decidable_eq S] (f : R →+* S) : fintype (srange f) :=
+set.fintype_range f
+
 end ring_hom
 
 namespace subsemiring