-
Notifications
You must be signed in to change notification settings - Fork 259
/
FinPartOrd.lean
99 lines (72 loc) · 2.75 KB
/
FinPartOrd.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.CategoryTheory.FintypeCat
import Mathlib.Order.Category.PartOrd
/-!
# The category of finite partial orders
This defines `FinPartOrd`, the category of finite partial orders.
Note: `FinPartOrd` is *not* a subcategory of `BddOrd` because finite orders are not necessarily
bounded.
## TODO
`FinPartOrd` is equivalent to a small category.
-/
universe u v
open CategoryTheory
/-- The category of finite partial orders with monotone functions. -/
structure FinPartOrd where
toPartOrd : PartOrd
[isFintype : Fintype toPartOrd]
namespace FinPartOrd
instance : CoeSort FinPartOrd Type* :=
⟨fun X => X.toPartOrd⟩
instance (X : FinPartOrd) : PartialOrder X :=
X.toPartOrd.str
attribute [instance] FinPartOrd.isFintype
-- synTaut
/-- Construct a bundled `FinPartOrd` from `PartialOrder` + `Fintype`. -/
def of (α : Type*) [PartialOrder α] [Fintype α] : FinPartOrd :=
⟨⟨α, inferInstance⟩⟩
@[simp]
theorem coe_of (α : Type*) [PartialOrder α] [Fintype α] : ↥(of α) = α := rfl
instance : Inhabited FinPartOrd :=
⟨of PUnit⟩
instance largeCategory : LargeCategory FinPartOrd :=
InducedCategory.category FinPartOrd.toPartOrd
instance concreteCategory : ConcreteCategory FinPartOrd :=
InducedCategory.concreteCategory FinPartOrd.toPartOrd
instance hasForgetToPartOrd : HasForget₂ FinPartOrd PartOrd :=
InducedCategory.hasForget₂ FinPartOrd.toPartOrd
instance hasForgetToFintype : HasForget₂ FinPartOrd FintypeCat where
forget₂ :=
{ obj := fun X => ⟨X, inferInstance⟩
-- Porting note: Originally `map := fun X Y => coeFn`
map := fun {X Y} (f : OrderHom X Y) => ⇑f }
/-- Constructs an isomorphism of finite partial orders from an order isomorphism between them. -/
@[simps]
def Iso.mk {α β : FinPartOrd.{u}} (e : α ≃o β) : α ≅ β where
hom := (e : OrderHom _ _)
inv := (e.symm : OrderHom _ _)
hom_inv_id := by
ext
exact e.symm_apply_apply _
inv_hom_id := by
ext
exact e.apply_symm_apply _
/-- `OrderDual` as a functor. -/
@[simps]
def dual : FinPartOrd ⥤ FinPartOrd where
obj X := of Xᵒᵈ
map {X Y} := OrderHom.dual
/-- The equivalence between `FinPartOrd` and itself induced by `OrderDual` both ways. -/
@[simps! functor inverse]
def dualEquiv : FinPartOrd ≌ FinPartOrd :=
CategoryTheory.Equivalence.mk dual dual
(NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X)
(NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X)
end FinPartOrd
theorem FinPartOrd_dual_comp_forget_to_partOrd :
FinPartOrd.dual ⋙ forget₂ FinPartOrd PartOrd =
forget₂ FinPartOrd PartOrd ⋙ PartOrd.dual := rfl