feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel (#28818)

Currently `ker_lift_injective` and `quotientKerEquivOfRightInverse` lift `f` to `ker f` in their definition.
This PR makes this function available as `Setoid.kerLift f` and adds a few more theorems about it.

Author: SnirBroshi

Counterexamples/AharoniKorman.lean

@@ -545,7 +545,7 @@ theorem exists_partition_iff_nonempty_spinalMap
   · rintro ⟨f⟩
     refine ⟨_, (Setoid.ker f).isPartition_classes, ?_⟩
     rintro _ ⟨x, rfl⟩
-    exact ⟨f.fibre_antichain _, f x, by simp [Setoid.ker, Function.onFun]⟩
+    exact ⟨f.fibre_antichain _, f x, by simp⟩
 
 variable {f : SpinalMap C}
 

Mathlib/Data/Setoid/Basic.lean

@@ -77,6 +77,7 @@ theorem ker_mk_eq (r : Setoid α) : ker (@Quotient.mk'' _ r) = r :=
 theorem ker_apply_mk_out {f : α → β} (a : α) : f (⟦a⟧ : Quotient (Setoid.ker f)).out = f a :=
   @Quotient.mk_out _ (Setoid.ker f) a
 
+@[simp]
 theorem ker_def {f : α → β} {x y : α} : ker f x y ↔ f x = f y :=
   Iff.rfl
 
@@ -314,38 +315,56 @@ theorem lift_unique {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quoti
   ext ⟨x⟩
   rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
 
+/-- Given a function `f`, lift it to the quotient by its kernel. -/
+def kerLift (f : α → β) : Quotient (ker f) → β :=
+  Quotient.lift f fun _ _ ↦ id
+
+@[simp]
+theorem kerLift_mk (f : α → β) (x : α) : kerLift f ⟦x⟧ = f x :=
+  rfl
+
 /-- Given a map f from α to β, the natural map from the quotient of α by the kernel of f is
 injective. -/
-theorem ker_lift_injective (f : α → β) : Injective (@Quotient.lift _ _ (ker f) f fun _ _ h => h) :=
+theorem kerLift_injective (f : α → β) : Injective <| kerLift f :=
   fun x y => Quotient.inductionOn₂' x y fun _ _ h => Quotient.sound' h
 
+@[deprecated (since := "2025-10-11")] alias ker_lift_injective := kerLift_injective
+
 /-- Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose
 induced map from the quotient of α to β is injective. -/
-theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : ∀ x y, r x y → f x = f y)
+theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : r ≤ ker f)
     (h : Injective (Quotient.lift f H)) : ker f = r :=
   le_antisymm
     (fun x y hk =>
       Quotient.exact <| h <| show Quotient.lift f H ⟦x⟧ = Quotient.lift f H ⟦y⟧ from hk)
     H
 
+theorem lift_injective_iff_ker_eq_of_le {r : Setoid α} {f : α → β}
+    (hle : r ≤ ker f) : Injective (Quotient.lift f hle) ↔ ker f = r :=
+  ⟨ker_eq_lift_of_injective f hle, fun h ↦ h ▸ kerLift_injective _⟩
+
 variable (r : Setoid α) (f : α → β)
 
+/-- The image of `f` lifted to the quotient by its kernel is equal to the image of `f` itself. -/
+@[simp] theorem range_kerLift_eq_range : Set.range (kerLift f) = Set.range f :=
+  Set.range_quotient_lift (s := ker f) _
+
+/-- The quotient of `α` by the kernel of a function `f`
+bijects with the image of `f` lifted to the quotient. -/
+noncomputable def quotientKerEquivRangeKerLift : Quotient (ker f) ≃ Set.range (kerLift f) :=
+  .ofInjective _ <| kerLift_injective _
+
 /-- The first isomorphism theorem for sets: the quotient of α by the kernel of a function f
 bijects with f's image. -/
 noncomputable def quotientKerEquivRange : Quotient (ker f) ≃ Set.range f :=
-  Equiv.ofBijective
-    ((@Quotient.lift _ (Set.range f) (ker f) fun x => ⟨f x, Set.mem_range_self x⟩) fun _ _ h =>
-      Subtype.ext h)
-    ⟨fun x y h => ker_lift_injective f <| by rcases x with ⟨⟩; rcases y with ⟨⟩; injections,
-      fun ⟨_, z, hz⟩ =>
-      ⟨@Quotient.mk'' _ (ker f) z, Subtype.ext_iff.2 hz⟩⟩
+  quotientKerEquivRangeKerLift _ |>.trans <| .setCongr <| range_kerLift_eq_range _
 
 /-- If `f` has a computable right-inverse, then the quotient by its kernel is equivalent to its
 domain. -/
 @[simps]
 def quotientKerEquivOfRightInverse (g : β → α) (hf : Function.RightInverse g f) :
     Quotient (ker f) ≃ β where
-  toFun a := (Quotient.liftOn' a f) fun _ _ => id
+  toFun := kerLift f
   invFun b := Quotient.mk'' (g b)
   left_inv a := Quotient.inductionOn' a fun a => Quotient.sound' <| hf (f a)
   right_inv := hf

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -391,11 +391,10 @@ def integerSetQuotEquivAssociates :
   Equiv.ofBijective
     (Quotient.lift (integerSetToAssociates K)
       fun _ _ h ↦ ((integerSetToAssociates_eq_iff _ _).mpr h).symm)
-    ⟨by convert Setoid.ker_lift_injective (integerSetToAssociates K)
-        all_goals
-        · ext a b
-          rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
-            MulAction.orbitRel_apply, MulAction.mem_orbit_iff],
+    ⟨Setoid.lift_injective_iff_ker_eq_of_le _ |>.mpr <| by
+        ext a b
+        rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
+          MulAction.orbitRel_apply, MulAction.mem_orbit_iff],
         (Quot.surjective_lift _).mpr (integerSetToAssociates_surjective K)⟩
 
 @[simp]

Mathlib/Topology/Separation/Hausdorff.lean

@@ -445,7 +445,7 @@ lemma compatible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Spac
     ∀ (a b : X), a ≈ b → f a = f b := by
   change t2Setoid X ≤ Setoid.ker f
   exact sInf_le <| .of_injective_continuous
-    (Setoid.ker_lift_injective _) (hf.quotient_lift fun _ _ ↦ id)
+    (Setoid.kerLift_injective _) (hf.quotient_lift fun _ _ ↦ id)
 
 /-- The universal property of the largest T2 quotient of a topological space `X`: any continuous
 map from `X` to a T2 space `Y` uniquely factors through `T2Quotient X`. This declaration builds the