Skip to content

Commit e292ba0

Browse files
antoinelab01qawbecrdtey
antoinelab01
and
qawbecrdtey
committed
feat: port combinatorics.quiver.single obj (#1686)
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com>
1 parent 2d1d054 commit e292ba0

File tree

2 files changed

+181
-0
lines changed

2 files changed

+181
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -206,6 +206,7 @@ import Mathlib.Combinatorics.Quiver.Cast
206206
import Mathlib.Combinatorics.Quiver.ConnectedComponent
207207
import Mathlib.Combinatorics.Quiver.Path
208208
import Mathlib.Combinatorics.Quiver.Push
209+
import Mathlib.Combinatorics.Quiver.SingleObj
209210
import Mathlib.Combinatorics.Quiver.Subquiver
210211
import Mathlib.Combinatorics.Quiver.Symmetric
211212
import Mathlib.Combinatorics.SetFamily.Compression.Down

‎Mathlib/Combinatorics/Quiver/SingleObj.lean‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
/-
2+
Copyright (c) 2023 Antoine Labelle. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Antoine Labelle
5+
6+
! This file was ported from Lean 3 source module combinatorics.quiver.single_obj
7+
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Combinatorics.Quiver.Cast
12+
import Mathlib.Combinatorics.Quiver.Symmetric
13+
14+
/-!
15+
# Single-object quiver
16+
17+
Single object quiver with a given arrows type.
18+
19+
## Main definitions
20+
21+
Given a type `α`, `SingleObj α` is the `unit` type, whose single object is called `star α`, with
22+
`Quiver` structure such that `star α ⟶ star α` is the type `α`.
23+
An element `x : α` can be reinterpreted as an element of `star α ⟶ star α` using
24+
`toHom`.
25+
More generally, a list of elements of `a` can be reinterpreted as a path from `star α` to
26+
itself using `pathEquivList`.
27+
-/
28+
29+
30+
namespace Quiver
31+
32+
/-- Type tag on `Unit` used to define single-object quivers. -/
33+
-- Porting note: Removed.
34+
@[nolint unusedArguments]
35+
def SingleObj (_ : Type _) : Type :=
36+
Unit
37+
#align quiver.single_obj Quiver.SingleObj
38+
39+
-- Porting note: `deriving` from above has been moved to below.
40+
instance : Unique (SingleObj α) where
41+
default := ⟨⟩
42+
uniq := fun _ => rfl
43+
44+
namespace SingleObj
45+
46+
variable (α β γ : Type _)
47+
48+
instance : Quiver (SingleObj α) :=
49+
⟨fun _ _ => α⟩
50+
51+
/-- The single object in `SingleObj α`. -/
52+
def star : SingleObj α :=
53+
Unit.unit
54+
#align quiver.single_obj.star Quiver.SingleObj.star
55+
56+
instance : Inhabited (SingleObj α) :=
57+
⟨star α⟩
58+
59+
variable {α β γ}
60+
61+
lemma ext {x y : SingleObj α} : x = y := Unit.ext x y
62+
63+
-- See note [reducible non-instances]
64+
/-- Equip `SingleObj α` with a reverse operation. -/
65+
@[reducible]
66+
def hasReverse (rev : α → α) : HasReverse (SingleObj α) := ⟨rev⟩
67+
#align quiver.single_obj.has_reverse Quiver.SingleObj.hasReverse
68+
69+
-- See note [reducible non-instances]
70+
/-- Equip `SingleObj α` with an involutive reverse operation. -/
71+
@[reducible]
72+
def hasInvolutiveReverse (rev : α → α) (h : Function.Involutive rev) :
73+
HasInvolutiveReverse (SingleObj α)
74+
where
75+
toHasReverse := hasReverse rev
76+
inv' := h
77+
#align quiver.single_obj.has_involutive_reverse Quiver.SingleObj.hasInvolutiveReverse
78+
79+
/-- The type of arrows from `star α` to itself is equivalent to the original type `α`. -/
80+
@[simps]
81+
def toHom : α ≃ (star α ⟶ star α) :=
82+
Equiv.refl _
83+
#align quiver.single_obj.to_hom Quiver.SingleObj.toHom
84+
85+
/-- Prefunctors between two `SingleObj` quivers correspond to functions between the corresponding
86+
arrows types.
87+
-/
88+
@[simps]
89+
def toPrefunctor : (α → β) ≃ SingleObj α ⥤q SingleObj β
90+
where
91+
toFun f := ⟨id, f⟩
92+
invFun f a := f.map (toHom a)
93+
left_inv _ := rfl
94+
right_inv _ := rfl
95+
96+
#align quiver.single_obj.to_prefunctor Quiver.SingleObj.toPrefunctor
97+
98+
theorem toPrefunctor_id : toPrefunctor id = 𝟭q (SingleObj α) :=
99+
rfl
100+
#align quiver.single_obj.to_prefunctor_id Quiver.SingleObj.toPrefunctor_id
101+
102+
@[simp]
103+
theorem toPrefunctor_symm_id : toPrefunctor.symm (𝟭q (SingleObj α)) = id :=
104+
rfl
105+
#align quiver.single_obj.to_prefunctor_symm_id Quiver.SingleObj.toPrefunctor_symm_id
106+
107+
theorem toPrefunctor_comp (f : α → β) (g : β → γ) :
108+
toPrefunctor (g ∘ f) = toPrefunctor f ⋙q toPrefunctor g :=
109+
rfl
110+
#align quiver.single_obj.to_prefunctor_comp Quiver.SingleObj.toPrefunctor_comp
111+
112+
@[simp]
113+
theorem toPrefunctor_symm_comp (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ) :
114+
toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f := by
115+
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]
116+
#align quiver.single_obj.to_prefunctor_symm_comp Quiver.SingleObj.toPrefunctor_symm_comp
117+
118+
/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
119+
Converts a path in the quiver `single_obj α` into a list of elements of type `a`.
120+
-/
121+
def pathToList : ∀ {x : SingleObj α}, Path (star α) x → List α
122+
| _, Path.nil => []
123+
| _, Path.cons p a => a :: pathToList p
124+
#align quiver.single_obj.path_to_list Quiver.SingleObj.pathToList
125+
126+
/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
127+
Converts a list of elements of type `α` into a path in the quiver `SingleObj α`.
128+
-/
129+
@[simp]
130+
def listToPath : List α → Path (star α) (star α)
131+
| [] => Path.nil
132+
| a :: l => (listToPath l).cons a
133+
#align quiver.single_obj.list_to_path Quiver.SingleObj.listToPath
134+
135+
theorem listToPath_pathToList {x : SingleObj α} (p : Path (star α) x) :
136+
listToPath (pathToList p) = p.cast rfl ext :=
137+
by
138+
induction' p with y z p a ih
139+
rfl
140+
dsimp at *; rw [ih]
141+
#align quiver.single_obj.path_to_list_to_path Quiver.SingleObj.listToPath_pathToList
142+
143+
theorem pathToList_listToPath (l : List α) : pathToList (listToPath l) = l :=
144+
by
145+
induction' l with a l ih
146+
rfl
147+
change a :: pathToList (listToPath l) = a :: l; rw [ih]
148+
149+
#align quiver.single_obj.list_to_path_to_list Quiver.SingleObj.pathToList_listToPath
150+
151+
/-- Paths in `SingleObj α` quiver correspond to lists of elements of type `α`. -/
152+
def pathEquivList : Path (star α) (star α) ≃ List α :=
153+
⟨pathToList, listToPath, fun p => listToPath_pathToList p, pathToList_listToPath⟩
154+
#align quiver.single_obj.path_equiv_list Quiver.SingleObj.pathEquivList
155+
156+
@[simp]
157+
theorem pathEquivList_nil : pathEquivList Path.nil = ([] : List α) :=
158+
rfl
159+
#align quiver.single_obj.path_equiv_list_nil Quiver.SingleObj.pathEquivList_nil
160+
161+
@[simp]
162+
theorem pathEquivList_cons (p : Path (star α) (star α)) (a : star α ⟶ star α) :
163+
pathEquivList (Path.cons p a) = a :: pathToList p :=
164+
rfl
165+
#align quiver.single_obj.path_equiv_list_cons Quiver.SingleObj.pathEquivList_cons
166+
167+
@[simp]
168+
theorem pathEquivList_symm_nil : pathEquivList.symm ([] : List α) = Path.nil :=
169+
rfl
170+
#align quiver.single_obj.path_equiv_list_symm_nil Quiver.SingleObj.pathEquivList_symm_nil
171+
172+
@[simp]
173+
theorem pathEquivList_symm_cons (l : List α) (a : α) :
174+
pathEquivList.symm (a :: l) = Path.cons (pathEquivList.symm l) a :=
175+
rfl
176+
#align quiver.single_obj.path_equiv_list_symm_cons Quiver.SingleObj.pathEquivList_symm_cons
177+
178+
end SingleObj
179+
180+
end Quiver

0 commit comments

Comments
 (0)