Merge branch 'master' into port/CategoryTheory.Yoneda

Mathlib.lean

@@ -222,6 +222,7 @@ import Mathlib.CategoryTheory.Bicategory.Basic
 import Mathlib.CategoryTheory.Bicategory.Strict
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.KleisliCat
+import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
@@ -280,6 +281,7 @@ import Mathlib.Combinatorics.SetFamily.Shadow
 import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
 import Mathlib.Combinatorics.Young.SemistandardTableau
 import Mathlib.Combinatorics.Young.YoungDiagram
+import Mathlib.Computability.Language
 import Mathlib.Computability.TuringMachine
 import Mathlib.Control.Applicative
 import Mathlib.Control.Basic
@@ -387,6 +389,7 @@ import Mathlib.Data.Finsupp.ToDfinsupp
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Card
+import Mathlib.Data.Fintype.CardEmbedding
 import Mathlib.Data.Fintype.Fin
 import Mathlib.Data.Fintype.Lattice
 import Mathlib.Data.Fintype.List
@@ -870,6 +873,7 @@ import Mathlib.Order.Filter.Cofinite
 import Mathlib.Order.Filter.CountableInter
 import Mathlib.Order.Filter.Curry
 import Mathlib.Order.Filter.Extr
+import Mathlib.Order.Filter.Germ
 import Mathlib.Order.Filter.IndicatorFunction
 import Mathlib.Order.Filter.Interval
 import Mathlib.Order.Filter.Lift

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -0,0 +1,199 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
+
+! This file was ported from Lean 3 source module category_theory.category.preorder
+! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Equivalence
+import Mathlib.Order.Hom.Basic
+
+/-!
+
+# Preorders as categories
+
+We install a category instance on any preorder. This is not to be confused with the category _of_
+preorders, defined in `Order.Category.Preorder`.
+
+We show that monotone functions between preorders correspond to functors of the associated
+categories.
+
+## Main definitions
+
+* `homOfLE` and `leOfHom` provide translations between inequalities in the preorder, and
+  morphisms in the associated category.
+* `Monotone.functor` is the functor associated to a monotone function.
+
+-/
+
+
+universe u v
+
+namespace Preorder
+
+open CategoryTheory
+
+-- see Note [lower instance priority]
+/--
+The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.
+
+Because we don't allow morphisms to live in `Prop`,
+we have to define `X ⟶ Y` as `ulift (plift (X ≤ Y))`.
+See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`.
+
+See <https://stacks.math.columbia.edu/tag/00D3>.
+-/
+instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α
+    where
+  Hom U V := ULift (PLift (U ≤ V))
+  id X := ⟨⟨le_refl X⟩⟩
+  comp := @fun X Y Z f g => ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩
+#align preorder.small_category Preorder.smallCategory
+
+end Preorder
+
+namespace CategoryTheory
+
+open Opposite
+
+variable {X : Type u} [Preorder X]
+
+/-- Express an inequality as a morphism in the corresponding preorder category.
+-/
+def homOfLE {x y : X} (h : x ≤ y) : x ⟶ y :=
+  ULift.up (PLift.up h)
+#align category_theory.hom_of_le CategoryTheory.homOfLE
+
+alias homOfLE ← _root_.LE.le.hom
+#align has_le.le.hom LE.le.hom
+
+@[simp]
+theorem hom_of_le_refl {x : X} : (le_refl x).hom = 𝟙 x :=
+  rfl
+#align category_theory.hom_of_le_refl CategoryTheory.hom_of_le_refl
+
+@[simp]
+theorem hom_of_le_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) :
+    homOfLE h ≫ homOfLE k = homOfLE (h.trans k) :=
+  rfl
+#align category_theory.hom_of_le_comp CategoryTheory.hom_of_le_comp
+
+/-- Extract the underlying inequality from a morphism in a preorder category.
+-/
+theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
+  h.down.down
+#align category_theory.le_of_hom CategoryTheory.leOfHom
+
+alias leOfHom ← _root_.Quiver.Hom.le
+#align quiver.hom.le Quiver.Hom.le
+
+-- porting note: linter seems to be wrong here
+@[simp, nolint simpNF]
+theorem le_of_hom_hom_of_le {x y : X} (h : x ≤ y) : h.hom.le = h :=
+  rfl
+#align category_theory.le_of_hom_hom_of_le CategoryTheory.le_of_hom_hom_of_le
+
+-- porting note: linter gives: "Left-hand side does not simplify, when using the simp lemma on
+-- itself. This usually means that it will never apply." removing simp? It doesn't fire
+-- @[simp]
+theorem hom_of_le_le_of_hom {x y : X} (h : x ⟶ y) : h.le.hom = h := by
+  cases' h with h
+  cases h
+  rfl
+#align category_theory.hom_of_le_le_of_hom CategoryTheory.hom_of_le_le_of_hom
+
+/-- Construct a morphism in the opposite of a preorder category from an inequality. -/
+def opHomOfLe {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
+  (homOfLE h).op
+#align category_theory.op_hom_of_le CategoryTheory.opHomOfLe
+
+theorem le_ofOp_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x :=
+  h.unop.le
+#align category_theory.le_of_op_hom CategoryTheory.le_ofOp_hom
+
+instance uniqueToTop [OrderTop X] {x : X} : Unique (x ⟶ ⊤) where
+  default := homOfLE le_top
+  uniq := fun a => by rfl
+#align category_theory.unique_to_top CategoryTheory.uniqueToTop
+
+instance uniqueFromBot [OrderBot X] {x : X} : Unique (⊥ ⟶ x) where
+  default := homOfLE bot_le
+  uniq := fun a => by rfl
+#align category_theory.unique_from_bot CategoryTheory.uniqueFromBot
+
+end CategoryTheory
+
+section
+
+variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y]
+
+/-- A monotone function between preorders induces a functor between the associated categories.
+-/
+def Monotone.functor {f : X → Y} (h : Monotone f) : X ⥤ Y
+    where
+  obj := f
+  map := @fun x₁ x₂ g => CategoryTheory.homOfLE (h g.le)
+#align monotone.functor Monotone.functor
+
+@[simp]
+theorem Monotone.functor_obj {f : X → Y} (h : Monotone f) : h.functor.obj = f :=
+  rfl
+#align monotone.functor_obj Monotone.functor_obj
+
+end
+
+namespace CategoryTheory
+
+section Preorder
+
+variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y]
+
+/-- A functor between preorder categories is monotone.
+-/
+-- @[mono] porting note: `mono` tactic is not ported yet
+theorem Functor.monotone (f : X ⥤ Y) : Monotone f.obj := fun _ _ hxy => (f.map hxy.hom).le
+#align category_theory.functor.monotone CategoryTheory.Functor.monotone
+
+end Preorder
+
+section PartialOrder
+
+variable {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y]
+
+theorem Iso.to_eq {x y : X} (f : x ≅ y) : x = y :=
+  le_antisymm f.hom.le f.inv.le
+#align category_theory.iso.to_eq CategoryTheory.Iso.to_eq
+
+/-- A categorical equivalence between partial orders is just an order isomorphism.
+-/
+def Equivalence.toOrderIso (e : X ≌ Y) : X ≃o Y
+    where
+  toFun := e.functor.obj
+  invFun := e.inverse.obj
+  left_inv a := (e.unitIso.app a).to_eq.symm
+  right_inv b := (e.counitIso.app b).to_eq
+  map_rel_iff' := @fun a a' =>
+    ⟨fun h =>
+      ((Equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (Equivalence.unitInv e).app a').le,
+      fun h : a ≤ a' => (e.functor.map h.hom).le⟩
+#align category_theory.equivalence.to_order_iso CategoryTheory.Equivalence.toOrderIso
+
+-- `@[simps]` on `Equivalence.toOrderIso` produces lemmas that fail the `simpNF` linter,
+-- so we provide them by hand:
+@[simp]
+theorem Equivalence.toOrderIso_apply (e : X ≌ Y) (x : X) : e.toOrderIso x = e.functor.obj x :=
+  rfl
+#align category_theory.equivalence.to_order_iso_apply CategoryTheory.Equivalence.toOrderIso_apply
+
+@[simp]
+theorem Equivalence.toOrderIso_symm_apply (e : X ≌ Y) (y : Y) :
+    e.toOrderIso.symm y = e.inverse.obj y :=
+  rfl
+#align category_theory.equivalence.to_order_iso_symm_apply CategoryTheory.Equivalence.toOrderIso_symm_apply
+
+end PartialOrder
+
+end CategoryTheory

Mathlib/CategoryTheory/Functor/Currying.lean

@@ -116,8 +116,8 @@ def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ 
 
 variable (B C D E)
 
-/-- A version of `category_theory.whiskering_right` for bifunctors, obtained by uncurrying,
-applying `whiskering_right` and currying back
+/-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying,
+applying `whiskeringRight` and currying back
 -/
 @[simps!]
 def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E :=

Mathlib/CategoryTheory/Groupoid.lean

@@ -17,7 +17,7 @@ import Mathlib.Combinatorics.Quiver.ConnectedComponent
 /-!
 # Groupoids
 
-We define `groupoid` as a typeclass extending `category`,
+We define `Groupoid` as a typeclass extending `category`,
 asserting that all morphisms have inverses.
 
 The instance `IsIso.ofGroupoid (f : X ⟶ Y) : IsIso f` means that you can then write
@@ -40,7 +40,7 @@ namespace CategoryTheory
 universe v v₂ u u₂
 
 -- morphism levels before object levels. See note [CategoryTheory universes].
-/-- A `groupoid` is a category such that all morphisms are isomorphisms. -/
+/-- A `Groupoid` is a category such that all morphisms are isomorphisms. -/
 class Groupoid (obj : Type u) extends Category.{v} obj : Type max u (v + 1) where
   /-- The inverse morphism -/ 
   inv : ∀ {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
@@ -78,7 +78,7 @@ theorem Groupoid.inv_eq_inv (f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv
   IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f
 #align category_theory.groupoid.inv_eq_inv CategoryTheory.Groupoid.inv_eq_inv
 
-/-- `groupoid.inv` is involutive. -/
+/-- `Groupoid.inv` is involutive. -/
 @[simps]
 def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) :=
   ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩

Mathlib/CategoryTheory/Types.lean

@@ -88,8 +88,7 @@ abbrev asHom {α β : Type u} (f : α → β) : α ⟶ β :=
   f
 #align category_theory.as_hom CategoryTheory.asHom
 
--- If you don't mind some notation you can use fewer keystrokes:
-/-- Type as \upr in VScode -/
+@[inherit_doc]
 scoped notation "↾" f:200 => CategoryTheory.asHom f
 
 section