chore(category_theory/*): provide aliases quiver.hom.le and has_le.le.hom (#7677)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: jcommelin

src/algebra/category/Module/limits.lean

@@ -147,7 +147,7 @@ variables (f : Π i j, i ≤ j → G i →ₗ[R] G j) [module.directed_system G
 @[simps]
 def direct_limit_diagram : ι ⥤ Module R :=
 { obj := λ i, Module.of R (G i),
-  map := λ i j hij, f i j (le_of_hom hij),
+  map := λ i j hij, f i j hij.le,
   map_id' := λ i, by { ext x, apply module.directed_system.map_self },
   map_comp' := λ i j k hij hjk,
   begin

src/category_theory/category/default.lean

@@ -260,6 +260,7 @@ Because we do not allow the morphisms of a category to live in `Prop`,
 unfortunately we need to use `plift` and `ulift` when defining the morphisms.
 
 As convenience functions, we provide `hom_of_le` and `le_of_hom` to wrap and unwrap inequalities.
+We also provide aliases `has_le.le.hom` and `quiver.hom.le` to use with dot notation.
 -/
 namespace preorder
 
@@ -291,19 +292,21 @@ Express an inequality as a morphism in the corresponding preorder category.
 -/
 def hom_of_le {U V : α} (h : U ≤ V) : U ⟶ V := ulift.up (plift.up h)
 
-@[simp] lemma hom_of_le_refl {U : α} : hom_of_le (le_refl U) = 𝟙 U := rfl
+alias hom_of_le ← has_le.le.hom
+
+@[simp] lemma hom_of_le_refl {U : α} : (le_refl U).hom = 𝟙 U := rfl
 @[simp] lemma hom_of_le_comp {U V W : α} (h : U ≤ V) (k : V ≤ W) :
-  hom_of_le h ≫ hom_of_le k = hom_of_le (h.trans k) := rfl
+  h.hom ≫ k.hom = (h.trans k).hom := rfl
 
 /--
 Extract the underlying inequality from a morphism in a preorder category.
 -/
 lemma le_of_hom {U V : α} (h : U ⟶ V) : U ≤ V := h.down.down
 
-@[simp] lemma le_of_hom_hom_of_le {a b : α} (h : a ≤ b) :
-  le_of_hom (hom_of_le h) = h := rfl
-@[simp] lemma hom_of_le_le_of_hom {a b : α} (h : a ⟶ b) :
-  hom_of_le (le_of_hom h) = h :=
+alias le_of_hom ← quiver.hom.le
+
+@[simp] lemma le_of_hom_hom_of_le {a b : α} (h : a ≤ b) : h.hom.le = h := rfl
+@[simp] lemma hom_of_le_le_of_hom {a b : α} (h : a ⟶ b) : h.le.hom = h :=
 by { cases h, cases h, refl, }
 
 end category_theory

src/category_theory/category/pairwise.lean

@@ -143,7 +143,7 @@ def cocone_is_colimit : is_colimit (cocone U) :=
   begin
     apply complete_lattice.Sup_le,
     rintros _ ⟨j, rfl⟩,
-    exact le_of_hom (s.ι.app (single j))
+    exact (s.ι.app (single j)).le
   end }
 
 end

src/category_theory/equivalence.lean

@@ -563,9 +563,8 @@ def equivalence.to_order_iso (e : α ≌ β) : α ≃o β :=
   left_inv := λ a, (e.unit_iso.app a).to_eq.symm,
   right_inv := λ b, (e.counit_iso.app b).to_eq,
   map_rel_iff' := λ a a',
-    ⟨λ h, le_of_hom
-      ((equivalence.unit e).app a ≫ e.inverse.map (hom_of_le h) ≫ (equivalence.unit_inv e).app a'),
-     λ (h : a ≤ a'), le_of_hom (e.functor.map (hom_of_le h))⟩, }
+    ⟨λ h, ((equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (equivalence.unit_inv e).app a').le,
+     λ (h : a ≤ a'), (e.functor.map h.hom).le⟩, }
 
 -- `@[simps]` on `equivalence.to_order_iso` produces lemmas that fail the `simp_nf` linter,
 -- so we provide them by hand:

src/category_theory/functor.lean

@@ -106,7 +106,7 @@ end
 
 @[mono] lemma monotone {α β : Type*} [preorder α] [preorder β] (F : α ⥤ β) :
   monotone F.obj :=
-λ a b h, le_of_hom (F.map (hom_of_le h))
+λ a b h, (F.map h.hom).le
 
 end functor
 

src/category_theory/isomorphism.lean

@@ -390,8 +390,7 @@ end functor
 section partial_order
 variables {α β : Type*} [partial_order α] [partial_order β]
 
-lemma iso.to_eq {X Y : α} (f : X ≅ Y) : X = Y :=
-le_antisymm (le_of_hom f.hom) (le_of_hom f.inv)
+lemma iso.to_eq {X Y : α} (f : X ≅ Y) : X = Y := le_antisymm f.hom.le f.inv.le
 
 end partial_order
 

src/category_theory/limits/lattice.lean

@@ -47,7 +47,7 @@ def limit_cone [complete_lattice α] (F : J ⥤ α) : limit_cone F :=
     { app := λ j, hom_of_le (complete_lattice.Inf_le _ _ (set.mem_range_self _)) } },
   is_limit :=
   { lift := λ s, hom_of_le (complete_lattice.le_Inf _ _
-    begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.π.app j), end) } }
+    begin rintros _ ⟨j, rfl⟩, exact (s.π.app j).le, end) } }
 
 /--
 The colimit cocone over any functor into a complete lattice.
@@ -59,7 +59,7 @@ def colimit_cocone [complete_lattice α] (F : J ⥤ α) : colimit_cocone F :=
     { app := λ j, hom_of_le (complete_lattice.le_Sup _ _ (set.mem_range_self _)) } },
   is_colimit :=
   { desc := λ s, hom_of_le (complete_lattice.Sup_le _ _
-    begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.ι.app j), end) } }
+    begin rintros _ ⟨j, rfl⟩, exact (s.ι.app j).le, end) } }
 
 -- It would be nice to only use the `Inf` half of the complete lattice, but
 -- this seems not to have been described separately.

src/category_theory/opposites.lean

@@ -419,18 +419,16 @@ universes v
 variables {α : Type v} [preorder α]
 
 /-- Construct a morphism in the opposite of a preorder category from an inequality. -/
-def op_hom_of_le {U V : αᵒᵖ} (h : unop V ≤ unop U) : U ⟶ V :=
-quiver.hom.op (hom_of_le h)
+def op_hom_of_le {U V : αᵒᵖ} (h : unop V ≤ unop U) : U ⟶ V := h.hom.op
 
-lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U :=
-le_of_hom (h.unop)
+lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U := h.unop.le
 
 namespace functor
 
 variables (C)
 variables (D : Type u₂) [category.{v₂} D]
 
-/-- 
+/--
 The equivalence of functor categories induced by `op` and `unop`.
 -/
 @[simps]

src/category_theory/sites/spaces.lean

@@ -45,7 +45,7 @@ def grothendieck_topology : grothendieck_topology (opens T) :=
   top_mem' := λ X x hx, ⟨_, 𝟙 _, trivial, hx⟩,
   pullback_stable' := λ X Y S f hf y hy,
   begin
-    rcases hf y (le_of_hom f hy) with ⟨U, g, hg, hU⟩,
+    rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩,
     refine ⟨U ⊓ Y, hom_of_le inf_le_right, _, hU, hy⟩,
     apply S.downward_closed hg (hom_of_le inf_le_left),
   end,
@@ -60,10 +60,10 @@ def grothendieck_topology : grothendieck_topology (opens T) :=
 def pretopology : pretopology (opens T) :=
 { coverings := λ X R, ∀ x ∈ X, ∃ U (f : U ⟶ X), R f ∧ x ∈ U,
   has_isos := λ X Y f i x hx,
-        by exactI ⟨_, _, presieve.singleton_self _, le_of_hom (inv f) hx⟩,
+        by exactI ⟨_, _, presieve.singleton_self _, (inv f).le hx⟩,
   pullbacks := λ X Y f S hS x hx,
   begin
-    rcases hS _ (le_of_hom f hx) with ⟨U, g, hg, hU⟩,
+    rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩,
     refine ⟨_, _, presieve.pullback_arrows.mk _ _ hg, _⟩,
     have : U ⊓ Y ≤ pullback g f,
       refine le_of_hom (pullback.lift (hom_of_le inf_le_left) (hom_of_le inf_le_right) rfl),

src/category_theory/skeletal.lean

@@ -152,7 +152,7 @@ variables {C} {D}
 def map (F : C ⥤ D) : thin_skeleton C ⥤ thin_skeleton D :=
 { obj := quotient.map F.obj $ λ X₁ X₂ ⟨hX⟩, ⟨F.map_iso hX⟩,
   map := λ X Y, quotient.rec_on_subsingleton₂ X Y $
-           λ x y k, hom_of_le ((le_of_hom k).elim (λ t, ⟨F.map t⟩)) }
+           λ x y k, hom_of_le (k.le.elim (λ t, ⟨F.map t⟩)) }
 
 lemma comp_to_thin_skeleton (F : C ⥤ D) : F ⋙ to_thin_skeleton D = to_thin_skeleton C ⋙ map F :=
 rfl
@@ -172,11 +172,11 @@ def map₂ (F : C ⥤ D ⥤ E) :
                 (λ X₁ X₂ ⟨hX⟩ Y₁ Y₂ ⟨hY⟩, ⟨(F.obj X₁).map_iso hY ≪≫ (F.map_iso hX).app Y₂⟩) x y,
     map := λ y₁ y₂, quotient.rec_on_subsingleton x $
             λ X, quotient.rec_on_subsingleton₂ y₁ y₂ $
-              λ Y₁ Y₂ hY, hom_of_le ((le_of_hom hY).elim (λ g, ⟨(F.obj X).map g⟩)) },
+              λ Y₁ Y₂ hY, hom_of_le (hY.le.elim (λ g, ⟨(F.obj X).map g⟩)) },
   map := λ x₁ x₂, quotient.rec_on_subsingleton₂ x₁ x₂ $
            λ X₁ X₂ f,
            { app := λ y, quotient.rec_on_subsingleton y
-              (λ Y, hom_of_le ((le_of_hom f).elim (λ f', ⟨(F.map f').app Y⟩))) } }
+              (λ Y, hom_of_le (f.le.elim (λ f', ⟨(F.map f').app Y⟩))) } }
 
 variables (C)
 
@@ -192,7 +192,7 @@ noncomputable def from_thin_skeleton : thin_skeleton C ⥤ C :=
   map := λ x y, quotient.rec_on_subsingleton₂ x y $
     λ X Y f,
             (nonempty.some (quotient.mk_out X)).hom
-          ≫ (le_of_hom f).some
+          ≫ f.le.some
           ≫ (nonempty.some (quotient.mk_out Y)).inv }
 
 noncomputable instance from_thin_skeleton_equivalence : is_equivalence (from_thin_skeleton C) :=
@@ -218,7 +218,7 @@ instance thin_skeleton_partial_order : partial_order (thin_skeleton C) :=
   ..category_theory.thin_skeleton.preorder C }
 
 lemma skeletal : skeletal (thin_skeleton C) :=
-λ X Y, quotient.induction_on₂ X Y $ λ x y h, h.elim $ λ i, (le_of_hom i.1).antisymm (le_of_hom i.2)
+λ X Y, quotient.induction_on₂ X Y $ λ x y h, h.elim $ λ i, i.1.le.antisymm i.2.le
 
 lemma map_comp_eq (F : E ⥤ D) (G : D ⥤ C) : map (F ⋙ G) = map F ⋙ map G :=
 functor.eq_of_iso skeletal $