feat(GroupTheory/Coset): add equivalences of fibers of monoid homomorphisms (#14684)

Author: Multramate

Mathlib/GroupTheory/Coset.lean

@@ -809,6 +809,54 @@ theorem card_comap_dvd_of_injective (K : Subgroup H) (f : α →* H)
 
 end Subgroup
 
+namespace MonoidHom
+
+variable [Group α] {H : Type*} [Group H]
+
+/-- An equivalence between any non-empty fiber of a `MonoidHom` and its kernel. -/
+@[to_additive "An equivalence between any non-empty fiber of an `AddMonoidHom` and its kernel."]
+def fiberEquivKer (f : α →* H) (a : α) : f ⁻¹' {f a} ≃ f.ker :=
+  (Equiv.setCongr <| Set.ext fun _ => by erw [mem_singleton_iff, mem_smul_set_iff_inv_smul_mem,
+    mem_ker, map_mul, map_inv, inv_mul_eq_one, eq_comm]).trans <| Subgroup.leftCosetEquivSubgroup a
+
+@[to_additive (attr := simp)]
+lemma fiberEquivKer_apply (f : α →* H) (a : α) (g : f ⁻¹' {f a}) : f.fiberEquivKer a g = a⁻¹ * g :=
+  rfl
+
+@[to_additive (attr := simp)]
+lemma fiberEquivKer_symm_apply (f : α →* H) (a : α) (g : f.ker) :
+    (f.fiberEquivKer a).symm g = a * g :=
+  rfl
+
+/-- An equivalence between any fiber of a surjective `MonoidHom` and its kernel. -/
+@[to_additive "An equivalence between any fiber of a surjective `AddMonoidHom` and its kernel."]
+noncomputable def fiberEquivKerOfSurjective {f : α →* H} (hf : Function.Surjective f) (h : H) :
+    f ⁻¹' {h} ≃ f.ker :=
+  (hf h).choose_spec ▸ f.fiberEquivKer (hf h).choose
+
+/-- An equivalence between any two non-empty fibers of a `MonoidHom`. -/
+@[to_additive "An equivalence between any two non-empty fibers of an `AddMonoidHom`."]
+def fiberEquiv (f : α →* H) (a b : α) : f ⁻¹' {f a} ≃ f ⁻¹' {f b} :=
+  (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
+
+@[to_additive (attr := simp)]
+lemma fiberEquiv_apply (f : α →* H) (a b : α) (g : f ⁻¹' {f a}) :
+    f.fiberEquiv a b g = b * (a⁻¹ * g) :=
+  rfl
+
+@[to_additive (attr := simp)]
+lemma fiberEquiv_symm_apply (f : α →* H) (a b : α) (g : f ⁻¹' {f b}) :
+    (f.fiberEquiv a b).symm g = a * (b⁻¹ * g) :=
+  rfl
+
+/-- An equivalence between any two fibers of a surjective `MonoidHom`. -/
+@[to_additive "An equivalence between any two fibers of a surjective `AddMonoidHom`."]
+noncomputable def fiberEquivOfSurjective {f : α →* H} (hf : Function.Surjective f) (h h' : H) :
+    f ⁻¹' {h} ≃ f ⁻¹' {h'} :=
+  (fiberEquivKerOfSurjective hf h).trans (fiberEquivKerOfSurjective hf h').symm
+
+end MonoidHom
+
 namespace QuotientGroup
 
 variable [Group α]