From 68742ef0061e8fde6483a2e403b1b281f4f5820b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:46:42 +0100 Subject: [PATCH 1/3] feat(CategoryTheory/Category/Preorder): isIso_homOfLE --- Mathlib/CategoryTheory/Category/Preorder.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean index 502cd253384312..4b61bb5cecc445 100644 --- a/Mathlib/CategoryTheory/Category/Preorder.lean +++ b/Mathlib/CategoryTheory/Category/Preorder.lean @@ -68,6 +68,10 @@ def homOfLE {x y : X} (h : x ≤ y) : x ⟶ y := @[inherit_doc homOfLE] abbrev _root_.LE.le.hom := @homOfLE +/-- Express an inequality `x ≤ y` as a morphism in the corresponding preorder category. +(In this version, the variables `x` and `y` are explicit.) -/ +abbrev homOfLE' (x y : X) (h : x ≤ y) : x ⟶ y := homOfLE h + @[simp] theorem homOfLE_refl {x : X} (h : x ≤ x) : h.hom = 𝟙 x := rfl @@ -92,6 +96,16 @@ lemma homOfLE_isIso_of_eq {x y : X} (h : x ≤ y) (heq : x = y) : IsIso (homOfLE h) := ⟨homOfLE (le_of_eq heq.symm), by simp⟩ +lemma isIso_homOfLE {x y : X} (h : x = y) : + IsIso (homOfLE (by rw [h]): x ⟶ y) := by + subst h + change IsIso (𝟙 _) + infer_instance + +lemma isIso_homOfLE' (x y : X) (h : x = y) : + IsIso (homOfLE' x y (by rw [h])) := + isIso_homOfLE h + @[simp, reassoc] lemma homOfLE_comp_eqToHom {a b c : X} (hab : a ≤ b) (hbc : b = c) : homOfLE hab ≫ eqToHom hbc = homOfLE (hab.trans (le_of_eq hbc)) := From 9131c8d8af660ef882d579df5ba6994064e436a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:49:01 +0100 Subject: [PATCH 2/3] whitespace --- Mathlib/CategoryTheory/Category/Preorder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean index 4b61bb5cecc445..25dd3d16386ca6 100644 --- a/Mathlib/CategoryTheory/Category/Preorder.lean +++ b/Mathlib/CategoryTheory/Category/Preorder.lean @@ -97,7 +97,7 @@ lemma homOfLE_isIso_of_eq {x y : X} (h : x ≤ y) (heq : x = y) : ⟨homOfLE (le_of_eq heq.symm), by simp⟩ lemma isIso_homOfLE {x y : X} (h : x = y) : - IsIso (homOfLE (by rw [h]): x ⟶ y) := by + IsIso (homOfLE (by rw [h]) : x ⟶ y) := by subst h change IsIso (𝟙 _) infer_instance From 29305a1a277f57a694e745ee74c05f79784bdc3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 16:23:49 +0100 Subject: [PATCH 3/3] removed homOfLE' --- Mathlib/CategoryTheory/Category/Preorder.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean index 25dd3d16386ca6..a7ad9f3a14836a 100644 --- a/Mathlib/CategoryTheory/Category/Preorder.lean +++ b/Mathlib/CategoryTheory/Category/Preorder.lean @@ -68,10 +68,6 @@ def homOfLE {x y : X} (h : x ≤ y) : x ⟶ y := @[inherit_doc homOfLE] abbrev _root_.LE.le.hom := @homOfLE -/-- Express an inequality `x ≤ y` as a morphism in the corresponding preorder category. -(In this version, the variables `x` and `y` are explicit.) -/ -abbrev homOfLE' (x y : X) (h : x ≤ y) : x ⟶ y := homOfLE h - @[simp] theorem homOfLE_refl {x : X} (h : x ≤ x) : h.hom = 𝟙 x := rfl @@ -102,10 +98,6 @@ lemma isIso_homOfLE {x y : X} (h : x = y) : change IsIso (𝟙 _) infer_instance -lemma isIso_homOfLE' (x y : X) (h : x = y) : - IsIso (homOfLE' x y (by rw [h])) := - isIso_homOfLE h - @[simp, reassoc] lemma homOfLE_comp_eqToHom {a b c : X} (hab : a ≤ b) (hbc : b = c) : homOfLE hab ≫ eqToHom hbc = homOfLE (hab.trans (le_of_eq hbc)) :=