@@ -22,11 +22,162 @@ Similarly, the binary coproduct of two types `X` and `Y` identifies to
2222
2323@[expose] public section
2424
25- universe v u
25+ universe w v u
2626
27- open CategoryTheory Limits
27+ namespace CategoryTheory
2828
29- namespace CategoryTheory.Limits.Types
29+ namespace Limits
30+
31+ variable {C : Type u} (F : C → Type v)
32+
33+ /-- Given a functor `F : Discrete C ⥤ Type v`, this is a "cofan" for `F`,
34+ but we allow the point to be in `Type w` for an arbitrary universe `w`. -/
35+ abbrev CofanTypes := Functor.CoconeTypes.{w} (Discrete.functor F)
36+
37+ variable {F}
38+
39+ namespace CofanTypes
40+
41+ /-- The injection map for a cofan of a functor to types. -/
42+ abbrev inj (c : CofanTypes.{w} F) (i : C) : F i → c.pt := c.ι ⟨i⟩
43+
44+ variable (F) in
45+ /-- The cofan given by a sigma type. -/
46+ @[simps]
47+ def sigma : CofanTypes F where
48+ pt := Σ (i : C), F i
49+ ι := fun ⟨i⟩ x ↦ ⟨i, x⟩
50+ ι_naturality := by
51+ rintro ⟨i⟩ ⟨j⟩ f
52+ obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
53+ rfl
54+
55+ @[simp]
56+ lemma sigma_inj (i : C) (x : F i) :
57+ (sigma F).inj i x = ⟨i, x⟩ := rfl
58+
59+ lemma isColimit_mk (c : CofanTypes.{w} F)
60+ (h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj i y = x)
61+ (h₂ : ∀ (i : C), Function.Injective (c.inj i))
62+ (h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j) :
63+ Functor.CoconeTypes.IsColimit c where
64+ bijective := by
65+ constructor
66+ · intro x y h
67+ obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x
68+ obtain ⟨⟨j⟩, y, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective y
69+ obtain rfl := h₃ _ _ _ _ h
70+ obtain rfl := h₂ _ h
71+ rfl
72+ · intro x
73+ obtain ⟨i, y, rfl⟩ := h₁ x
74+ exact ⟨(Discrete.functor F).ιColimitType ⟨i⟩ y, rfl⟩
75+
76+ variable (F) in
77+ lemma isColimit_sigma : Functor.CoconeTypes.IsColimit (sigma F) :=
78+ isColimit_mk _ (by aesop)
79+ (fun _ _ _ h ↦ by rw [Sigma.ext_iff] at h; simpa using h)
80+ (fun _ _ _ _ h ↦ congr_arg Sigma.fst h)
81+
82+ variable (F) in
83+ /-- Given a cofan of a functor to types, this is a canonical map
84+ from the Sigma type to the point of the cofan. -/
85+ @[simp]
86+ def fromSigma (c : CofanTypes.{w} F) (x : Σ (i : C), F i) : c.pt :=
87+ c.inj x.1 x.2
88+
89+ lemma isColimit_iff_bijective_fromSigma (c : CofanTypes.{w} F) :
90+ c.IsColimit ↔ Function.Bijective c.fromSigma := by
91+ rw [(isColimit_sigma F).iff_bijective]
92+ aesop
93+
94+ section
95+
96+ variable {c : CofanTypes.{w} F} (hc : Functor.CoconeTypes.IsColimit c)
97+
98+ include hc
99+
100+ lemma bijective_fromSigma_of_isColimit :
101+ Function.Bijective c.fromSigma := by
102+ rwa [← isColimit_iff_bijective_fromSigma]
103+
104+ /-- The bijection from the sigma type to the point of a colimit cofan
105+ of a functor to types. -/
106+ noncomputable def equivOfIsColimit :
107+ (Σ (i : C), F i) ≃ c.pt :=
108+ Equiv.ofBijective _ (bijective_fromSigma_of_isColimit hc)
109+
110+ @[simp]
111+ lemma equivOfIsColimit_apply (i : C) (x : F i) :
112+ equivOfIsColimit hc ⟨i, x⟩ = c.inj i x := rfl
113+
114+ @[simp]
115+ lemma equivOfIsColimit_symm_apply (i : C) (x : F i) :
116+ (equivOfIsColimit hc).symm (c.inj i x) = ⟨i, x⟩ :=
117+ (equivOfIsColimit hc).injective (by simp)
118+
119+ lemma inj_jointly_surjective_of_isColimit (x : c.pt) :
120+ ∃ (i : C) (y : F i), c.inj i y = x := by
121+ obtain ⟨⟨i⟩, y, rfl⟩ := hc.ι_jointly_surjective x
122+ exact ⟨i, y, rfl⟩
123+
124+ lemma inj_injective_of_isColimit (i : C) :
125+ Function.Injective (c.inj i) := by
126+ intro y₁ y₂ h
127+ simpa using (equivOfIsColimit hc).injective (a₁ := ⟨i, y₁⟩) (a₂ := ⟨i, y₂⟩) h
128+
129+ lemma eq_of_inj_apply_eq_of_isColimit
130+ {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) (h : c.inj i₁ y₁ = c.inj i₂ y₂) :
131+ i₁ = i₂ :=
132+ congr_arg Sigma.fst ((equivOfIsColimit hc).injective (a₁ := ⟨i₁, y₁⟩) (a₂ := ⟨i₂, y₂⟩) h)
133+
134+ end
135+
136+ end CofanTypes
137+
138+ namespace Cofan
139+
140+ variable {C : Type u} {F : C → Type v} (c : Cofan F)
141+
142+ /-- If `F : C → Type v`, then the data of a "type-theoretic" cofan of `F`
143+ with a point in `Type v` is the same as the data of a cocone (in a categorical sense). -/
144+ @[simps]
145+ def cofanTypes :
146+ CofanTypes.{v} F where
147+ pt := c.pt
148+ ι := fun ⟨j⟩ ↦ c.inj j
149+ ι_naturality := by
150+ rintro ⟨i⟩ ⟨j⟩ f
151+ obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
152+ rfl
153+
154+ lemma isColimit_cofanTypes_iff :
155+ c.cofanTypes.IsColimit ↔ Nonempty (IsColimit c) :=
156+ Functor.CoconeTypes.isColimit_iff _
157+
158+ lemma nonempty_isColimit_iff_bijective_fromSigma :
159+ Nonempty (IsColimit c) ↔ Function.Bijective c.cofanTypes.fromSigma := by
160+ rw [← isColimit_cofanTypes_iff, CofanTypes.isColimit_iff_bijective_fromSigma]
161+
162+ variable {c}
163+
164+ lemma inj_jointly_surjective_of_isColimit (hc : IsColimit c) (x : c.pt) :
165+ ∃ (i : C) (y : F i), c.inj i y = x :=
166+ CofanTypes.inj_jointly_surjective_of_isColimit
167+ ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) x
168+
169+ lemma inj_injective_of_isColimit (hc : IsColimit c) (i : C) :
170+ Function.Injective (c.inj i) :=
171+ CofanTypes.inj_injective_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) i
172+
173+ lemma eq_of_inj_apply_eq_of_isColimit (hc : IsColimit c)
174+ {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) (h : c.inj i₁ y₁ = c.inj i₂ y₂) :
175+ i₁ = i₂ :=
176+ CofanTypes.eq_of_inj_apply_eq_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) _ _ h
177+
178+ end Cofan
179+
180+ namespace Types
30181
31182/-- The category of types has `PEmpty` as an initial object. -/
32183def initialColimitCocone : Limits.ColimitCocone (Functor.empty (Type u)) where
0 commit comments