Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit e8ac631

Browse files
YaelDilliesParcly-Taxel
YaelDillies
and
Parcly-Taxel
committed
chore(order/category): Rename categories (#18657)
The Lean 4 naming convention forces us to rename the categories of orders. Instead of blankly appending `Cat` to the names, we proactively shorten the names. Incidentally, this gets them closer to the way they're referred in the literature. * `Preorder` → `Preord` (the literature name is `Ord`, but Lean 4 already takes it) * `PartialOrder` → `PartOrd` * `BoundedOrder` → `BddOrd` * `FinPartialOrder` → `FinPartOrd` * `SemilatticeSup` → `SemilatSup` * `SemilatticeInf` → `SemilatInf` * `Lattice` → `Lat` * `DistribLattice` → `DistLat` * `BoundedLattice` → `BddLat` * `BoundedDistribLattice` → `BddDistLat` * `LinearOrder` → `LinOrd` * `CompleteLattice` → `CompleteLat` * `Frame` → `Frm` (the corresponding class is `Order.Frame`, but better be safe) Co-authored-by: Jeremy Tan Jie Rui <e0191785@u.nus.edu>
1 parent 0187644 commit e8ac631

29 files changed

Lines changed: 886 additions & 887 deletions

‎src/algebraic_topology/simplex_category.lean‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -811,8 +811,7 @@ end epi_mono
811811
to the category attached to the ordered set `{0, 1, ..., n}` -/
812812
@[simps obj map]
813813
def to_Cat : simplex_category ⥤ Cat.{0} :=
814-
simplex_category.skeletal_functor ⋙ forget₂ NonemptyFinLinOrd LinearOrder ⋙
815-
forget₂ LinearOrder Lattice ⋙ forget₂ Lattice PartialOrder ⋙
816-
forget₂ PartialOrder Preorder ⋙ Preorder_to_Cat
814+
simplex_category.skeletal_functor ⋙ forget₂ NonemptyFinLinOrd LinOrd ⋙
815+
forget₂ LinOrd Lat ⋙ forget₂ Lat PartOrd ⋙ forget₂ PartOrd Preord ⋙ Preord_to_Cat
817816

818817
end simplex_category

‎src/order/category/BddDistLat.lean‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
/-
2+
Copyright (c) 2022 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
-/
6+
import order.category.BddLat
7+
import order.category.DistLat
8+
9+
/-!
10+
# The category of bounded distributive lattices
11+
12+
This defines `BddDistLat`, the category of bounded distributive lattices.
13+
14+
Note that this category is sometimes called [`DistLat`](https://ncatlab.org/nlab/show/DistLat) when
15+
being a lattice is understood to entail having a bottom and a top element.
16+
-/
17+
18+
universes u
19+
20+
open category_theory
21+
22+
/-- The category of bounded distributive lattices with bounded lattice morphisms. -/
23+
structure BddDistLat :=
24+
(to_DistLat : DistLat)
25+
[is_bounded_order : bounded_order to_DistLat]
26+
27+
namespace BddDistLat
28+
29+
instance : has_coe_to_sort BddDistLat Type* := ⟨λ X, X.to_DistLat⟩
30+
instance (X : BddDistLat) : distrib_lattice X := X.to_DistLat.str
31+
32+
attribute [instance] BddDistLat.is_bounded_order
33+
34+
/-- Construct a bundled `BddDistLat` from a `bounded_order` `distrib_lattice`. -/
35+
def of (α : Type*) [distrib_lattice α] [bounded_order α] : BddDistLat := ⟨⟨α⟩⟩
36+
37+
@[simp] lemma coe_of (α : Type*) [distrib_lattice α] [bounded_order α] : ↥(of α) = α := rfl
38+
39+
instance : inhabited BddDistLat := ⟨of punit⟩
40+
41+
/-- Turn a `BddDistLat` into a `BddLat` by forgetting it is distributive. -/
42+
def to_BddLat (X : BddDistLat) : BddLat := BddLat.of X
43+
44+
@[simp] lemma coe_to_BddLat (X : BddDistLat) : ↥X.to_BddLat = ↥X := rfl
45+
46+
instance : large_category.{u} BddDistLat := induced_category.category to_BddLat
47+
48+
instance : concrete_category BddDistLat :=
49+
induced_category.concrete_category to_BddLat
50+
51+
instance has_forget_to_DistLat : has_forget₂ BddDistLat DistLat :=
52+
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_lattice_hom } }
53+
54+
instance has_forget_to_BddLat : has_forget₂ BddDistLat BddLat :=
55+
induced_category.has_forget₂ to_BddLat
56+
57+
lemma forget_BddLat_Lat_eq_forget_DistLat_Lat :
58+
forget₂ BddDistLat BddLat ⋙ forget₂ BddLat Lat =
59+
forget₂ BddDistLat DistLat ⋙ forget₂ DistLat Lat := rfl
60+
61+
/-- Constructs an equivalence between bounded distributive lattices from an order isomorphism
62+
between them. -/
63+
@[simps] def iso.mk {α β : BddDistLat.{u}} (e : α ≃o β) : α ≅ β :=
64+
{ hom := (e : bounded_lattice_hom α β),
65+
inv := (e.symm : bounded_lattice_hom β α),
66+
hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
67+
inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }
68+
69+
/-- `order_dual` as a functor. -/
70+
@[simps] def dual : BddDistLat ⥤ BddDistLat :=
71+
{ obj := λ X, of Xᵒᵈ, map := λ X Y, bounded_lattice_hom.dual }
72+
73+
/-- The equivalence between `BddDistLat` and itself induced by `order_dual` both ways. -/
74+
@[simps functor inverse] def dual_equiv : BddDistLat ≌ BddDistLat :=
75+
equivalence.mk dual dual
76+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
77+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
78+
79+
end BddDistLat
80+
81+
lemma BddDistLat_dual_comp_forget_to_DistLat :
82+
BddDistLat.dual ⋙ forget₂ BddDistLat DistLat =
83+
forget₂ BddDistLat DistLat ⋙ DistLat.dual := rfl

‎src/order/category/BddLat.lean‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
/-
2+
Copyright (c) 2022 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
-/
6+
import order.category.BddOrd
7+
import order.category.Lat
8+
import order.category.Semilat
9+
10+
/-!
11+
# The category of bounded lattices
12+
13+
This file defines `BddLat`, the category of bounded lattices.
14+
15+
In literature, this is sometimes called `Lat`, the category of lattices, because being a lattice is
16+
understood to entail having a bottom and a top element.
17+
-/
18+
19+
universes u
20+
21+
open category_theory
22+
23+
/-- The category of bounded lattices with bounded lattice morphisms. -/
24+
structure BddLat :=
25+
(to_Lat : Lat)
26+
[is_bounded_order : bounded_order to_Lat]
27+
28+
namespace BddLat
29+
30+
instance : has_coe_to_sort BddLat Type* := ⟨λ X, X.to_Lat⟩
31+
instance (X : BddLat) : lattice X := X.to_Lat.str
32+
33+
attribute [instance] BddLat.is_bounded_order
34+
35+
/-- Construct a bundled `BddLat` from `lattice` + `bounded_order`. -/
36+
def of (α : Type*) [lattice α] [bounded_order α] : BddLat := ⟨⟨α⟩⟩
37+
38+
@[simp] lemma coe_of (α : Type*) [lattice α] [bounded_order α] : ↥(of α) = α := rfl
39+
40+
instance : inhabited BddLat := ⟨of punit⟩
41+
42+
instance : large_category.{u} BddLat :=
43+
{ hom := λ X Y, bounded_lattice_hom X Y,
44+
id := λ X, bounded_lattice_hom.id X,
45+
comp := λ X Y Z f g, g.comp f,
46+
id_comp' := λ X Y, bounded_lattice_hom.comp_id,
47+
comp_id' := λ X Y, bounded_lattice_hom.id_comp,
48+
assoc' := λ W X Y Z _ _ _, bounded_lattice_hom.comp_assoc _ _ _ }
49+
50+
instance : concrete_category BddLat :=
51+
{ forget := ⟨coe_sort, λ X Y, coe_fn, λ X, rfl, λ X Y Z f g, rfl⟩,
52+
forget_faithful := ⟨λ X Y, by convert fun_like.coe_injective⟩ }
53+
54+
instance has_forget_to_BddOrd : has_forget₂ BddLat BddOrd :=
55+
{ forget₂ := { obj := λ X, BddOrd.of X,
56+
map := λ X Y, bounded_lattice_hom.to_bounded_order_hom } }
57+
58+
instance has_forget_to_Lat : has_forget₂ BddLat Lat :=
59+
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_lattice_hom } }
60+
61+
instance has_forget_to_SemilatSup : has_forget₂ BddLat SemilatSup :=
62+
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_sup_bot_hom } }
63+
64+
instance has_forget_to_SemilatInf : has_forget₂ BddLat SemilatInf :=
65+
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_inf_top_hom } }
66+
67+
@[simp] lemma coe_forget_to_BddOrd (X : BddLat) :
68+
↥((forget₂ BddLat BddOrd).obj X) = ↥X := rfl
69+
70+
@[simp] lemma coe_forget_to_Lat (X : BddLat) :
71+
↥((forget₂ BddLat Lat).obj X) = ↥X := rfl
72+
73+
@[simp] lemma coe_forget_to_SemilatSup (X : BddLat) :
74+
↥((forget₂ BddLat SemilatSup).obj X) = ↥X := rfl
75+
76+
@[simp] lemma coe_forget_to_SemilatInf (X : BddLat) :
77+
↥((forget₂ BddLat SemilatInf).obj X) = ↥X := rfl
78+
79+
lemma forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd :
80+
forget₂ BddLat Lat ⋙ forget₂ Lat PartOrd =
81+
forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl
82+
83+
lemma forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd :
84+
forget₂ BddLat SemilatSup ⋙ forget₂ SemilatSup PartOrd =
85+
forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl
86+
87+
lemma forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd :
88+
forget₂ BddLat SemilatInf ⋙ forget₂ SemilatInf PartOrd =
89+
forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl
90+
91+
/-- Constructs an equivalence between bounded lattices from an order isomorphism
92+
between them. -/
93+
@[simps] def iso.mk {α β : BddLat.{u}} (e : α ≃o β) : α ≅ β :=
94+
{ hom := e,
95+
inv := e.symm,
96+
hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
97+
inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }
98+
99+
/-- `order_dual` as a functor. -/
100+
@[simps] def dual : BddLat ⥤ BddLat :=
101+
{ obj := λ X, of Xᵒᵈ, map := λ X Y, bounded_lattice_hom.dual }
102+
103+
/-- The equivalence between `BddLat` and itself induced by `order_dual` both ways. -/
104+
@[simps functor inverse] def dual_equiv : BddLat ≌ BddLat :=
105+
equivalence.mk dual dual
106+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
107+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
108+
109+
end BddLat
110+
111+
lemma BddLat_dual_comp_forget_to_BddOrd :
112+
BddLat.dual ⋙ forget₂ BddLat BddOrd =
113+
forget₂ BddLat BddOrd ⋙ BddOrd.dual := rfl
114+
115+
lemma BddLat_dual_comp_forget_to_Lat :
116+
BddLat.dual ⋙ forget₂ BddLat Lat =
117+
forget₂ BddLat Lat ⋙ Lat.dual := rfl
118+
119+
lemma BddLat_dual_comp_forget_to_SemilatSup :
120+
BddLat.dual ⋙ forget₂ BddLat SemilatSup =
121+
forget₂ BddLat SemilatInf ⋙ SemilatInf.dual := rfl
122+
123+
lemma BddLat_dual_comp_forget_to_SemilatInf :
124+
BddLat.dual ⋙ forget₂ BddLat SemilatInf =
125+
forget₂ BddLat SemilatSup ⋙ SemilatSup.dual := rfl

‎src/order/category/BddOrd.lean‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
/-
2+
Copyright (c) 2022 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
-/
6+
import category_theory.category.Bipointed
7+
import order.category.PartOrd
8+
import order.hom.bounded
9+
10+
/-!
11+
# The category of bounded orders
12+
13+
This defines `BddOrd`, the category of bounded orders.
14+
-/
15+
16+
universes u v
17+
18+
open category_theory
19+
20+
/-- The category of bounded orders with monotone functions. -/
21+
structure BddOrd :=
22+
(to_PartOrd : PartOrd)
23+
[is_bounded_order : bounded_order to_PartOrd]
24+
25+
namespace BddOrd
26+
27+
instance : has_coe_to_sort BddOrd Type* := induced_category.has_coe_to_sort to_PartOrd
28+
instance (X : BddOrd) : partial_order X := X.to_PartOrd.str
29+
30+
attribute [instance] BddOrd.is_bounded_order
31+
32+
/-- Construct a bundled `BddOrd` from a `fintype` `partial_order`. -/
33+
def of (α : Type*) [partial_order α] [bounded_order α] : BddOrd := ⟨⟨α⟩⟩
34+
35+
@[simp] lemma coe_of (α : Type*) [partial_order α] [bounded_order α] : ↥(of α) = α := rfl
36+
37+
instance : inhabited BddOrd := ⟨of punit⟩
38+
39+
instance large_category : large_category.{u} BddOrd :=
40+
{ hom := λ X Y, bounded_order_hom X Y,
41+
id := λ X, bounded_order_hom.id X,
42+
comp := λ X Y Z f g, g.comp f,
43+
id_comp' := λ X Y, bounded_order_hom.comp_id,
44+
comp_id' := λ X Y, bounded_order_hom.id_comp,
45+
assoc' := λ W X Y Z _ _ _, bounded_order_hom.comp_assoc _ _ _ }
46+
47+
instance concrete_category : concrete_category BddOrd :=
48+
{ forget := ⟨coe_sort, λ X Y, coe_fn, λ X, rfl, λ X Y Z f g, rfl⟩,
49+
forget_faithful := ⟨λ X Y, by convert fun_like.coe_injective⟩ }
50+
51+
instance has_forget_to_PartOrd : has_forget₂ BddOrd PartOrd :=
52+
{ forget₂ := { obj := λ X, X.to_PartOrd, map := λ X Y, bounded_order_hom.to_order_hom } }
53+
54+
instance has_forget_to_Bipointed : has_forget₂ BddOrd Bipointed :=
55+
{ forget₂ := { obj := λ X, ⟨X, ⊥, ⊤⟩, map := λ X Y f, ⟨f, map_bot f, map_top f⟩ },
56+
forget_comp := rfl }
57+
58+
/-- `order_dual` as a functor. -/
59+
@[simps] def dual : BddOrd ⥤ BddOrd :=
60+
{ obj := λ X, of Xᵒᵈ, map := λ X Y, bounded_order_hom.dual }
61+
62+
/-- Constructs an equivalence between bounded orders from an order isomorphism between them. -/
63+
@[simps] def iso.mk {α β : BddOrd.{u}} (e : α ≃o β) : α ≅ β :=
64+
{ hom := e,
65+
inv := e.symm,
66+
hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
67+
inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }
68+
69+
/-- The equivalence between `BddOrd` and itself induced by `order_dual` both ways. -/
70+
@[simps functor inverse] def dual_equiv : BddOrd ≌ BddOrd :=
71+
equivalence.mk dual dual
72+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
73+
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
74+
75+
end BddOrd
76+
77+
lemma BddOrd_dual_comp_forget_to_PartOrd :
78+
BddOrd.dual ⋙ forget₂ BddOrd PartOrd =
79+
forget₂ BddOrd PartOrd ⋙ PartOrd.dual := rfl
80+
81+
lemma BddOrd_dual_comp_forget_to_Bipointed :
82+
BddOrd.dual ⋙ forget₂ BddOrd Bipointed =
83+
forget₂ BddOrd Bipointed ⋙ Bipointed.swap := rfl

‎src/order/category/BoolAlg.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -32,16 +32,16 @@ def of (α : Type*) [boolean_algebra α] : BoolAlg := bundled.of α
3232

3333
instance : inhabited BoolAlg := ⟨of punit⟩
3434

35-
/-- Turn a `BoolAlg` into a `BoundedDistribLattice` by forgetting its complement operation. -/
36-
def to_BoundedDistribLattice (X : BoolAlg) : BoundedDistribLattice := BoundedDistribLattice.of X
35+
/-- Turn a `BoolAlg` into a `BddDistLat` by forgetting its complement operation. -/
36+
def to_BddDistLat (X : BoolAlg) : BddDistLat := BddDistLat.of X
3737

38-
@[simp] lemma coe_to_BoundedDistribLattice (X : BoolAlg) : ↥X.to_BoundedDistribLattice = ↥X := rfl
38+
@[simp] lemma coe_to_BddDistLat (X : BoolAlg) : ↥X.to_BddDistLat = ↥X := rfl
3939

40-
instance : large_category.{u} BoolAlg := induced_category.category to_BoundedDistribLattice
41-
instance : concrete_category BoolAlg := induced_category.concrete_category to_BoundedDistribLattice
40+
instance : large_category.{u} BoolAlg := induced_category.category to_BddDistLat
41+
instance : concrete_category BoolAlg := induced_category.concrete_category to_BddDistLat
4242

43-
instance has_forget_to_BoundedDistribLattice : has_forget₂ BoolAlg BoundedDistribLattice :=
44-
induced_category.has_forget₂ to_BoundedDistribLattice
43+
instance has_forget_to_BddDistLat : has_forget₂ BoolAlg BddDistLat :=
44+
induced_category.has_forget₂ to_BddDistLat
4545

4646
section
4747

@@ -71,6 +71,6 @@ equivalence.mk dual dual
7171

7272
end BoolAlg
7373

74-
lemma BoolAlg_dual_comp_forget_to_BoundedDistribLattice :
75-
BoolAlg.dual ⋙ forget₂ BoolAlg BoundedDistribLattice =
76-
forget₂ BoolAlg BoundedDistribLattice ⋙ BoundedDistribLattice.dual := rfl
74+
lemma BoolAlg_dual_comp_forget_to_BddDistLat :
75+
BoolAlg.dual ⋙ forget₂ BoolAlg BddDistLat =
76+
forget₂ BoolAlg BddDistLat ⋙ BddDistLat.dual := rfl

0 commit comments

Comments
 (0)